💾 Archived View for dcreager.net › swanson › formalism.gmi captured on 2024-06-16 at 12:29:19. Gemini links have been rewritten to link to archived content

-=-=-=-=-=-=-

Swanson formalism

2022-07-12

Starting a formal description of the Swanson execution model.

n                           [names]

v ≜ κ | ρ | c               [values]
κ                           [constants]
ρ                           [primitive values]
c ≜ (Γ) b̂                   [closure]

Constants can be created from S₀. Primitive values can only be created via builtins. (Old atoms are an example of primitive values; old literals are an example of constants.)

A closure consists of an environment (the “closed over” set) and a list of named branches.

Γ ≜ ε | Γ, n ↦ v            [environment]

An environment is a collection of named values. Might want to change this to a set representation since we don't care about ordering, and because there cannot be duplicate names in an environment.

s ≜ nD ← ∘κ                 [create constant]
  | nD ← (n̂) b̂              [create closure]
  | nD ← ~nS                [rename]

There are three kinds of statement, all of which create a new value in the current environment named ‘nD’. You can create a new constant, a new closure, or rename an existing value.

t ≜ ⇒ nB                    [invoke primitive]
  | → nT nB                 [invoke closure]

There are two kinds of terminal statement, each of which pass control to some other part of code. In both cases, you must provide the name of a branch to invoke (‘nB’). When invoking a closure, you also specify the name of a value in the environment (‘nT’). This value must exist, and is consumed (i.e. removed from the environment) before passing control.

b ≜ nB (n̂) ŝ t              [branch]

A branch is named (‘nB’), and consists of a receiving set (‘n̂’), a list of statements, and exactly one terminal statement.

ξ ≜ Γi → (Γo, c, nB)        [builtin]

A builtin is a function that takes in an input environment (‘Γi’) and returns an output environment (‘Γo’) and a continuation (closure+branch) to pass control back to.