Krivine machine

In theoretical computer science, the Krivine machine is an abstract machine (sometimes called virtual machine). As an abstract machine, it shares features with Turing machines and the SECD machine. The Krivine machine explains how to compute a recursive function. More specifically it aims to define rigorously head normal form reduction of a lambda term using call-by-name reduction. Thanks to its formalism, it tells in details how a kind of reduction works and sets the theoretical foundation of the operational semantics of functional programming languages. On the other hand, Krivine machine implements call-by-name because it evaluates the body of a β-redex before it applies the body to its parameter. In other words, in an expression (λ x. t) u it evaluates first λ x. t before applying it to u. In functional programming, this would mean that in order to evaluate a function applied to a parameter, it evaluates first the function before applying it to the parameter.

A picture view of a Krivine machine

The Krivine machine was designed by the French logician Jean-Louis Krivine at the beginning of the 1980s.

Call by name and head normal form reduction
Further information: Lambda calculus

The Krivine machine is based on two concepts related to lambda calculus, namely head reduction and call by name.

Head normal form reduction

A redex[1] (one says also β-redex) is a term of the lambda calculus of the form (λ x. t) u. If a term has the shape (λ x. t) u1 ... un it is said to be a head redex. A head normal form is a term of the lambda calculus which is not a head redex.[lower-alpha 1] A head reduction is a (non empty) sequence of contractions of a term which contracts head redexes. A head reduction of a term t (which is supposed not to be in head normal form) is a head reduction which starts from a term t and ends on a head normal form. From an abstract point of view, head reduction is the way a program computes when it evaluates a recursive sub-program. To understand how such a reduction can be implemented is important. One of the aims of the Krivine machine is to propose a process to reduct a term in head normal form and to describe formally this process. Like Turing used an abstract machine to describe formally the notion of algorithm, Krivine used an abstract machine to describe formally the notion of head normal form reduction.

An example

The term ((λ 0) (λ 0)) (λ 0) (which corresponds, if one uses explicit variables, to the term (λx.x) (λy.y) (λz.z)) is not in head normal form because (λ 0) (λ 0) contracts in (λ 0) yielding the head redex (λ 0) (λ 0) which contracts in (λ 0) and which is therefore the head normal form of ((λ 0) (λ 0)) (λ 0). Said otherwise the head normal form contraction is:

((λ 0) (λ 0)) (λ 0) ➝ (λ 0) (λ 0) ➝ λ 0,

which corresponds to :

(λx.x) (λy.y) (λz.z) ➝ (λy.y) (λz.z) ➝ λz.z.

We will see further how the Krivine machine reduces the term ((λ 0) (λ 0)) (λ 0).

Call by name

To implement the head reduction of a term u v which is an application, but which is not a redex, one must reduce the body u to exhibit an abstraction and therefore create a redex with v. When a redex appears, one reduces it. To reduce always the body of an application first is called call by name. The Krivine machine implements call by name.

Description

The presentation of the Krivine machine given here is based on notations of lambda terms that use de Bruijn indices and assumes that the terms of which it computes the head normal forms are closed.[2] It modifies the current state until it cannot do it anymore, in which case it obtains a head normal form. This head normal form represents the result of the computation or yields an error, meaning that the term it started from is not correct. However, it can enter an infinite sequence of transitions, which means that the term it attempts reducing has no head normal form and corresponds to a non terminating computation.

It has been proved that the Krivine machine implements correctly the call by name head normal form reduction in the lambda-calculus. Moreover, the Krivine machine is deterministic, since each pattern of the state corresponds to at most one machine transition.

The state

The state has three components[2]

  1. a term,
  2. a stack,
  3. an environment.

The term is a λ-term with de Bruijn indices. The stack and the environment belong to the same recursive data structure. More precisely, the environment and the stack are lists of pairs <term, environment>, that are called closures. In what follows, the insertion as the head of a list ℓ (stack or environment) of an element a is written a:ℓ, whereas the empty list is written □. The stack is the location where the machine stores the closures that must be evaluated furthermore, whereas the environment is the association between the indices and the closures at a given time during the evaluation. The first element of the environment is the closure associated with the index 0, the second element corresponds to the closure associated with index 1 etc. If the machine has to evaluate an index, it fetches there the pair <term, environment> the closure that yields the term to be evaluated and the environment in which this term must be evaluated.[lower-alpha 2] This intuitive explanations allow understanding the operating rules of the machine. If one writes t for term, p for stack,[lower-alpha 3] and e for environment, the states associated with these three entities will be written t, p, e. The rules explain how the machine transforms a state into another state, after identifying the patterns among the states.

The initial state aims to evaluate a term t, it is the state t,□,□, in which the term is t and the stack and the environment are empty. The final state (in absence of error) is of the form λ t, □, e, in other words, the resulting terms is an abstraction together with its environment and an empty stack.

The transitions

The Krivine machine[2] has four transitions : App, Abs, Zero, Succ.

Transitions of the Krivine machine
Name Before After

App

t u, p, e

t, <u,e>:p, e

Abs

λ t, <u,e'>:p, e

t, p, <u,e'>:e

Zero

0, p, <t, e'>:e

t, p, e'

Succ

n+1, p, <t,e'>:e

n, p, e

The transition App removes the parameter of an application and put it on the stack for further evaluation. The transition Abs removes the λ of the term and pop up the closure from the top of the stack and put it on the top of the environment. This closure corresponds to the de Bruijn index 0 in the new environment. The transition Zero takes the first closure of the environment. The term of this closure becomes the current term and the environment of this closure becomes the current environment. The transition Succ removes the first closure of the environment list and decreases the value of the index.

Two examples

