[Prev][Next][Index][Thread]
More on Pratt's conjectures
To continue my response to Vaughan's conjectures:
Here is an example where a *restriction* of the notion of
augmentation leads to interesting results (as opposed to the
generalization I mentioned in my last message which identifies
augmentation with extension and leads to initial algebra
semantics as the "optimal" semantics):
Kapur and Musser introduced a notion of "completable"
extension of a base theory in their paper on proof by
consistency in LICS, 1986 (their formulation is a little different,
but I won't go into the details here). For our purposes, we may
define a completable extension as any extension which has a
*standard model*, i.e., a model in which the only values of
observable sort are those in the initial model of the base
theory. Now suppose we have a base theory T0 and extension
T1, and we are interested in the optimal augment of T1 as
before, but this time, we want to restrict attention to those
augments which are *completable* extensions of T0. Such an
optimal completable augment always exists but it is *not*
always the same as the optimal augment among *all* augments.
Here is an example which shows the difference (it is from the
LICS paper of Kapur-Musser):
Let T0 be a theory of natural numbers with only
0: --> NAT
SUC: NAT --> NAT
and no equations. Now let T1 be an extension which introduces
three new symbols
PLUS: NAT x NAT --> NAT
DOUBLE: NAT --> NAT
K: --> NAT
and the equations
PLUS(0, x) = x
PLUS(SUC(x), y) = SUC(PLUS(x, y))
DOUBLE(0) = 0
DOUBLE(SUC(x)) = SUC(SUC(DOUBLE(x)))
Now the assertion
DOUBLE(x) = PLUS(x, x)
holds in the optimal completable augment but not in the
general optimal augment. The reason is that one may identify
DOUBLE(K)=SUC(0) in a general augment but not in a
completable one (assuming, of course, that all augments are
conservative).
The proof techniques Kapur and Musser give in their paper are
based on "optimal completable augment semantics". It almost
seems as if there is a need for a discipline of "semantic
engineering" where semantics is tailored to the reasoning
context!
Satish Thatte