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?
$\begingroup$
$\endgroup$
Add a comment
|
2 Answers
$\begingroup$
$\endgroup$
0
I'm assuming you mean Krivine's notation from Lambda Calculus: Types and Models.
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 for a formalization of this idea.
answered Mar 7, 2013 at 13:46
$\begingroup$
$\endgroup$
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$.
