# ¶ The Krivine abstract machine

The Krivine machine is an abstract machine that executes terms of the call-by-name untyped $\lambda \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 \lambda$-calculus.

There are three parts to it:

• λ-calculus terms
• closures
• environments

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

Environments are finite maps from variables to closures:

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

A configuration of the Krivine machine is a triple

$\left(M,E,S\right)\left(M, E, S\right)$

where $MM$ is a term, $EE$ is an environment, and $SS$ is a stack, i.e. a list of closures. We write $S={c}_{1}\cdot \dots \cdot {c}_{n}S = c_1 \cdot \ldots \cdot c_n$ for such a generic such list, and $S=c\cdot {S}^{\mathrm{\prime }}S = c \cdot S\text{'}$ to indicate that $cc$ is the first element of the list, i.e. the top of the stack.

The machine is implemented by the following transitions:

The last clause is only defined whenever $EE$ maps the variable $xx$ to a specific closure $\left(M,{E}^{\mathrm{\prime }}\right)\left(M, E\text{'}\right)$.

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

• $\lambda \lambda$ means pop
• $\left(-\right)-\left(-\right)-$ 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 \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:
• Chicago
• BibTeX
• Krivine, Jean-Louis. 2007. ‘A Call-by-Name Lambda-Calculus Machine’. Higher-Order and Symbolic Computation 20 (3): 199–207. https://doi.org/10.1007/s10990-007-9018-9. pdf

@article{krivine_call-by-name_2007,
title = {A call-by-name lambda-calculus machine},
volume = {20},
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
• Text
• Salvati, Sylvain, and Igor Walukiewicz. Krivine machines and higher-order schemes. Information and Computation, Volume 239, 2014, Pages 340-355. https://doi.org/10.1016/j.ic.2014.07.012.

### ¶

• The relationship to head linear reduction seems to have been first described in the following LICS 1996 article.
• Chicago
• BibTeX
• Danos, V., H. Herbelin, and L. Regnier. 1996. ‘Game Semantics and Abstract Machines’. In Proceedings 11th Annual IEEE Symposium on Logic in Computer Science, 394–405. New Brunswick, NJ, USA: IEEE Comput. Soc. Press. https://doi.org/10.1109/LICS.1996.561456.

@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
• Chicago
• BibTeX
• Danos, Vincent, and Laurent Regnier. 2004. ‘Head Linear Reduction’. [pdf]

@unpublished{danos_2004,
author = {Danos, Vincent and Regnier, Laurent},
year = {2004}
}