Add PLAN opcode explanation

[kjekac]

We show the PLAN data model and the PLAN spec, but it's only in the documentation of sire_01_fan.sire that we explain the opcodes. This seems like it's too deep into the weeds of the docs for something so central to the system, especially when we end the intro of the stdlib with this:

By starting with PLAN and going through all the files above, after a (relatively) small investment of time, you could understand the entirety of this computational model. Pretty cool.

Stretch goal: explain the rules in the spec and explain how they work together to implement the opcodes, probably touching on the lazy semantics and normalization at the same time. (I guess i'll have to do some parts of this, or have a lot of back and forth with Vinney while he does it. Not sure how our time is best invested here.)

[cvanetten]

I have some LLM generated explanations that I've reviewed and edited that explains the rules in the spec. It's very fine-grained, but maybe useful? It will still require a review from you.

Here's an example:

E(o:@)     = o
E(o:<x>)   = o
E(o:(f x)) =  
    E(f)      
    when A(f)=1 
        o <- X(o,o)
        E(o)       
    o              
E(o:{n a b}) =     
    if a!=0 then o else 
        o <- <>         
        o <- R(0,o,b) 
        E(o)

The E() function is responsible for evaluating an expression to its weak head normal form (WHNF). It takes a single parameter o, which represents the expression to be evaluated.

Procedure:

• It checks the type of the input expression o:
• If the type of o is 'hol' (indicating a hole or an undefined value):
• It raises an exception indicating a loop, as evaluating a hole is not allowed.
• If the type of o is 'app' (indicating an application):
• It recursively calls E() on the head of the application (o.head) to evaluate the function to its WHNF.
• It then checks if the arity of the evaluated function (A(o.head)) is equal to 1:
• If the arity is 1, it means the function is saturated (has enough arguments).
• It updates o by calling S(o) to simplify the expression by removing any unnecessary pins in the head of the application.
• It then calls X(o, o) to perform one step of simplification on the saturated expression.
• It updates o with the simplified expression.
• It recursively calls E() on the updated o to continue the evaluation process.
• Finally, it returns the evaluated expression o.

The E() function relies on the A() function to determine the arity of a function, the S() function to simplify the expression by removing unnecessary pins, and the X() function to perform the actual simplification step on a saturated expression.

The evaluation process continues recursively until the expression reaches its WHNF.

[kjekac]

Haha nope. It got some parts right but overall this is dead wrong.

Let's forget about the stretch goal for now. Here's an explanation of the opcodes from PLAN.md:

There are five built-in operations, indicated by the first four natural numbers.

• (0 n a b): Construct a new law: {n a b}

• (1 p l a n x): Pattern match on the value x (is it a pin, a law, an app, or a nat?).

  case x of
      PIN <i>     -> p i
      LAW {n,a,b} -> l n a b
      APP (f x)   -> a f x
      NAT x       -> n x

• (2 z p x): Pattern match on a natural number (is it zero or (n+1)?).

  case x of
      0 -> z
      x -> p (x-1)

• (3 x): Increment a natural number.

• (4 x): Normalize x and construct a new pin <x>.

...And then the challenge is to explain that the language is "split": law bodies are written in an internal "EDSL" which has the following constructs:

Law = Self                -- self-reference
    | Var Nat             -- "reference bound name", but we use indices instead of names
    | Const PLAN          -- produce constant value
    | (Law Law)           -- function application
    | let Law in Law      -- let binding, i.e. add a value to the end of the environment (bindings may self-reference)

Note that you can always drop back into PLAN, either deliberately by using the Const construct, or automatically: whenever a part of a law body doesn't have a meaning in the EDSL, evaluation will fall back to PLAN rules. Conversely you'll switch from PLAN into the EDSL whenever a law has been applied to enough arguments. The two languages depend on each other, but they use separate rules.

The EDSL of law bodies isn't really a separate language, it is embedded within PLAN in the following way: a few of PLAN's native opcodes are used in their partially applied forms (i.e. non-evaluating) in order to encode an AST:

    |---------|--------------------|
    | pattern | meaning            |
    |---------|--------------------|
    | (0 f x) | (f x)              |
    | (1 v b) | let v in b         |
    | (2 k)   | Const k            |
    | 0       | Self               |
    | 1       | var 1              |
    | 2       | var 2              |
    | x       | Const x (fallback) |
    |---------|--------------------|

Verify to yourself that none of these cases reduce, meaning that any valid AST of the EDSL can be stored using this encoding.

[vcavallo]

addressed by #21