On Saturday 24 Sep 2011 22:53, Roger Bishop Jones wrote:
> On Saturday 24 Sep 2011 13:09, Rob Arthan wrote:
> > The quick answer is no - the term generator
> > (imp063.doc) never calls mk_z_schema_pred with
> > non-empty decoration. I need to remind myself exactly
> > what the decoration in mk_z_schema_pred is for (I know
> > what the semantics is intended to be but I can't
> > recall why we have it). Perhaps Roger can cast his
> > mind back to this.
> My memory is pretty bad on the history.
> I expect that I started out with the syntax in Spivey's
> "The Z Notation" (It was the only game in town at the
> time). But then you might expect to see "gen actuals"
> and "renaming!" there.

A better answer is as follows.

We were making the Spivey syntax more "orthogonal" by 
allowing schema expressions in places where only schemas 
were previously allowed, and in that context there was no 
benefit in putting actual parameters or renamings into the 
predication operation, since they could be implemented 
using the normal schema expression operations.

However, decoration is another matter.
Decoration during schema-predication requires only that the 
free variables in the covert theta term be decorated.
Decorating the schema(expression) is a more horrible 
operation and is unnecessary.
So the parameter would enable a more efficient mapping of the 
Z into HOL, if it had actually been used!
Presumably the implementation (of z_schema_pred) does just 
decorate the theta term not the schema expression.


Proofpower mailing list

Reply via email to