From a4b2e52408115e73cdb62d29959bea278392ac9a Mon Sep 17 00:00:00 2001 From: Sol Date: Thu, 13 Jul 2023 14:50:51 -0400 Subject: [PATCH] Operational semantics for PLAN --- doc/PLAN_OPERATIONAL.txt | 44 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 44 insertions(+) create mode 100644 doc/PLAN_OPERATIONAL.txt diff --git a/doc/PLAN_OPERATIONAL.txt b/doc/PLAN_OPERATIONAL.txt new file mode 100644 index 0000000..fe77661 --- /dev/null +++ b/doc/PLAN_OPERATIONAL.txt @@ -0,0 +1,44 @@ +Every PLAN is a pin x:, 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(

, 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)) = | A(

) = 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 | + -> 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) -- 2.45.2