On 15 Apr 2012, at 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.
Alas, I am fairly confident that Phil's reading was Spivey's intention. Fuzz allows monsters like: A == 1 .. 10 S ^= [A : A x A | (_+_)A < 10] I endorse your view that this is a bad thing and that the ProofPower way is better. > ... > Another consideration is the effect of the scope rules on > proof. > And as so often, language decisions that are bad for proof are often bad for pedagogical and other reasons too. In this case, it stops the language being closed under certain desirable transformations. In particular, the standard account of how to normalise a schema fails. If you try to normalise S, you get the ill-typed schema [A : Z x Z | A in A x A /\ (_+_) A < 10]. In this example, you can expand the definition of A, but if A were loosely specified, I don't see any clean way of describing the normalised version. GIven its provenance in academia, it amazes me how many design decisions in Z make it harder to teach, typically, as here, by making useful rules of thumb fail to work in edge cases. Regards, Rob. _______________________________________________ Proofpower mailing list [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
