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.

Phil


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
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to