The Krivine machine is an abstract machine that executes terms of the call-by-name untyped -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.
We demonstrate the Krivine machine on the untyped -calculus.
There are three parts to it:
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
where is a term, is an environment, and is a stack, i.e. a list of closures. We write for such a generic such list, and to indicate that 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 maps the variable to a specific closure .
Notice that the operational meaning of term constructors is clear here:
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 -conversion [Danos and Regnier 2004].
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},
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}
}
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.
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}
}
Danos, Vincent, and Laurent Regnier. 2004. ‘Head Linear Reduction’. [pdf]
@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}
}