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

Reply via email to