7
$\begingroup$

Can someone please point out online resources to learn about Krivine Machine?

My professor briefly touched it while teaching a course in Computer logic. google did not turn up much except some papers which seemed hard to follow. Neither was there anything on it over at Wikipedia.

$\endgroup$
3
  • $\begingroup$ Why don't you ask your professor? $\endgroup$
    – Chris Eagle
    Nov 9, 2012 at 17:37
  • $\begingroup$ because he mentioned he would not be teaching it and instead concentrate on the SECD machine. he just mentioned that if one is interested they could read about Krivines machine as well $\endgroup$
    – Ankit
    Nov 9, 2012 at 17:50
  • $\begingroup$ Found these set of pdf slides at gallium.inria.fr/~xleroy/mpri/2-4/machines.2up.pdf that provide a somewhat decent explanation of Krivine machine $\endgroup$
    – Ankit
    Nov 14, 2012 at 12:24

3 Answers 3

Reset to default
2
$\begingroup$

The Krivine machine (or K-machine) [1] is a simple and natural implementation of the weak-head call-by-name reduction strategy for pure λ-terms. It can be described in just three or four rules with minimal machinery (an environment and a stack). It is an abstract machines for the implementation of functional languages. It has been used in many variants. The paper [2] gives an overview of the Krivine-machine variants.

[1] A call-by-name lambda-calculus machine, J.-L. Krivine.

[2] The Next 700 Krivine Machines, R. Douence, P. Fradet.

$\endgroup$
1
$\begingroup$

I found this paper that explains the Krivine machine and relates it with the call-by-name lambda calculus:

Leonardo Rodríguez, Daniel Fridlender, and Miguel Pagano, "A Certified Extension of the Krivine Machine for a Call-by-Name Higher-Order Imperative Language", http://drops.dagstuhl.de/opus/volltexte/2014/4634/pdf/13.pdf

It defines a call-by-name lambda calculus of closures and then briefly describes the Krivine machine, that appears natural once you understand the calculus of closures. I found it readable and it can complement the very succint description of the Krivine machine in the slides proposed by Ankit. Note that it supposes that you already know what De Bruijn indices are. However the Krivine machine by itself is not very useful, since most programming languages have not call-by-name semantics (Algol 60 was one, and was deemed unusable exactly for this reason). You may therefore want to study the version of the Krivine machine for strict or lazy semantics. The paper above also discusses a Krivine machine for call-by-name with numbers and operations. For strict semantics the typical variant is the Krivine machine with marks on the stack; You can find a description of it at section 3.2 of the ZINC paper:

Xavier Leroy, "The ZINC experiment: An economical implementation of the ML language", http://gallium.inria.fr/~xleroy/publi/ZINC.pdf

$\endgroup$
0
$\begingroup$

The original paper by Jean-Louis Krivine that describes the machine can be found here (PDF):
A call-by-name lambda-calculus machine.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .