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