The Turing machine model gives a simple, incremental method for computing. Given is a set of states and transition rules, and update requires inspecting the current tape value and then following the corresponding state transition. These steps are completely "local." Here I will describe an elegant method with similar properties, the Krivine machine, for evaluating the lambda calculus:
-- Natural Numbers data N = O | S N deriving (Show, Eq) -- Reference, Abstraction, Application data E = R N | Abs E | App E E deriving (Show, Eq) data Pair = Pair E [Pair] deriving (Show, Eq) -- The machine's state: (Expression, Argument stack, Context) type S = (E, [Pair], [Pair]) -- performs a single reduction step -- returns Nothing to signal completion kr :: S -> Maybe S kr (Abs b, (v : s), c) = Just (b, s, v : c) kr (App f x, s, c) = Just (f, Pair x c : s, c) kr (R O, s, (Pair v c : _)) = Just (v, s, c) kr (R (S n), s, _ : c) = Just (R n, s, c) kr (Abs b, _, _) = Nothing fix :: (a -> Maybe a) -> a -> a fix f x = maybe x (fix f) (f x) reduce :: E -> E reduce t = let (t', _, _) = fix kr (t, , ) in t'
Some things to note:
App interact through the argument stack, and how name evaluation pops from the context stack using the De Bruijn convention.
Evaluation strategy is call by name. Termination occurs at weak head normal form.
Closures are created around arguments rather than partial lambda applications.
No special work is needed to avoid name capture.
It was created originally to evaluate programs derived from mathematical proofs. Its simplicity lends itself both to formal reasoning and also to extension with other axioms, such as call/cc to model classical logic, and with alternate evaluation strategies.