<p>Here's a quote from <a href="https://www.irif.fr/~krivine/articles/Lambda.pdf" rel="noreferrer">this version</a> which can be found on the author's page (emphasis mine):</p>

<blockquote>
  <p>The term $(t)u$ should be thought of as “$t$ applied to $u$” ; it will also be denoted by $t u$ <strong>if there is no ambiguity</strong> ; the term $(\dots (((t)u_1)u_2)\dots)u_k$ will also be written $(t)u_1u_2\dots u_k$ or $tu_1u_2\dots u_k$. Thus, for example, $(t)uv$, $(tu)v$ and $tuv$ denote the same term.</p>
</blockquote>

<p>I'd expect the "if there is no ambiguity" condition to also apply to the second notation (which is just the first notation applied $k-1$ times).</p>

CC BY-SA 3.0
2017-08-24T02:29:37.337Z
2017-08-24T02:36:26.793Z
2017-08-24T02:36:26.793Z
xavierm02
<p>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 :</p>

<ul>
<li>any variable x is a λ-term ;</li>
<li>whenever t and u are λ-terms, then so is (t)u ;</li>
<li>whenever t is a λ-term and x is a variable, then λx t is a λ-term.</li>
</ul>

<p>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:</p>

<ul>
<li>$v_1 = ((x)\lambda y. (y)z)w$ </li>
<li>$v_2 = (x)\lambda y. ((y)z)w$</li>
</ul>

<p>($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$:</p>

<ul>
<li><p>either $t = x$, $k = 2$, $u_1 =\lambda y. (y)z$ and $u_2 = w$</p></li>
<li><p>or $t = x$, $k= 1$ and $u_1 = \lambda y. ((y)z)w$</p></li>
</ul>

<p>It seems that the notation "$(t)u_1 u_2 ...u_k$" is ambiguous. Which rule am I violating in my interpretation?</p>

CC BY-SA 3.0
2017-08-24T12:07:19.017Z
Welcome to TCS StackExchange!  This forum is for *research level* questions on theoretical computer science.  You should ask your question on [this site](https://cs.stackexchange.com/).  Anyhow, you're not violating any rule, Krivine's notation is non-ambiguous but the abbreviation may be ambiguous when we spell out all terms.  Why does this surprise you?
Damiano Mazza
CC BY-SA 3.0
2017-08-24T12:48:09.270Z
I am sorry if my question was not addressed to the right site. I think that generally it does not make any sense to introduce a notation that might denote two different objects. So, either one of my interpretations is not correct (i.e. $(x)\lambda y. (y) z w$ denotes only $v_1$ or denotes only $v_2$) or, as xavierm02 answered, we are not allowed to use this notation in such a case.
user251130
CC BY-SA 3.0
2017-08-24T13:15:21.927Z
Yes, it's like xavierm02 says: in this case, suppressing parentheses leads to an ambiguity, so you cannot suppress them.  In general, however, this kind of notations are introduced to write more succintly terms in which there are several metavariables denoting subterms.  So, with your notations, $v_1$ is of the form $(x)u_1u_2$ and $v_2$ is of the form $xu_1$, there is no ambiguity as long as we know what $u_1$ (and $u_2$) are.
Damiano Mazza
<lambda-calculus>
Krivine's notation for lambda-terms
user251130
# Krivine's notation for lambda-terms

(Asked by: username_0 on 2017-08-23)

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?

**Tags:** lambda-calculus

> **Comments:**
> **username_1**: Welcome to TCS StackExchange!  This forum is for *research level* questions on theoretical computer science.  You should ask your question on [this site](https://cs.stackexchange.com/).  Anyhow, you're not violating any rule, Krivine's notation is non-ambiguous but the abbreviation may be ambiguous when we spell out all terms.  Why does this surprise you?  
> **username_0**: I am sorry if my question was not addressed to the right site. I think that generally it does not make any sense to introduce a notation that might denote two different objects. So, either one of my interpretations is not correct (i.e. $(x)\lambda y. (y) z w$ denotes only $v_1$ or denotes only $v_2$) or, as username_2 answered, we are not allowed to use this notation in such a case.  
> **username_1**: Yes, it's like username_2 says: in this case, suppressing parentheses leads to an ambiguity, so you cannot suppress them.  In general, however, this kind of notations are introduced to write more succintly terms in which there are several metavariables denoting subterms.  So, with your notations, $v_1$ is of the form $(x)u_1u_2$ and $v_2$ is of the form $xu_1$, there is no ambiguity as long as we know what $u_1$ (and $u_2$) are.  

---

## 1 answers

### Answer by username_2 on 2017-08-24. Score: 6 | Accepted answer

Here's a quote from [this version](https://www.irif.fr/~krivine/articles/Lambda.pdf) which can be found on the author's page (emphasis mine):

> The term $(t)u$ should be thought of as “$t$ applied to $u$” ; it will also be denoted by $t u$ **if there is no ambiguity** ; the term $(\dots (((t)u\_1)u\_2)\dots)u\_k$ will also be written $(t)u\_1u\_2\dots u\_k$ or $tu\_1u\_2\dots u\_k$. Thus, for example, $(t)uv$, $(tu)v$ and $tuv$ denote the same term.

I'd expect the "if there is no ambiguity" condition to also apply to the second notation (which is just the first notation applied $k-1$ times).


---

