[CZT-Users] Logical operator ambiguity considered harmful

[Rob A. <rd...@le...>]

Section 8.4 of the ISO Z standard points out that logical operators (conjunction, disjunction etc.) can be used both to form predicates and to form expressions. It goes on to claim that  the resulting ambiguity is "benign, as both interpretations have the same precedence, associativity and meaning". Unfortunately, that's only true on an unwarranted assumption about the shapes of parse trees. To see this consider the following two predicates (in e-mail syntax using (* ... *) for comments):

{} = ( %lambda x: %Z @ (  [y: %Z  | x < y] \/ [y:%Z  | y < x] ) )      (*1*)

({} = ( %lambda x: %Z @[y: %Z  | x < y] ) \/  [y:%Z  | y < x]          (*2*)

Predicate 1 has no free variables and contains a schema disjunction. Predicate 2 has both free and bound occurrences of x and y and contains a predicate disjunction.  But predicates 1 and 2 above are just two different ways of resolving the ambiguity in the following construct:

{} = %lambda x: %Z @[y: %Z  | x < y] \/ [y:%Z  | y < x]   (*3*)

According to the ISO standard this ambiguity is benign, i.e., it does not matter how we resolve the ambiguity. But this is not so, even if we ignore the difference in the free variables: as neither of the lambda abstractions can be empty, predicate 1 is false, while predicate 2 is equivalent to the assertion that y < x.

You can cook up similar examples using mu-expressions or using schema quantifications. An experiment with CZT (source at: http://dl.dropbox.com/u/34693999/ambiguity.zed8) shows that it rejects predicate 3 unless x and y are in scope, so it looks like it is taking reading 2.

The required assumption on the shapes of parse trees can be made to hold by doing what ProofPower does and imposing a restriction like the one that Spivey imposes on mu- and lambda-expressions extended to cover schema quantifications. Under this restriction, these constructs are only allowed as expressions when enclosed in brackets.

Regards,

Rob.