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)

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.


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)

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

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

ProofPower-Z does allow a predicate in the body of a let expression (an earlier design decision) but def007A has not yet been updated, e.g. it does not appear to permit

     let x %def% 2 %spot% x %mem% S

because it requires parentheses around the body.

Proofpower mailing list

Reply via email to