On 25/09/11 10:04, Roger Bishop Jones wrote:
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.
I have just found section 4.3.7 in ZED003 and it appears to say that.
Although the Z'SchemaPred semantic constant enables renaming to be
avoided, Z'SchemaPred HOL terms are "not Z" when the schema components
are decorated inconsistently. So perhaps renaming is useful?
Proofpower mailing list