On Sunday 25 Sep 2011 16:20, Phil Clayton wrote:

> 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?

I'm sure it is.

But I doubt that it is sensible in the mapping of a 
decorated schema reference.
In this case the same decoration is applied to all 

As to the merits of the design of z_schema_pred, it seems to 
me that the mapping is not only simpler but works more as 
one would expect if a decorated schema reference uses the 
decoration parameter as intended.

In that case, simply rewriting with the definition of 
Z'SchemaPred (which is just membership) yields the statement 
that the binding with decorated variable names (but 
undecorated component names) is a member of the schema 
This is as close as you get to asserting that the decorated 
theta term is a member of the schema (which might possibly 
have been even better in some ways, though less "efficient").

My guess is that it probably was done that way in the 
prototype embedding of Z into the prototype ICL HOL (I did 
the specifications and explained them to Geoff Scullard who 
implemented them), but that when this was all re-implemented 
for the "product version", the implementation fell out 
without using it (I don't think either Geoff or myself had 
much involvement at that stage, so the reason for using it 
got lost).


Proofpower mailing list

Reply via email to