<p>One interesting difference shows up in Section 2 "Representable functions" of Chapter 2 of Krivine's book.  Church-encoded three is written in standard notation as <span class="math-container">$\lambda\ x.\ \lambda\ y.\ x\ (x\ (x\ y))$</span>.  With Krivine's notation (if I am finally understanding it correctly!), we would write instead <span class="math-container">$\lambda x\ \lambda y\ (x)(x)(x)y$</span>.  </p>

CC BY-SA 4.0
2019-03-27T21:54:27.660Z
2019-03-27T21:54:27.660Z
Aaron Stump
<p>I'm assuming you mean Krivine's notation from <a href="http://www.pps.univ-paris-diderot.fr/~krivine/articles/Lambda.pdf"><em>Lambda Calculus: Types and Models</em></a>.</p>

<p>This notation, used as a data representation, makes many algorithms on lambda-terms simpler to implement and prove correct. That is, given a  lambda term $f\; e_1\; e_2\; \ldots\; e_n$, you want to view it as a <em>head</em> $f$, together with a <em>list</em> of arguments $[e_1,  e_2, \ldots, e_n]$. </p>

<p>For example, suppose you want to compare two terms $f\;e_1\;\ldots\; e_n$ with $g\;t_1\;\ldots\;t_n$. It is often most natural to compare the heads $f$ and $g$ first, and not even look at the $(e_i, t_i)$ pairs unless that comparison succeeds. (This often comes up in implementations of higher-order unification.) </p>

<p>See Cervesato and Pfenning's paper <a href="http://repository.cmu.edu/cgi/viewcontent.cgi?article=1023&amp;context=compsci"><em>A Linear Spine Calculus</em></a> for a formalization of this idea. </p>

CC BY-SA 3.0
2013-03-07T13:46:21.677Z
2013-03-07T13:46:21.677Z
Neel Krishnaswami
<p>I saw some people uses Krivine's notation for function application when presenting the syntax for the $\lambda$-calculus.  For example, the $\lambda$-term $\lambda f . \lambda x . \lambda y . f\ x\ y$ (with the normal convention that function application associates to the left, so it actually means $\lambda f . \lambda x . \lambda y . ((f\ x)\ y)$) is written $\lambda f . \lambda x . \lambda y . (f)\ x\ y$ (with a similar convention that it actually means $\lambda f . \lambda x . \lambda y . ((f)\ x)\ y$).  I do not see the point of having another pair of parentheses around the innermost $f$.  Why do people use Krivine's notation instead of the usual one?</p>

<lo.logic><lambda-calculus>
What is the benefit of Krivine's notation?
day
# What is the benefit of Krivine's notation?

(Asked by: username_0 on 2013-03-07)

I saw some people uses Krivine's notation for function application when presenting the syntax for the $\lambda$-calculus. For example, the $\lambda$-term $\lambda f . \lambda x . \lambda y . f\ x\ y$ (with the normal convention that function application associates to the left, so it actually means $\lambda f . \lambda x . \lambda y . ((f\ x)\ y)$) is written $\lambda f . \lambda x . \lambda y . (f)\ x\ y$ (with a similar convention that it actually means $\lambda f . \lambda x . \lambda y . ((f)\ x)\ y$). I do not see the point of having another pair of parentheses around the innermost $f$. Why do people use Krivine's notation instead of the usual one?

**Tags:** lo.logic, lambda-calculus


---

## 2 answers

### Answer by username_2 on 2013-03-07. Score: 13 | Accepted answer

I'm assuming you mean Krivine's notation from [*Lambda Calculus: Types and Models*](http://www.pps.univ-paris-diderot.fr/~krivine/articles/Lambda.pdf).

This notation, used as a data representation, makes many algorithms on lambda-terms simpler to implement and prove correct. That is, given a lambda term $f\; e\_1\; e\_2\; \ldots\; e\_n$, you want to view it as a *head* $f$, together with a *list* of arguments $[e\_1, e\_2, \ldots, e\_n]$.

For example, suppose you want to compare two terms $f\;e\_1\;\ldots\; e\_n$ with $g\;t\_1\;\ldots\;t\_n$. It is often most natural to compare the heads $f$ and $g$ first, and not even look at the $(e\_i, t\_i)$ pairs unless that comparison succeeds. (This often comes up in implementations of higher-order unification.)

See Cervesato and Pfenning's paper [*A Linear Spine Calculus*](http://repository.cmu.edu/cgi/viewcontent.cgi?article=1023&context=compsci) for a formalization of this idea.


---

### Answer by username_1 on 2019-03-27. Score: 0

One interesting difference shows up in Section 2 "Representable functions" of Chapter 2 of Krivine's book. Church-encoded three is written in standard notation as $\lambda\ x.\ \lambda\ y.\ x\ (x\ (x\ y))$. With Krivine's notation (if I am finally understanding it correctly!), we would write instead $\lambda x\ \lambda y\ (x)(x)(x)y$.


---

