The Krivine machine explains how to compute a recursive function.
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.
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.
From an abstract point of view, head reduction is the way a program computes when it evaluates a recursive sub-program.
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 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.
The state has three components[2] The term is a λ-term with de Bruijn indices.
[b] This intuitive explanations allow understanding the operating rules of the machine.
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.
This closure corresponds to the de Bruijn index 0 in the new environment.
The transition Succ removes the first closure of the environment list and decreases the value of the index.
[9] [7] (Also, if the reduction strategy is right-to-left call by value and includes generalized
)[10] [7] Content in this edit is translated from the existing French Wikipedia article at fr:Machine de Krivine; see its history for attribution.