On 28/09/11 13:40, Phil Clayton wrote:
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
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).
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.)
To answer my own question: from what Roger is saying, this must have
been the intention as Z'SchemaPred can only occur in a predicate and
Z'Decor only in an expression.
Phil
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