Let us evaluate the term (λ 0 0) (λ 0) which corresponds to the term (λ x. x x) (λ x. x). Let us start with the state (λ 0 0) (λ 0), □, □.

Evaluation of the term (λ 0 0) (λ 0)

(λ 0 0) (λ 0), □, □

λ 0 0, [<λ 0, □>], □

0 0, □, [<λ 0, □>]

0, [<0, <λ 0, □>>], [<λ 0, □>]

λ 0, [<0, <λ 0, □>>], □

0, □, [<0, <λ 0, □>>]

0, □, [<λ 0, □>]

λ 0, □, □

The conclusion is that the head normal form of the term (λ 0 0) (λ 0) is λ 0. This translates with variables in: the head normal form of the term (λ x. x x) (λ x. x) is λ x. x.

Let us evaluate the term ((λ 0) (λ 0)) (λ 0) as shown belown:

Evaluation of ((λ 0) (λ 0)) (λ 0)
((λ 0) (λ 0)) (λ 0), □, □
(λ 0) (λ 0), [<(λ 0), □>], □
(λ 0), [<(λ 0), □>,<(λ 0), □>], □
0, [<(λ 0), □>], [<(λ 0), □>]
λ 0, [<(λ 0), □>], □
0, □, [<(λ 0), □>]
(λ 0), □, □

This confirms the above fact that the normal form of the term ((λ 0) (λ 0)) (λ 0) is (λ 0).

Inter-derivations

The Krivine machine, like the CEK machine, does not only functionally correspond to a meta-circular evaluator, [3] [4] [5] it also syntactically corresponds to the calculus -- a version of Pierre-Louis Curien's calculus of explicit substitutions that is closed under reduction -- with a normal-order reduction strategy. [6] [7] [8]

If the calculus includes generalized reduction (i.e., the nested redex is contracted in one step instead of two), then the syntactically corresponding machine coincides with Jean-Louis Krivine's original machine.[9] [7] (Also, if the reduction strategy is right-to-left call by value and includes generalized reduction, then the syntactically corresponding machine is Xavier Leroy's ZINC abstract machine, which underlies OCaml.)[10] [7]

See also

Notes
  1. If one only deals with closed terms, these terms take the form λ x. t.
  2. Using the concept of closure, one may replace the triple <term,stack, environment>, which defines the state, by a couple <closure,stack>, but this change is cosmetic.
  3. p is for pile, the French word for stack, which we do not want to mix up with s, for state.

References
  1. Barendregt, Hendrik Pieter (1984), The Lambda Calculus: Its Syntax and Semantics, Studies in Logic and the Foundations of Mathematics, vol. 103 (Revised ed.), North Holland, Amsterdam, ISBN 0-444-87508-5, archived from the original on 2004-08-23 Corrections.
  2. Curien, Pierre-Louis (1993). Categorical Combinators, Sequential Algorithms and Functional (2nd ed.). Birkhaüser.
  3. Schmidt, David A. (1980). "State transition machines for lambda-calculus expressions". State transition machines for lambda calculus expressions. Lecture Notes in Computer Science. Vol. 94. Semantics-Directed Compiler Generation, LNCS 94. pp. 415–440. doi:10.1007/3-540-10250-7_32. ISBN 978-3-540-10250-2.
  4. Schmidt, David A. (2007). "State-transition machines, revisited". Higher-Order and Symbolic Computation. 20 (3): 333–335. doi:10.1007/s10990-007-9017-x. S2CID 3012667.
  5. Ager, Mads Sig; Biernacki, Dariusz; Danvy, Olivier; Midtgaard, Jan (2003). "A Functional Correspondence between Evaluators and Abstract Machines". Brics Report Series. 5th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP'03). 10 (13): 8–19. doi:10.7146/brics.v10i13.21783.
  6. Curien, Pierre-Louis (1991). "An Abstract Framework for Environment Machines". Theoretical Computer Science. 82 (2): 389–402. doi:10.1016/0304-3975(91)90230-Y.
  7. Biernacka, Małgorzata; Danvy, Olivier (2007). Article #6. "A Concrete Framework for Environment Machines". ACM Transactions on Computational Logic. 9 (1): 1–30. doi:10.7146/brics.v13i3.21909.
  8. Swierstra, Wouter (2012). "From mathematics to abstract machine: A formal derivation of an executable Krivine machine". Electronic Proceedings in Theoretical Computer Science. Proceedings of the Fourth Workshop on Mathematically Structured Functional Programming (MSFP 2012). 76: 163–177. arXiv:1202.2924. doi:10.4204/EPTCS.76.10. S2CID 14668530.
  9. Krivine, Jean-Louis (2007). "A call-by-name lambda-calculus machine". Higher-Order and Symbolic Computation. 20 (3): 199–207. doi:10.1007/s10990-007-9018-9. S2CID 18158499.
  10. Leroy, Xavier (1990). The ZINC experiment: an economical implementation of the ML language (Technical report). Inria. 117.

Content in this edit is translated from the existing French Wikipedia article at fr:Machine de Krivine; see its history for attribution.

Bibliography
  • Jean-Louis Krivine: A call-by-name lambda-calculus machine. Higher-Order and Symbolic Computation 20(3): 199-207 (2007) archive.
  • Curien, Pierre-Louis (1993). Categorical Combinators, Sequential Algorithms and Functional (2nd ed.). Birkhaüser.
  • Frédéric Lang: Explaining the lazy Krivine machine using explicit substitution and addresses. Higher-Order and Symbolic Computation 20(3): 257-270 (2007) archive.
  • Olivier Danvy (Ed.): Editorial of special issue of Higher-Order and Symbolic Computation on the Krivine machine, vol. 20(3) (2007)
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.