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
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
Proofpower mailing list