3
$\begingroup$

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?

Improve this question
$\endgroup$
3
  • 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, 2017 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, 2017 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, 2017 at 13:15

1 Answer 1

Reset to default
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).

Improve this answer
$\endgroup$

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