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
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to