7512dcfad1f5baae5b8731beba153d9909de2cbf — Sol 4 months ago 35c797c
wip: renovate PLAN_INFORMAL_SPEC
1 files changed, 18 insertions(+), 5 deletions(-)

M doc/plan/PLAN_INFORMAL_SPEC.txt => doc/plan/PLAN_INFORMAL_SPEC.txt +18 -5
@@ 51,11 51,24 @@ Here are the reduction rules.
    toNat(x:@) = x
    toNat(_)   = 0

    EXEC(e, n:@)     = e[n] or n if n>=len(e)
    EXEC(e, (0 x y)) = (EXEC(x), EXEC(y))
    EXEC(e, (1 v b)) = EXEC(f,b) where f = e ++ [EXEC(f,v)]
    EXEC(e, (2 x))   = x
    EXEC(e, x)       = x
And then, `EXEC` describes how to interpret the code of a law within
the environment of a self-refence and a list of arguments.  `BIND`
sets up the environment, and `RUN` expands legal expressions.

    ;; TODO: This is a rough draft, go through this again, but with much
    ;; more care.

    EXEC(e, b) =
        let (e2, body) = BIND(e2, e, b)
        in RUN(e2, body)

    BIND(e2, e, (1 v b)) = BIND(e2, e++[RUN(e2,v)], b)
    BIND(e2, e, body)    = (e, body)

    RUN(e, n:@)     = e[n] or n if n>=len(e)
    RUN(e, (0 x y)) = (RUN(x), RUN(y))
    RUN(e, (2 x))   = x
    RUN(e, x)       = x

One important detail here, is that nats have infinite arity (formally
arity=0), and so they are never reduced.  Because of this, you can use