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). Roger _______________________________________________ Proofpower mailing list [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
