The Krivine abstract machine

The Krivine machine is an abstract machine that executes terms of the call-by-name untyped \lambda-calculus.

Danos, Herbelin and Regnier 1996 claim that the Krivine abstract machine implements head linear reduction. In Krivine 2007 it is explicitly mentioned that the Krivine machine implements "weak head reduction," which might (or might not) be the same thing.

A simplified version

We demonstrate the Krivine machine on the untyped \lambda-calculus.

There are three parts to it:

• λ-calculus terms
• closures
• environments

These are defined by mutual recursion. Terms are given as usual:

 M, N\ ::=\ x \mid \lambda x.\ M \mid MN

Environments are finite maps from variables to closures:

 E     ::=\ \emptyset \mid E[x \mapsto c]

Finally, closures are pairs of a term and an environment to evaluate it in:

 c\    ::= (M, E)

A configuration of the Krivine machine is a triple

	(M, E, S)

where M is a term, E is an environment, and S is a stack, i.e. a list of closures. We write S = c_1 \cdot \ldots \cdot c_n for such a generic such list, and S = c \cdot S' to indicate that c is the first element of the list, i.e. the top of the stack.

The machine is implemented by the following transitions:

\begin{aligned}
	(\lambda x. M, E, c \cdot S) &\longrightarrow (M, E[x \mapsto c], S) \\
  (MN, E, S) &\longrightarrow (M, E, (N, E) \cdot S) \\
  (x, E, S)    &\longrightarrow (M, E', S) \quad \text{where } (M, E') \simeq E(x)
\end{aligned}

The last clause is only defined whenever E maps the variable x to a specific closure (M, E').

Notice that the operational meaning of term constructors is clear here:

• \lambda means pop
• (-)- means push

Other presentations

There are many variations to the Krivine machine.

The original presentation by Krivine (in an unpublished 1986 manuscript) used doubly-indexed de Bruijn indices. (I believe this is the presentation that survives in Krivine 2007).

Danos and Regnier 2004 present a version based on a single de Bruijn index.

The version given above uses names. In his thesis, Sylvain Lippi shows that this is workable, and does not require any \alpha-conversion Danos and Regnier 2004.

References

• Jean-Louis Krivine designed the machine in the mid-1980s, and an unpublished manuscript was circulated. The details were eventually published in 2007:

@article{krivine_call-by-name_2007,
	title = {A call-by-name lambda-calculus machine},
	volume = {20},
	url = {http://link.springer.com/10.1007/s10990-007-9018-9},
	doi = {10.1007/s10990-007-9018-9},
	number = {3},
	journal = {Higher-Order and Symbolic Computation},
	author = {Krivine, Jean-Louis},
	year = {2007},
	pages = {199--207}
}

• The simplified account given here is derived from

• The relationship to head linear reduction seems to have been first described in the following LICS 1996 article.

@inproceedings{danos_1996,
	address = {New Brunswick, NJ, USA},
	title = {Game semantics and abstract machines},
	doi = {10.1109/LICS.1996.561456},
	booktitle = {Proceedings 11th {Annual} {IEEE} {Symposium} on {Logic} in {Computer} {Science}},
	publisher = {IEEE Comput. Soc. Press},
	author = {Danos, V. and Herbelin, H. and Regnier, L.},
	year = {1996},
	pages = {394--405}
}

• The exact relationship with head linear reduction is described in

@unpublished{danos_2004,
	title = {Head {Linear} {Reduction}},
	url = {http://people.cs.uchicago.edu/~brady/CSPP50102/notes/pam.pdf},
	author = {Danos, Vincent and Regnier, Laurent},
	year = {2004}
}