[Prev][Next][Index]

Re: Basic LSL Questions

Steve,

You are not alone.  The "specification in the large" features of LSL
have consistently been the hardest part of the language for us to explain
clearly.  (They were also among the trickiest to design and implement.)
If they did not seem so important, we would surely have scrapped them by
now.

    1-I'm assuming that a trait definition with an includes statement can
    be replaced with the trait definitions and all definitions in the
    included trait.  I don't quite understand what 'discharging' the
    definitions mean for an assumes statement.  Does it simply mean to
    ignore the definitions for any trait if it is included or assumed by a
    'parent' trait?

The description in Chapter 4 of the Larch book is fairly informal, and
attempts to indicate how we expect these features to be used, rather than
to give a precise semantics.  (We did that for an earlier version of the
language in "Report on the Larch Shared Language: Version 2.3," SRC-58,
but people found the technical detail off-putting.)  You will find a
more precise description of their interpretation in Chapter 7, especially
sections 7.1 and 7.2, which describe the proof obligations associated with
these constructs.

Once again, "includes" and "assumes" clauses are equivalent in terms of the
theory generated--they differ only in the checking.

	eg	X:trait
			Includes Y,Z
		
		Y:trait
			Includes A
			Assumes B

	Does this mean that X would inherit all of A's
	definitions and ignore B's definitions?  How would
	conflicting definitions be handled.

X will certainly inherit all of A's definitions.  Whether it inherits B's
definitions depends on precisely what you mean by "inherits."  The semantic
requirement is that X's body plus its externals (other than Y) must imply
B.
- So "X inherits B" in the sense that the theory of B is part of the
  theory of X.
- However, "X doesn't inherit B" in the sense that X's theory must be
  exactly the same as it would be if Y did not assume B.

If B and Z give conflicting definitions, this is an inconsistency, no
different from A and Z giving conflicting definitions.

    2-Are implies statements used only in proofs about the trait, or are
    traits given on an implies statement also inherited by the parent
    trait?

The implies statements identify "intended theorems."  If these theorems are
proved once for the original trait, then they can be used in all traits
that include (or assume) it, since adding more axioms will not falsify
theorems that can be proved from the original axioms.  So it makes sense to
"inherit" them, rather than repeatedly reproving them.  [NB: There are some
important technical restrictions on the form of theorems for which this
"monotonicity" property holds.  I expect Steve Garland will want to clarify
this point. :-]

I hope this helps.

Jim H.
Reference(s):