Phil,
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".
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.
>
> 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)
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.
>
> 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. 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.
>
> 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.
See above - this is just an omission from USR005.
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.
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.
Regards,
Rob.
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
