Krivine in his book (Lambda-calculus: Types and Models) introduces the grammar of lambda-terms and then abbreviations to denote them. The grammar itself is not ambiguous: Lambda-terms are obtained by applying, a finite number of times, the following rules :
- any variable x is a λ-term ;
- whenever t and u are λ-terms, then so is (t)u ;
- whenever t is a λ-term and x is a variable, then λx t is a λ-term.
Then: "the term $(...(((t)u_1)u_2)...)u_k$ will also be written "$(t)u_1 u_2 ...u_k$". But let us consider the two following different $\lambda$-terms:
- $v_1 = ((x)\lambda y. (y)z)w$
- $v_2 = (x)\lambda y. ((y)z)w$
($w, x, y, z$ are variables) and now it seems that I have two ways to interpret the notation $(x)\lambda y. (y)z w$:
either $t = x$, $k = 2$, $u_1 =\lambda y. (y)z$ and $u_2 = w$
or $t = x$, $k= 1$ and $u_1 = \lambda y. ((y)z)w$
It seems that the notation "$(t)u_1 u_2 ...u_k$" is ambiguous. Which rule am I violating in my interpretation?