On 16/07/11 16:02, Rob Arthan wrote:
On 15 Jul 2011, at 15:29, Phil Clayton wrote:

I was going to leave this issue for now but I bumped into it again
today, so I've had a look into it. (It's not something that is holding
me up, just forcing me to put in parentheses where I don't want to!)

This issue was originally noticed because the following term prints
back without parentheses around the body of the lambda expression:

%SZT% %lambda% x : X
%spot% (%exists% [y : Y | p y]
%spot% [x : X; y : Y | q x y]) %>%; (1)

I.e., (for those who don't have the time to parse this in and pick it
apart), you have a lambda abstraction whose body is a schema expression
formed using the schema existential quantifier.

Consequently, the printed term does not re-parse. (Similarly for a mu
expression but let-expressions are ok.) In the printer module imp064,
it looks like parentheses would get inserted in (1): the precedence
for lambda and mu expressions is set to pc_expr0_%lambda%_%mu%_let.
However, the function do_binder_aux overrides the precedence with
PcLowest, inhibiting the parentheses. (Note pc_expr0_%lambda%_%mu%_let
is not used for let expressions, although its name suggests it is.)

Now, I think the issue is with the parser and parentheses should not
be required in (1) The definition of ProofPower-Z in usr005 (def007A)
appears to say that parentheses are not required: for non-terminal
Expr0, Expr in the lambda expression can be Schema.

A possible fix is to update the grammar in dtd061 by moving lambda and
mu expressions along side the current let/quantification expressions.
However, in doing this, I've noticed discrepancies between the syntax
in def007A and the grammar, so I'm not really sure whether this is ok.
See below.

To help the uninitiated, when Phil writes def007A he is referring to the
description of the ProofPower-Z language in part II of the manual USR005
"ProofPower Description".

Yes, def0070A.doc is the source file providing that part of USR005.

USR005 is just plain wrong about let-expressions/let-predicates. It
should do for them what it does for quantifiers, i.e., they should
appear twice: once as as a form of expression and once as a form of
predicate (as an extra alternative for Pred1) - the existing
disambiguation rules in section 6.4.14 of USR005 serve to resolve the
resulting ambiguity. This is what the parser implements for
let-expressions and let-predicates.


def007A allows a predicate as the body of a lambda expression but it
must be enclosed in parentheses as follows:

%lambda% x : X %spot% (x %mem% S)

Note that this example is not ISO Z, because it is not first order. An
analogous example that is standard Z is when the thing inside the
brackets is a schema-expression as in your original example above.

This was deliberately non-Standard because I thought a schema quantifier is already allowed without parentheses in the body by USR005 (because Expr can be Schema, even with the fix below). (In Spivey, Expression can be Schema-Ref.)

However, the current implementation in dtd061 doesn't require the
parentheses, which seems to contradict def007A:

%lambda% x : X %spot% x %mem% S (* ok *)

USR005 (or def007A as you keep calling it) appears to have been trying
to follow Spivey Z here. Unfortunately it contains a very significant
typo: when it defines Expr = Expr0, it should say Expr = Expr1. With
this correction, USR005 is trying to give the same effect as Spivey
whereby lambda-, mu- and let-expressions have to appear in brackets.

Presumably Expr4 would be updated accordingly (by separating the singleton tuple case to allow Expr0 in a parenthesized expression). It might be worth considering allowing Expr0 in other lowest-precedence contexts such as tuple/set/sequence display elements and 'inner' template arguments (as Spivey hardwires for the relational image set).

Somewhat to my surprise the Spivey rules require the brackets even after
the bullet in another lambda-, mu or let-expression. I.e., you can't
omit the brackets from:

let inc == 1 in (\lamda a : Z @ a + inc)

The ProofPower-Z parser corrects what I just consider to be errors in
USR005 and in Spivey's grammar: the symbol after the bullet in a
lambda-, mu- and let-expression should be Expr0 and not Expr.

That seems a sensible change to Spivey.

Now bearing in mind that the thing after the bullet in a lambda- and
mu-expression can sensibly be a schema-expression (even in first-order
ISO Z), it would make sense to allow arbitrary schema expressions
without brackets. This would amount to changing the symbol after the
bullet in USR005 from Expr to Schema. Here are two completely different
Z predicates.

val pred1 = %SZT%{} = (%fn%x: %bbZ%%spot% ([y: %bbZ% | x < y] %or% [y:
%bbZ% | y > x]))%>%;
val pred2 = %SZT%{} = (%fn%x: %bbZ%%spot% [y: %bbZ% | x < y]) %or% [y:
%bbZ% | y > x]%>%;

pred1 has no free variables while x and y appear free in pred2. pred1 is
the false assertion that the function mapping an integer x to the set of
bindings (y == y) where y <> x is empty. pred2 is equivalent to the
potentially true assertion that y is greater than x. ISO Z appears to
allow all the brackets to be omitted from pred1 and pred2, which is a
little unfortunate.

For Standard Z I think it's just a case of knowing the precedences which seem to be the sensible choice: function construction binds tighter than relational operator application which binds tighter than logical operators. So e.g.

  lambda x : X @ f x < y

would never have a predicate after the spot (@) and

  x < y \/ y < x

has the obvious meaning.

However, this would be a case where style guidelines should suggest parentheses.

On the whole, I think I would rather stick with the implemented
ProofPower-Z grammar, correct its description in USR005 and treat your
problem as a pretty-printer issue.

Thanks - I know what to expect.

While you are updating USR005, I noticed a few minor discrepancies that could usefully be fixed:
  - %not%%down%s is not mentioned
  - %exists%%down%1%down%s is not in reserved identifiers list (6.4)
  - Quotation occurs in Expr4 twice


Proofpower mailing list

Reply via email to