3
$\begingroup$

This question already has an answer here:

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?

$\endgroup$

marked as duplicate by Andrej Bauer, Neel Krishnaswami, Damiano Mazza, Kaveh, Yuval Filmus Aug 29 '17 at 11:27

This question has been asked before and already has an answer. If those answers do not fully address your question, please ask a new question.

  • 1
    $\begingroup$ Welcome to TCS StackExchange! This forum is for research level questions on theoretical computer science. You should ask your question on this site. 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? $\endgroup$ – Damiano Mazza Aug 24 '17 at 12:07
  • $\begingroup$ 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. $\endgroup$ – user251130 Aug 24 '17 at 12:48
  • $\begingroup$ 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. $\endgroup$ – Damiano Mazza Aug 24 '17 at 13:15
6
$\begingroup$

Here's a quote from this version 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).

$\endgroup$

Not the answer you're looking for? Browse other questions tagged or ask your own question.