[Prev][Next][Index]

Re: LSL boolean combinations involving undefined terms



Gary,

This is an area that most people find murky some of the time, and some
people find murky most of the time.

The trouble starts with the title of you message: There are no "undefined
terms" in LSL.  One way to get a carrier set for the algebra of a trait is
to define equivalence classes over the free word algebra of its operators.
Every term's equivalence class can be thought of as its "definition."

Another way to say this is that LSL is a language of total functions.
There are no partial functions associated with operators, although there
may be underspecified operators (i.e., operators bound to functions with
different values in different models).  The possibility of
underspecification is intentional; it is important that models of traits do
not have to be isomorphic.

QTrait says that q.theInt is always of sort Int.  However, it places no
constraint on *which* int it is unless tag(q) = theInt.  So in Q1 and Q2,
both operands of /\ are always defined (i.e., always either true or false,
since Bool is generated by true and false), even though we may not always
know which.  [By the way, you can prove commutativity of /\ by a simple
induction on the generators of Bool.]

So Q1, Q2, and Q3 are all both "legal" and also "correct" in that they all
define the same function for isPositive, which is what you say you had in
mind.

I agree that adding the implication is good practice.

Jim H.

PS One of the tightest corners for the total function interpretation is
division by zero.  You have to make sure that your generated by clause
produces at least one value in the equivalence class of 1/0, something that
is easy to overlook.  Without it, you can prove by induction all the
"paradoxes" involving "hidden" divisions by zero that we learned in high
school.  With it, of course, all your inductions get an extra, sometimes
messy, case.

Follow-Up(s): Reference(s):