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.
Phil
_______________________________________________
Proofpower mailing list
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
