On Wednesday 28 Sep 2011 13:52, Phil Clayton wrote:
> > I wondered whether the original design intended to map
> > decoration differently for predicates and expressions?
> > Then the user could determine the mapping of e.g. S'
> > as either
> > mk_z_schema_pred (S, "'")
> > mk_z_schema_pred (mk_z_decor%down%s (S, "'"), "")
> > by controlling predicate/expression parsing modes as
> > usual. (As Rob points out, the second is always used
> > currently.)
> To answer my own question: from what Roger is saying,
> this must have been the intention as Z'SchemaPred can
> only occur in a predicate and Z'Decor only in an
The rationale is specific to schemas as predicates, in other
contexts I don't see how to avoid decorating the schema.
I see that the account I gave is pretty much the same as
what Spivey says about decoration of schemas as predicates
on page 72 of the second edition of "The Z notation".
He gives the expansion as "decorated theta term isin schema"
(not in words of course) and I guess we decided to go
straight to the explicit binding display because we knew we
had to have those things and might as well go straight
there, whereas Spivey seemed content to do without them.
Their absence from "The Z notation" explains why we ended up
with a non-standard syntax for binding displays, since we
had to make one up and the standards committee chose not to
follow our lead (Rob might know why, I think I had left the
committee before that decision).
Proofpower mailing list