[Prev][Next][Index]
Re: Consistency

To: Daniel.Schweizer@qmail.tik.ethz.ch (Daniel Schweizer)

Subject: Re: Consistency

From: horning

Date: Tue, 24 Aug 93 11:30:31 0700

Cc: horning

InReplyTo: Message of Thu, 5 Aug 1993 20:32:06 MET
Daniel,
Sorry for the delay in responding; questions are definitely welcome.
You are definitely in a "thin ice" area of LSL/LP. Proving inconsistency is
often easy. Proving consistency is not. Jim Saxe has given quite a bit of
thought to this. He would like a "definitional" capability that allows one
to introduce definitions that are guaranteed not to create inconsistencies.
(Basically, this is the only kind of definitions allowed in BoyerMoore's
NQTHM.) This doesn't solve the problem of proving that your axioms are
consistent, but it at least reduces the number of axioms that you need to
worry about.
Your "trick" of giving the induction rule G1 would be all right if you did
not also provide the generator function "[__, __, __, __]: D, L, T, B >
S". The latter, combined with the four observers, gives a way to generate
the entire Cartesian product, not just the states reached by init, push,
release, timeImpulse, sensorOpen, and sensorClose. If you want to keep G1,
you are going to have to give different definitions of door, light, timer,
and button, e.g.,
door(init) == closed;
light(init) == dark;
...
button(sensorClose(sys)) == button(sys);
The generally recommended style for generating axioms that are sufficient,
but not too strong, for an ADT is to write a lefthandside that applies
each nongenerator to each generator. Such axioms are generally consistent
"by construction." In this case, I don't think the axioms would be much
more complex than yours. (However, in general, it may lead you to write
groups of axioms that can readily be abbreviated by single axioms that are
not in this form.)
You are correct in your suspicion that the reason completing your initial
system could not reveal an inconsistency is that completion deals only with
the equational part of the theory. Using the induction rule to prove a new
equation brought the inconsistency into the domain of completion.
To ensure that an LSL ADT is monomorph, you must in general use a
secondorder axiom (generated by or partitioned by). It's been a little
while since I've considered this topic, so I'm hazy on the details. My
recollection is that if all the operators of a sort except those in a
single "generated by" clause are "converted," then it specifies a monomorph
type.
Jim H.