THE KRIVINE MACHINE call-by-name: the discarded argument is never run
The smallest machine that runs the lambda calculus — a term, an environment, an argument stack, and three moves (Push an argument, Grab it into a lambda, Access a variable). It is call-by-name: a function’s argument is only evaluated if and when the body demands it, so an argument that is thrown away is never evaluated. And its closures are first-order data records (a de Bruijn index + an environment index), not host-language function values — which is exactly why it ports to a first-order language.
THE TECHNIQUE only evaluate what the body demands
Evaluate (λx.λy. x) A B, where A = 42 and B is an expensive computation. Under call-by-name, the body returns x = A and never touches y = B — so B’s work is never done. Compare with call-by-value, which evaluates B first and then throws it away. Same answer, different work. live demo
HISTORY & CREDIT designed early 1980s, published 2007
“The Krivine machine was invented in 2007” — no; that is only its first formal publication. Krivine designed it in the early 1980s; it circulated unpublished for ~25 years. cited
1964 · Landin’s SECD — the call-by-value machine; Krivine’s is its call-by-name dual (dumpless, far simpler), not its descendant. 1972 · de Bruijn — nameless indices (a variable is the count of binders to its own); the Access rule reads them — not a Krivine invention. early 1980s · Jean-Louis Krivine designs the minimal call-by-name machine — term + argument stack + environment of closures. 1997 / 2003 / 2007 · Sestoft turns call-by-name into call-by-need (lazy, with sharing) via update markers; Ager-Biernacki-Danvy-Midtgaard mechanically derive the machine by CPS + defunctionalization; Krivine finally publishes (HOSC 20(3)).
Call-by-name is not lazy: a discarded argument is skipped (good), but an argument used twice is re-evaluated twice — laziness (call-by-need) adds the sharing. Krivine, early 1980s
RECOMMEND FOR I-13 the closureless machine — a natural fit
Krivine’s closures are first-order data records, not host-language functions; the laziness shows as work not done:
$ i13 run kriv.i13 # (\x.\y. x) 42 (expensive) , expensive = sum 1..20
call-by-name: result 42, expensive forced 0 steps (y is never demanded)
call-by-value: result 42, expensive forced 20 steps (evaluated, then discarded)
Recommend:nothing new — the term is a flat tagged f64 array, the argument stack and environment are arrays with top pointers, and the three moves (Push / Grab / Access) are index arithmetic. Verified: both strategies return 42, but call-by-name does 0 steps on the discarded argument while call-by-value wastes 20. It ports because its closures are first-order data (a term index + an env index), not host-language functions. Note: it is the call-by-name counterpart to SECD (dart 142); adding sharing (call-by-need) is Sestoft’s update markers — and sharing is exactly what graph reduction (dart 145) provides. Full lambda terms want a node arena (PS-015).