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
> expression.

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

Reply via email to