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
