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:

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.