On 27/09/11 13:25, Roger Bishop Jones wrote:
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).

I wondered whether the original design intended to map decoration differently for predicates and expressions? Then the user could determine the mapping of e.g. S' as either
  mk_z_schema_pred (S, "'")
  mk_z_schema_pred (mk_z_decor%down%s (S, "'"), "")
by controlling predicate/expression parsing modes as usual. (As Rob points out, the second is always used currently.)

A better answer as to why Z'SchemaPred needs to support decoration is to allow e.g. predicate S' to match with S, for e.g. forward chaining, with such an S' being a valid Z term. (Currently, when a schema predicate is stripped in the subgoal package with the proof context 'z_schemas, any top-level Z'Decor is converted to decoration on the Z'SchemaPred binding variables.)

My suggestion regarding renaming was not about the mapping of Z into HOL but about what Z proof operations could do to avoid "not Z" HOL terms. That is actually a separate issue/discussion. Sorry for the confusion.


Proofpower mailing list

Reply via email to