On 20/04/12 18:48, Phil Clayton wrote:
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']
Oops, that should have been
[A' : ℤ × ℤ | A' ∈ A × A ∧ (_ + _) A' < 10][A / A']
so at least schemas are closed. For practical purposes, that seems
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