9
$\begingroup$

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?

$\endgroup$
13
$\begingroup$

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.

$\endgroup$
0
$\begingroup$

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$.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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