This document specifies PLAN, the evaluation model used by Plunder,
by defining a reference interpreter in a custom pseudocode.
You can find a Haskell version here.
PLAN is an acronym. Every PLAN value is either a pin x:<i>, a law
x:{n a b}, an app x:(f g), a nat x:@. (or a hole x:<>).
PLAN evaluation is similar to supercombinator-based graph-reduction
strategy for evaluating the lazy lambda calculus.
- E[x,y] executes the procedure E with parameters x and y.
- Ea means E[a], E(a b) means E[(a b)], Eab means E[a,b], etc.
- (f x y) and "f x y" are a short-hand way to write ((f x) y).
- o#x mutates o in place, updating it's value to equal x.
- x;y indicates sequencing: run x for it's effects, and then return y.
- Unmatched patterns diverge.
- Subtraction on natural numbers is truncating: (3-5) = 0
Evaluation works by performing updates on the graph until it is
in normal form. Fx normalizes the graph x.
Fo = Eo; Go | Cp____<i> = p i
| C_l___{n a b} = l n a b
G(f x) = Gf; Fx | C__a__(f x) = a f x
Go = o | C___z_0 = z
| C____m(x:@) = m (x-1)
E[o:(f x)] = Ef; Ho(Af) |
E[<>] = E[<>] | A(f x) = Af-1
E[o] = o | A{n a b} = a
| A<{n a b}> = a
Ho1 = o#Xoo; Eo | A[n:@] = 0
Hoa = o | A<n:@> = I[1, 6 1 3 1, n]
| A<i> = 1
I[f, e x, 0] = x |
I[f, e, 0] = e | X[f x, e] = Xfe
I[f, e x, n] = I[f, e, n-1] | X[<0>, _ i] = Fi; <i>
I[f, e, n] = f | X[<1>, _ n a b] = Fn; Ea; Fb; {n Na b}
| X[<2>, _ x] = Ex; Nx+1
L[i, n, e, 1 v b] = | X[<3>, _ p l a z m o] = Eo; Cplazmo
Iiei#Rnev; | X[{n a b}, e] = Baaebb
L[i+1, n, e, b] | X[<{n a b}>, e] = Baaebb
Linex = Rnex |
| Baneb(1 _ k) = B[a,n+1,(e <>),b,k]
Rne(b:@) | b<=n = Ine(n-b) | Banebx = Laneb
Rne(0 f x) = (Rnef Rnex) |
Rne(0 x) = x | N[x:@] = x
Rnex = x | N_ = 0