In ProofPower-Z, the scope of a variable declared in the Decl part of a
SchemaText includes all expressions in the Decl, for example, in
x : E1; y : E2
any free occurrence of x or y in E1 or E2 is the bound x or y.
I recently got caught out by a subtle case whilst systematically
constructing Z terms. I was proving something like
y = 3 ⇒ (∃ [x : ℤ | x = y - 1] ⦁ x = 2)
which is fine. Then a slight variant
y = 3 ⇒ (∃ [x : ℤ | x = y - 1][y / x] ⦁ y = 2)
which isn't provable. Although the schema
[x : ℤ | x = y - 1][y / x]
has a free variable y that is (necessarily) distinct from the schema
component y (even though they are the same type), the free y becomes
bound by its schema component y when appearing in a Decl.
I'm fairly familiar with the ProofPower-Z behaviour but, clearly, not
enough and this issue got me wondering what other Z dialects do about
the scope of variables declared in a declaration.
For Spivey-Z, see last para section 3.4 of ZRM: "the scope never include
the declaration itself: variables may not be used on the right of a
colon...".
For the Z Standard, looking at the semantic relations in section 15, I
believe that the scope never includes the declaration itself. (The
semantic value for a declaration expression is always derived from an M
∈ Model that is not extended with the bindings from the declaration.)
Is that right?
Thinking about the relative merits of the ProofPower-Z behaviour, I can
see that it could perhaps make schemas slightly more succinct but opens
the door to obfuscation, e.g.
∀ i : i .. j ⦁ P
instead of the equivalent
∀ i : ℤ | i ≤ j ⦁ P
and possible confusion due to a bound variable being referenced before
(in a textual sense) it has appeared bound. Is there any particular
reason ProofPower-Z behaves like it does?
Phil
_______________________________________________
Proofpower mailing list
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
