Thanks for your comments on the ProofPower-Z scope rules 

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 
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 
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 
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 

Roger Jones


Proofpower mailing list

Reply via email to