[Prev][Next][Index][Thread]
Pratt's latest example
Date: Fri, 18 Nov 88 09:09:25 PST
To: types@theory.LCS.MIT.EDU
I confess that I am thoroghly confused by Vaughn Pratt's modification of
Albert Meyer's example. The "wanted" sort NAT has no well-formed terms.
I thought that for final algebras, one usually restricted attention
to the class of *reachable* algebras. That class seems to consist of
algebras with empty carriers for NAT. In what sense can one then
talk of a model with a two element carrier for NAT as being "almost final"?
It seems to me that the following modification of Mitchell Wand's original
example (from his paper on final algebra semantics in JCSS, 1979) is a better
candidate for an "almost final" model. The signature, in addition to 0 and
Succ for NAT, contains
EQ: NAT x NAT --> BOOL
EMPTY: --> ARRAY
ALT: NAT x NAT x ARRAY --> ARRAY
VAL: NAT x ARRAY --> NAT
and just one equation
VAL(x, ALT(y, z, a)) = if EQ(x, y) then z else VAL(x, a)
The complete example had an additional constant UNDEFINED of sort NAT,
and the equation:
VAL(x, EMPTY) = UNDEFINED
The point of this example was that if natural numbers and booleans are the
only observables then array implementations need only maintain the latest
value at any index, forgetting earlier ones. This intuition was captured by
the final algebra for the complete spec.
Leaving the second equation out destroys the example because it now has no
final algebra (VAL(1,EMPTY) can be any natural number in a model).
Nonetheless, the first equation still seems to imply (in the sense of an
"almost final" model) that obsolete values at an index need not be
maintained. The intuition is that *any* way of completing the specification
would lead to a final algebra with this property. This is a somewhat tricky
point to argue, because if arbitrary new symbols are allowed to be added to
the signature, the property cannot be preserved. My point is that this is the
sort of "incomplete" spec for which one should consider "almost final"
models.
Am I making any sense?
Satish Thatte