[Prev][Next][Index][Thread]
Pratt's conjectures
Date: Tue, 22 Nov 88 13:47:23 PST
Vaughan's conjecture about "optimal augments" is correct.
There is indeed an optimal augment for any extension and it
can be obtained as the *intersection* of all *maximal* base-
conservative augments in his terminology. Any identification
not common to all such augments is in effect "controversial".
Another way to understand this is to say that any two ground
terms identified in the intersection are "inseparable" in that
they cannot be observably distinguished in any context in any
base-conservative augment.
The optimal augment obviously coincides with the greatest
augment when the latter exists, since in this case there is a
single maximal augment.
The idea of "controversial" identifications is the really
interesting idea here. Why are they controversial? Because
they may be contradicted by a possible augment. The point is
that semantics should provide a basis for reasoning about a
specification -- what else is it good for? It would be
distressing if a semantically valid conclusion about a
specification fails to hold up after legitimate augmentation of
the specification.
Of course, augmentation in the informal sense may or may not
be signature-preserving -- the question about optimal
augments can obviously be parameterized wrt a notion of
augmentation. It turns out that if augments are free to add
arbitrarily to the signature, then the "optimal" augment is
always precisely the *initial* algebra of the extension. What
this says is that when one is reasoning about a specification
based on some semantic foundation, one should always be
conscious of the range of validity of the reasoning wrt possible
enhancements of the specification. For instance, theorems
proved using "proof by consistency" are based on final algebra
semantics, which is the optimal semantics only within
Vaughan's strict notion of augmentation. These theorems
won't hold up in general if the theory is
enhanced with new symbols.
Satish Thatte