Roger,

Thanks for the background and explanation.  I have added responses below.


On 15/04/12 15:21, Roger Bishop Jones wrote:
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.

Regarding Spivey Z, I am reading the second edition ZRM (1998). It could be that the first edition (1992) was stricter, in line with your understanding. (I have no way of finding out.)

Addressing the question of what Spivey and Standard Z allow now, I have tried type checking some examples with Fuzz and CZT for the two dialects, respectively. Both accept the following pathological axiomatic description:

│ e : ℙ ℤ
├────────
│ ∀ e : e ⦁ e < e

and they both reject the following as type incorrect:

│ e : ℙ ℤ
├────
│ ∀ e : {e} ⦁ e < e

which is consistent with my understanding.


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.

For hand-written Z, I cannot think of any examples where it offers any benefit.

It is perhaps worth considering another use of Z though - as an intermediate language, e.g. to capture the semantics of some other notation according to some recursive translation/mapping scheme. In such a scheme that I was working on (to embed another notation), there was extensive use of schemas that contained free variables. (I doubt that this would occur much in hand-written Z.) With the alternative scoping behaviour, the translation scheme can construct such schemas and use them in declarations without needing to adjust for any overlap between the free variables and component names of such a schema.


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

So with the alternative scoping, it seems that additional variable renaming would occur during proof compared with the ProofPower scoping but, presumably, that because the ProofPower scoping ensures that a non-clashing name is used when writing Z in the first place.

As a user, the existing renamings to avoid clashes and the additional "partial renamings" that the alternative scoping would require seem like the same sort of thing. I would have to think more about what the implementation has to do. (I note that the alternative scoping would simplify an implementation by avoiding the need for a double-pass over a declaration for type checking.)


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.

I can't come up with a compelling example where the alternative scoping is advantageous. I don't think my previous point about generation of Z with free variables in schemas is particularly compelling without a good example. Whichever scoping is used, the practical benefits appear marginal, perhaps in favour of the ProofPower behaviour. So, for now, my main reservation is that there is a difference in scoping, rather than the particular choice of scoping.

Phil

_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to