Re: LSL boolean combinations involving undefined terms

• Subject: Re: LSL boolean combinations involving undefined terms
• From: garland@lcs.mit.edu (Stephen J. Garland)
• Date: 20 Jul 1995 18:57:18 GMT
• Distribution: world
• Keywords: undefined, lazy evaluation
• Newsgroups: comp.specification.larch
• Organization: lcs.mit.edu
• References: <leavens.805997000@bambam.cs.iastate.edu> <leavens.806079418@bambam.cs.iastate.edu> <3uiv5j$n60@newsflash.concordia.ca>
• Sender: garland@fire.lcs.mit.edu (Stephen J. Garland)

For the record, I agree completely with Patrice Chalin's response to Gary Leaven's
question.  

The semantics of LSL is based on the standard semantics of first-order logic.  Every
structure with an appropriate signature defines some value for every term in an LSL
expression, although the value may not be specified by the axioms of a particular LSL
trait.  Hence, strictly speaking, while there may be such a thing as an "unspecified
value", there is no such thing as an "undefined term".  Furthermore, since every term
has some value in every model, operational notions like "order of evaluation" play no
role in the semantics of first-order logic or LSL.

The proof obligation for "converts isPositive" is trivial to discharge because the trait
contains an explicit definition of isPositive, that is, a definition of the form
     isPositive(x) == ...
where ... does not contain any (direct or recursive) reference to isPositive.

• LSL boolean combinations involving undefined terms
• From: leavens@cs.iastate.edu (Gary Leavens)
• Re: LSL boolean combinations involving undefined terms
• From: leavens@cs.iastate.edu (Gary Leavens)
• Re: LSL boolean combinations involving undefined terms
• From: chalin@cs.concordia.ca (CHALIN patrice)

• Prev: Re: LSL boolean combinations involving undefined terms
• Next: Re: LSL boolean combinations involving undefined terms
• Index: Larch archive index