Re: [ProofPower] Writing Z schema predicates with decorations
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.) 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. Phil ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Writing Z schema predicates with decorations
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
Re: [ProofPower] Writing Z schema predicates with decorations
On Wednesday 28 Sep 2011 13:52, Phil Clayton wrote: 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. The rationale is specific to schemas as predicates, in other contexts I don't see how to avoid decorating the schema. I see that the account I gave is pretty much the same as what Spivey says about decoration of schemas as predicates on page 72 of the second edition of The Z notation. He gives the expansion as decorated theta term isin schema (not in words of course) and I guess we decided to go straight to the explicit binding display because we knew we had to have those things and might as well go straight there, whereas Spivey seemed content to do without them. Their absence from The Z notation explains why we ended up with a non-standard syntax for binding displays, since we had to make one up and the standards committee chose not to follow our lead (Rob might know why, I think I had left the committee before that decision). Roger ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Writing Z schema predicates with decorations
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
Re: [ProofPower] Writing Z schema predicates with decorations
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. Roger ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Writing Z schema predicates with decorations
My guess would be that a non-empty decoration is possible for Z'SchemaPred to allow for variable decoration during proof operations: if all variables in the characteristic binding are consistently decorated, the resulting term is still Z. However, not all Z proof operations consistently decorate the variables in the characteristic binding, so the semantic constant Z'SchemaPred is exposed fairly often. (This could be avoided with schema renaming as already done recently.) Phil On 24/09/11 13:09, Rob Arthan wrote: Phil, On 17 Sep 2011, at 15:06, Phil Clayton wrote: Using the subgoal package, I have just been trying to quote an assumption (as a term quotation) but couldn't. On the assumption term, dest_z_term returns the form ZSchemaPred (..., ') Given, e.g. (* S : P [a, b : Z] *) val S = %SZT% S %bigcolon% %bbP% [a, b : %bbZ%] %%; is there a way to write a Z term quotation equal to tm1 as follows: val tm1 = mk_z_schema_pred (S, '); ? (I can do so in HOL using Z'SchemaPred directly.) 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. This reminds me that I always meant to make the Z specifications of the Z to HOL mapping available. As a quick fix, I have put the documents here: http://dl.dropbox.com/u/34693999/zed002.pdf http://dl.dropbox.com/u/34693999/zed003.pdf http://dl.dropbox.com/u/34693999/zed005.pdf I will make sure they typecheck presently and include them in the doc directory in future builds. Regards, Rob. ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Writing Z schema predicates with decorations
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? Phil ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Writing Z schema predicates with decorations
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. To unravel it one would need to look at the very early editions of the specification. Do the SCCS files have the full history in them? This reminds me that I always meant to make the Z specifications of the Z to HOL mapping available. As a quick fix, I have put the documents here: http://dl.dropbox.com/u/34693999/zed002.pdf http://dl.dropbox.com/u/34693999/zed003.pdf http://dl.dropbox.com/u/34693999/zed005.pdf I will make sure they typecheck presently and include them in the doc directory in future builds. FIrst time I clicked on those links it worked OK but every subsequent attempt to access the documents has come up with something Acrobat could not process. Roger ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
