## ~plan/plunder

a4b2e52408115e73cdb62d29959bea278392ac9a — Sol 1 year, 24 days ago
```Operational semantics for PLAN
```
```1 files changed, 44 insertions(+), 0 deletions(-)

A doc/PLAN_OPERATIONAL.txt
```
`A doc/PLAN_OPERATIONAL.txt => doc/PLAN_OPERATIONAL.txt +44 -0`
```@@ 0,0 1,44 @@
+Every PLAN is a pin x:<i>, a law x:{n a b}, an app x:(f g), a nat x:@,
+or a black hole x:ø.
+
+Run F(x) to normalize a value.
+
+(f x y z) is short-hand for (((f x) y) z)
+
+Implementations may deviate from this evaluation order as long as the
+result is always the same.
+
+E(a) =                                  | H((f x)) = H(f)
+    case a                              | H(x)     = x
+        {n 0 b}                         |
+            a ← ø                       | F(a) =
+            a ← RUN(a,b)                |     E(a)
+            E(a)                        |     if a:(f x)
+        (f x)                           |         F(f); F(x)
+            E(f)                        |     a
+            if A(f)=1                   |
+                a ← X(H(f), a)          | N(a) =
+                E(a)                    |     E(a)
+    a                                   |     if a:@ then a else 0
+                                        |
+X(<p>, e)           = X(p,e)            | I((e x), 0, f) = x
+X({n a b}, e)       = R(e,b)            | I(e,     0, f) = e
+X(0, (_ n a b))     = {N(n) N(a) F(b)}  | I((e x), n, f) = I(e, n-1, f)
+X(1, (_ p l a n x)) = P(p,l,a,n,x)      | I(e,     n, f) = f
+X(2, (_ z p x))     = C(z,p,x)          |
+X(3, (_ x))         = N(x)+1            | A((f x))   = A(f)-1
+X(4, (_ x))         = <F(x)>            | A(<p>)     = A(p)
+                                        | A({n a b}) = a
+P(p,l,a,n,v) =                          | A(n:@)     = I((3 5 3), n, 1)
+    case E(v)                           |
+        (f x)   -> a f x                |
+        <x>     -> p x                  | C(z,p,x) =
+        {n a b} -> l n a b              |     case N(x)
+        x:@     -> n x                  |         0 -> z
+                                        |         n -> p (n-1)
+R(e,b:@)     = I(e,b,b)                 |
+R(e,(0 f x)) = (R(e,f) R(e,x))          | L(e,v,b) =
+R(e,(1 v b)) = L(e,v,b)                 |     x  := ø
+R(e,(2 x))   = x                        |     e2 := (e x)
+R(e,x)       = x                        |     x  <- R(e2, v)
+                                        |     R(e2, b)

```