On 20/04/12 11:19, Rob Arthan wrote:


A == 1 .. 10

S ^= [A : A x A | (_+_)A<  10]


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.

Whilst horizontal schemas are not closed under normalization, we can write

  [A' : A × A | (_ + _) A' < 10][A / A']

so at least schemas are closed. For practical purposes, that seems sufficient.

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.

Yes, another headache for teachers and students.


Proofpower mailing list

Reply via email to