Thanks for your comments on the ProofPower-Z scope rules Phil. I personally believe that the ProofPower position on the scope of variables is preferable to "the" alternative, for reasons I will come to shortly, but I think it possible that in coming to the decision I was partly influenced by a misreading of the passage you quoted from the ZRM.
I thought Spivey was saying that the names bound by the schema declaration could not be used in the declaration. Whereas you read him as saying that they can be used but fall outside the scope of the declaration. Of course he does say explicitly that they fall outside the scope, but that is consistent with the prohibition. In the context of that possible misunderstanding, one may imagine there to be a little scope for discretion in how to deal with a specification which seems to be formally outside the scope of Z. One might then implement the (semantics of) mapping into HOL with a different scope rule and then debate about whether an error report should be raised if the prohibition is violated. I did consider the merits of the two alternatives, and I was then and am now still strongly in favour of the existing behaviour. As to the opportunities for writing obscure specifications, they are ample whichever choice is made, and my opinion was then that the decision should be made not on the basis of bad practice but on the basis of good practice. The only cases of good practice which came to mind in which a variable is used in a declaration which binds it are cases in which the variable is used in a subsequent part of the declaration to the one in which it is bound, In these cases it is often the case that the specification can be made both more concise and more easily understood by allowing the use. I did not think of any examples in which the use of a variable from an outside scope in a declaration which binds it would be a good thing. Another consideration is the effect of the scope rules on proof. This is connected with the way in which the scope rules influence the mapping into HOL (and this is the case even if you are not implementing in HOL). There can be no doubt that I was influenced by the fact that it is much more straighforward to implement the mapping if the predicate implicit in the declaration is in the scope of the bindings. This is reflected in a simpler description of how to obtain the implicit predicate from the declaration, the nub of which is that one simply replaces the colons by membership signs. This effects the proof behaviour, for one then expects that to prove a universally quantified predicate one can just drop the universal quantifier and replace the declaration with is implicit predicate on the LHS of an implication. Of course, if there are name clashes then then there will have to be renamings, but they are at least uniform. If the other scope rule is used, then partial renaming is necessary just to give the implicit predicate, and hence also in any context in which the proof requires the declaration to be eliminated but not the predicate. I too am now curious about how other proof tools handle such situations (there were no others to refer to when ProofPower-Z was being designed). Of course, it was not our intention to invent a new language, but there was no standard then in place, and our success in arguing the merits of our choices while standardisation was in progress was limited. I am interested to know whether you think there are examples in which the ProofPower Z scope implementation is suboptimal which are not themselves undesirable on other grounds. I.e. if contrary to my belief at the time, the scope rule is not consistent with good practice. I don't see that any of your examples are convincing in this respect. Roger Jones _______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
