(λ x. + x x) (add1 2)
Christopher Wadsworth's 71 thesis is credited. David Turner looks at a FP program without free variables. We can convert any term to a small set of combinations and define a machine based on those combinatord.
S, K, Y combinators:
(((S f) g) x) = (f x) (g x) K x y = x I x = x (λ x. add1 x) 2 S (λ x. add1) (λ x. x) 2 ; introduce S S (K add1) I 2
Avoid manually stepping and looking at each node.
We have a graph and a heap:
Problems with representing programs with these three combinators:
In early 1980s there were two hardware implementations of this.
Take a term, break it down into those "super combinators," and run those.
Super Combinator: combinator; no free variables; abstraction; inside the body, any abstractions are also super combinators.
λ x. (λ y. (+ x y) x) 2
Not a super combinator. x is free in + x y
(λ x. ((λ w λ y . + w y) x x) 2)
Super combinator: (λ w λ y . + w y)
[P w y = + w y], (λ x . P x x) 2 Main := (λ x . P x x) [Main x = P x x] λ x1 ... λ xn . E E != λ t in E λ => Super Combinator
Define a machine with stack, graph, control, and dump
Linear sequence of instructions that does the work of a super combinator. At start, stack has pointer to root, w, and y.
DEF GLOBAL P2 PUSHG + PUSH 1 ;; 1 is w MKAP PUSH 2 ;; 2 is y MKAP UPDATE d UNWIND
Creating nodes, but need to overwrite root with the result of the reduction.
Given some sequence of applications, how do we know which is the root of the reductions? Which to overwrite? At start, we're given a pointer to root.
Unwind moves back up and picks up the args.