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. Roger _______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
