![]() | This article includes a list of general references, but it lacks sufficient corresponding inline citations .(January 2024) |
In theoretical computer science, the Krivine machine is an abstract 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.
The Krivine machine was designed by the French logician Jean-Louis Krivine at the beginning of the 1980s.
The Krivine machine is based on two concepts related to lambda calculus, namely head reduction and call by name.
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.
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:
which corresponds to :
We will see further how the Krivine machine reduces the term ((λ 0) (λ 0)) (λ 0).
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.
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 has three components [2]
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 Krivine machine [2] has four transitions : App, Abs, Zero, Succ.
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.
Let us evaluate the term (λ 0 0) (λ 0) which corresponds to the term (λx. xx) (λx. x). Let us start with the state (λ 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. xx) (λx. x) is λx. x.
Let us evaluate the term ((λ 0) (λ 0)) (λ 0) as shown belown:
((λ 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).
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]
Lambda calculus is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. Untyped lambda calculus, the topic of this article, is a universal model of computation that can be used to simulate any Turing machine. It was introduced by the mathematician Alonzo Church in the 1930s as part of his research into the foundations of mathematics. In 1936, Church found a formulation which was logically consistent, and documented it in 1940.
The SECD machine is a highly influential virtual machine and abstract machine intended as a target for functional programming language compilers. The letters stand for Stack, Environment, Control, Dump—the internal registers of the machine. The registers Stack, Control, and Dump point to stacks, and Environment points to an associative array.
Combinatory logic is a notation to eliminate the need for quantified variables in mathematical logic. It was introduced by Moses Schönfinkel and Haskell Curry, and has more recently been used in computer science as a theoretical model of computation and also as a basis for the design of functional programming languages. It is based on combinators, which were introduced by Schönfinkel in 1920 with the idea of providing an analogous way to build up functions—and to remove any mention of variables—particularly in predicate logic. A combinator is a higher-order function that uses only function application and earlier defined combinators to define a result from its arguments.
In lambda calculus, the Church–Rosser theorem states that, when applying reduction rules to terms, the ordering in which the reductions are chosen does not make a difference to the eventual result.
In combinatory logic for computer science, a fixed-point combinator, is a higher-order function that returns some fixed point of its argument function, if one exists.
In programming language theory and proof theory, the Curry–Howard correspondence is the direct relationship between computer programs and mathematical proofs.
Operational semantics is a category of formal programming language semantics in which certain desired properties of a program, such as correctness, safety or security, are verified by constructing proofs from logical statements about its execution and procedures, rather than by attaching mathematical meanings to its terms. Operational semantics are classified in two categories: structural operational semantics formally describe how the individual steps of a computation take place in a computer-based system; by opposition natural semantics describe how the overall results of the executions are obtained. Other approaches to providing a formal semantics of programming languages include axiomatic semantics and denotational semantics.
In mathematical logic and type theory, the λ-cube is a framework introduced by Henk Barendregt to investigate the different dimensions in which the calculus of constructions is a generalization of the simply typed λ-calculus. Each dimension of the cube corresponds to a new kind of dependency between terms and types. Here, "dependency" refers to the capacity of a term or type to bind a term or type. The respective dimensions of the λ-cube correspond to:
In the lambda calculus, a term is in beta normal form if no beta reduction is possible. A term is in beta-eta normal form if neither a beta reduction nor an eta reduction is possible. A term is in head normal form if there is no beta-redex in head position. The normal form of a term, if one exists, is unique. However, a term may have more than one head normal form.
The simply typed lambda calculus, a form of type theory, is a typed interpretation of the lambda calculus with only one type constructor that builds function types. It is the canonical and simplest example of a typed lambda calculus. The simply typed lambda calculus was originally introduced by Alonzo Church in 1940 as an attempt to avoid paradoxical use of the untyped lambda calculus.
In computing, a meta-circular evaluator (MCE) or meta-circular interpreter (MCI) is an interpreter which defines each feature of the interpreted language using a similar facility of the interpreter's host language. For example, interpreting a lambda application may be implemented using function application. Meta-circular evaluation is most prominent in the context of Lisp. A self-interpreter is a meta-circular interpreter where the interpreted language is nearly identical to the host language; the two terms are often used synonymously.
In abstract rewriting, an object is in normal form if it cannot be rewritten any further, i.e. it is irreducible. Depending on the rewriting system, an object may rewrite to several normal forms or none at all. Many properties of rewriting systems relate to normal forms.
In mathematical logic, the de Bruijn index is a tool invented by the Dutch mathematician Nicolaas Govert de Bruijn for representing terms of lambda calculus without naming the bound variables. Terms written using these indices are invariant with respect to α-conversion, so the check for α-equivalence is the same as that for syntactic equality. Each de Bruijn index is a natural number that represents an occurrence of a variable in a λ-term, and denotes the number of binders that are in scope between that occurrence and its corresponding binder. The following are some examples:
In programming language semantics, normalisation by evaluation (NBE) is a method of obtaining the normal form of terms in the λ-calculus by appealing to their denotational semantics. A term is first interpreted into a denotational model of the λ-term structure, and then a canonical (β-normal and η-long) representative is extracted by reifying the denotation. Such an essentially semantic, reduction-free, approach differs from the more traditional syntactic, reduction-based, description of normalisation as reductions in a term rewrite system where β-reductions are allowed deep inside λ-terms.
In the study of denotational semantics of the lambda calculus, Böhm trees, Lévy-Longo trees, and Berarducci trees are tree-like mathematical objects that capture the "meaning" of a term up to some set of "meaningless" terms.
Computable topology is a discipline in mathematics that studies the topological and algebraic structure of computation. Computable topology is not to be confused with algorithmic or computational topology, which studies the application of computation to topology.
In rewriting, a reduction strategy or rewriting strategy is a relation specifying a rewrite for each object or term, compatible with a given reduction relation. Some authors use the term to refer to an evaluation strategy.
Lambda calculus is a formal mathematical system based on lambda abstraction and function application. Two definitions of the language are given here: a standard definition, and a definition using mathematical formulas.
A CEK Machine is an abstract machine invented by Matthias Felleisen and Daniel P. Friedman that implements left-to-right call by value. It is generally implemented as an interpreter for functional programming languages, but can also be used to implement simple imperative programming languages. A state in a CEK machine includes a control statement, environment and continuation. The control statement is the term being evaluated at that moment, the environment is (usually) a map from variable names to values, and the continuation stores another state, or a special halt case. It is a simplified form of another abstract machine called the SECD machine.
In computer science, refocusing is a program transformation used to implement a reduction semantics—i.e., a small-step operational semantics with an explicit representation of the reduction context—more efficiently. It is a step towards implementing a deterministic semantics as a deterministic abstract machine.
Content in this edit is translated from the existing French Wikipedia article at fr:Machine de Krivine; see its history for attribution.