Imported from heikowagner/nela-lang (.github/skills/nela-foundations/SKILL.md). Install upstream with npx skills add heikowagner/nela-lang --skill nela-foundations. Copyright stays with the author.

NELA Mathematical Foundations

ORIENTATION — READ FIRST. Despite the word "Automaton" in the name, NELA is not an automata-theory language. The name is historical (kept for brand continuity). The actual computational model is Interaction Net theory (Lafont, 1990): local graph rewriting over typed nodes.

Theory priority (read the parts below in this order):

Priority	Part	Theory	Role in NELA
1	Part 1	Interaction Nets	The computation model. Every NELA-C program IS an interaction net.
2	Part 2	Linear Logic	Resource semantics. Types are LL formulas. Cut elimination = reduction.
3	Part 3	Dependent Type Theory	Programs = proofs. Ill-typed nets are unrepresentable.
4	Part 4	Von Neumann CA	Historical ancestor. Contributed locality + quiescence metaphors only.

When extending the language: use Parts 1–3. Do not reach for CA concepts. If Parts 1–3 and Part 4 conflict, Parts 1–3 win.

Critical Architecture Decision: Two-Layer Design

Lesson from implementation (v0.1 → v0.2): Hand-writing interaction nets at the Lam/App/Dup/Fix grain is NOT the right surface language for LLMs. Quicksort required 17 nodes and 24 wired edges vs. 4 lines in Python — worse, not better, for LLM comprehension. The v0.1 runtime produced zero reductions because principal-port wiring conventions were ambiguous at that grain.

The correct design is a two-layer architecture:

Layer	Name	What LLMs do	Representation
Surface	NELA-S	Read, write, reason	ML/Haskell-like syntax (.nela files); parsed to typed expression DAG
Core	NELA-C	Never touch directly	Interaction net graph

LLMs write NELA-S. A compiler lowers NELA-S → NELA-C for formal verification and optimal parallel execution. The interaction net layer is the semantic foundation, not the working medium. This is the same relation as: Haskell → GHC Core → STG → machine code.

NELA Surface Language (NELA-S) — What LLMs Write

A NELA-S program is an ML/Haskell-like source file (.nela). nela_parser.py parses it into the typed expression DAG dict consumed by the runtime.

• One or more def name param ... = body forms
• Each body is an Expr (see grammar below)

Expr grammar (ML/Haskell-like surface form)

-- Program
def name param ... = body

-- Expr
INT | name                          -- literals / variables
(-INT)                              -- negative literal in arg position
[]                                  -- nil
[a, b, c]                           -- list literal (sugar for a :: b :: c :: [])
e :: e                              -- cons (right-associative)
e ++ e                              -- append
(e, e)                              -- pair
[x <- list | pred]                  -- list comprehension (filter)
match e | pat = body | pat = body   -- exhaustive pattern match
let x = e in body                   -- local binding
let (a, b) = e in body              -- tuple destructuring
if e then e else e                  -- conditional
e + e | e - e | e * e | e / e | e % e  -- arithmetic (/ = int div, % = mod)
-e                                  -- unary negation
e == e | e < e | e <= e | e > e | e >= e  -- comparison
e && e | e || e | not e             -- boolean
f e e ...                           -- function application

-- Pattern (inside match cases)
[]             -- nil
[h]            -- singleton
h :: t         -- cons
h :: h2 :: t   -- nested cons (3-spine)
(p1, p2)       -- tuple decomposition
_              -- wildcard
name           -- catch-all variable

Runtime dict ops (for reference / compiler output)

Expr :=
  | {"op": "var",    "n": name}                                 -- variable
  | {"op": "int",    "v": number}                               -- integer literal
  | {"op": "bool",   "v": bool}                                 -- boolean literal
  | {"op": "nil"}                                               -- empty list  []
  | {"op": "cons",   "head": Expr, "tail": Expr}                -- list cons  x : xs
  | {"op": "match",  "e": Expr, "cases": [Case]}                -- exhaustive pattern match
  | {"op": "call",   "fn": name, "a": [Expr]}                   -- call (single or multi-arg; recursive ok)
  | {"op": "let",    "x": name, "e": Expr, "in": Expr}          -- local binding
  | {"op": "if",     "cond": Expr, "then": Expr, "else_": Expr} -- conditional
  -- Pair ADT  (return two values from a single function)
  | {"op": "pair",   "l": Expr, "r": Expr}                      -- construct (a, b)
  | {"op": "fst",    "e": Expr}                                 -- project first
  | {"op": "snd",    "e": Expr}                                 -- project second
  -- List accessors
  | {"op": "head",   "e": Expr}                                 -- unsafe head (non-empty only)
  | {"op": "tail",   "e": Expr}                                 -- unsafe tail
  | {"op": "take",   "n": Expr, "e": Expr}                      -- first n elements
  | {"op": "drop",   "n": Expr, "e": Expr}                      -- drop first n
  -- Arithmetic & comparison
  | {"op": "add"|"sub"|"mul"|"div"|"mod", "l": Expr, "r": Expr}
    -- div = integer division, mod = remainder
  | {"op": "neg", "e": Expr}                                    -- unary negation (-e)
  | {"op": "eq"|"lt"|"le"|"gt"|"ge", "l": Expr, "r": Expr}
  -- Boolean combinators
  | {"op": "and"|"or", "l": Expr, "r": Expr}
  | {"op": "not",    "e": Expr}
  -- List combinators (prefer over hand-written recursion where applicable)
  | {"op": "append", "l": Expr, "r": Expr}                      -- list concat (++)
  | {"op": "filter", "pred": str, "pivot": Expr, "list": Expr}  -- [x <- list | pred pivot]

Token cost comparison (quicksort)

Part 1 — Interaction Nets (Lafont, 1990/1997)

This is the primary theory of NELA. Every NELA-C program is an interaction net. Strong confluence = free parallelism. 3 combinators are Turing-complete. This theory fully supersedes Von Neumann CA for language design.

1.1 Signature and Agents

Definition 2.1 (Signature). A signature $\Sigma$ is a set of agent names $\alpha$ each equipped with an arity $ar(\alpha) \in \mathbb{N}$.

An agent $\alpha$ of arity $n$ is drawn as a node with:

• 1 principal port (marked with a dot •)
• $n$ auxiliary ports $x_1, \ldots, x_n$ (ordered)

Total ports per agent: $ar(\alpha) + 1$.

1.2 Nets

Definition 1.2 (Net). A net $N$ over $\Sigma$ is a graph where:

• Nodes are agents from $\Sigma$ (each occurrence is distinct)
• Edges connect ports; each port is connected to at most one other port
• Ports with no connection are free ports forming the interface $\text{Int}(N)$
• No edge connects two auxiliary ports of the same agent

A net is closed if $\text{Int}(N) = \emptyset$.

1.3 Active Pairs

Definition 1.3 (Active pair). Two agents $\alpha, \beta$ form an active pair (or redex) when their principal ports are connected:

$$\alpha \bowtie \beta$$

This is the ONLY location where computation can occur.

1.4 Interaction Rules

Definition 1.4 (Rule). An interaction rule for the pair $(\alpha, \beta)$ is:

$$\alpha \bowtie \beta ;\longrightarrow; N_{\alpha\beta}$$

where $N_{\alpha\beta}$ is a net whose free ports are exactly the auxiliary ports of $\alpha$ and $\beta$.

Determinism constraint: Each pair $(\alpha, \beta)$ has at most one rule (commutativity: $(\alpha,\beta)$ and $(\beta,\alpha)$ share the same rule).

Locality: A rule application affects only the active pair and the net $N_{\alpha\beta}$; the rest of the net is untouched.

1.5 Strong Confluence

Theorem 1.1 (Strong Confluence, Lafont 1990). For any interaction system $(\Sigma, R)$, if $N \rightarrow_R N_1$ and $N \rightarrow_R N_2$ arise from different active pairs, then there exists $N_3$ such that:

$$N_1 \rightarrow_R N_3 \quad \text{and} \quad N_2 \rightarrow_R N_3$$

in exactly one step each.

Corollary: All reduction strategies (sequential, parallel, random) reach the same normal form. Parallelism is free.

Proof sketch: Different active pairs share no ports (by locality). Thus their reductions are completely independent; the resulting nets can be composed to yield $N_3$.

1.6 Symmetric Interaction Combinators

Definition 1.5. The Symmetric Interaction Combinators use signature:

$$\Sigma_{SIC} = {\gamma,; \delta,; \varepsilon}$$

with arities $ar(\gamma) = 2$, $ar(\delta) = 2$, $ar(\varepsilon) = 0$.

The six interaction rules:

Theorem 1.2 (Universality, Lafont 1997). The symmetric combinators $(\Sigma_{SIC}, R_{SIC})$ are computationally universal: any interaction system can be translated into $(\Sigma_{SIC}, R_{SIC})$.

Corollary: Any algorithm expressible in lambda calculus (or equivalently Turing machines) has a representation in NELA using only $\gamma$, $\delta$, $\varepsilon$.

1.7 Comparison to Von Neumann CA

For full detail see Part 4. Summary:

Part 2 — Linear Logic (Girard, 1987)

Resource semantics for NELA. LL types are the types of NELA ports. Cut elimination in LL proof nets corresponds exactly to interaction net reduction. A well-typed NELA net IS a proof net — type checking equals proof verification.

2.1 Resource Semantics

Classical logic has weakening ($A \vdash A \wedge A$) and contraction ($A \wedge A \vdash A$), meaning propositions can be copied and discarded freely. Linear Logic removes these structural rules, making every resource exactly once usable.

Linear implication: $A \multimap B$ means "consuming $A$ produces $B$" (no copying of $A$).

2.2 Connectives and Their Interaction Net Counterparts

Correction (from case study translations, Part 6): The original spec omitted & and ⊕. Their absence caused Mat_T's type to be stated with $\parr$ (par), which is wrong: par cannot select exactly one branch. & and ⊕ are required for sound pattern matching over algebraic data types.

Key identity: Cut elimination in linear logic proof nets corresponds exactly to interaction net reduction. A proof = a NELA program.

2.3 Proof Nets

A proof net is a graph representation of a LL proof where:

• Formulas are edges (hyperedges)
• Inference rules are nodes (agents)
• The correctness criterion (Girard's long trip criterion) ensures the net is a valid proof

Consequence for NELA: A well-typed NELA net IS a proof net. Type checking = proof verification.

Part 3 — Dependent Type Theory (Martin-Löf, 1984)

Programs = proofs. Ill-typed NELA nets are structurally unrepresentable. Use Π-types for parameterized agents, Σ-types for records/existentials, Id-types for equality constraints enforced at construction time.

3.1 Judgment Forms

Martin-Löf Type Theory (MLTT) has four basic judgments:

3.2 Dependent Products (Π-types)

$$\frac{\Gamma \vdash A ;\mathsf{type} \quad \Gamma, x:A \vdash B(x) ;\mathsf{type}}{\Gamma \vdash \Pi_{x:A} B(x) ;\mathsf{type}}$$

This generalizes function types: when $B$ does not depend on $x$, $\Pi_{x:A} B = A \to B$.

In NELA: a Π-type corresponds to a parameterized agent family $\alpha_v$ where the agent type depends on the value $v$ flowing through a port.

3.3 Dependent Sums (Σ-types)

$$\frac{\Gamma \vdash A ;\mathsf{type} \quad \Gamma, x:A \vdash B(x) ;\mathsf{type}}{\Gamma \vdash \Sigma_{x:A} B(x) ;\mathsf{type}}$$

Pairs $(a, b)$ where $b : B(a)$. Used in NELA to encode records and existential types.

3.4 Identity Types

$$\frac{\Gamma \vdash a : A \quad \Gamma \vdash b : A}{\Gamma \vdash \mathsf{Id}_A(a,b) ;\mathsf{type}}$$

Inhabitants of $\mathsf{Id}_A(a,b)$ are proofs that $a$ equals $b$. In NELA, these are typed edges that enforce program equalities at construction time.

3.5 Curry-Howard-Lambek Correspondence

NELA consequence: Writing a NELA program = constructing a proof. An ill-typed NELA net = an unprovable proposition = structurally impossible to construct.

Part 4 — Von Neumann CA: Historical Context Only

Do not use this section to guide language design. Von Neumann CA pre-dates type theory and confluence guarantees. Interaction Nets (Part 1) strictly subsume it for all NELA purposes. This section exists for historical completeness and to document the two concepts NELA inherited.

4.1 What NELA Inherited from CA

These two properties are both derivable from the interaction net active-pair constraint. They are not axioms in NELA; they are theorems.

4.2 Why CA Was Insufficient (and Superseded)

4.3 Self-Reproduction (Von Neumann Property, Restated)

Von Neumann proved a CA could construct a copy of itself. In NELA this is derivable:

$$N ;\rightarrow_R^*; N \otimes N$$

constructible using Dup agents on all top-level !-typed ports. The !A modality of Linear Logic (Part 2) is what makes this principled rather than ad hoc.

Part 5 — NELA Language Specification (Derived)

5.1 Core Signature

NELA's base signature extends $\Sigma_{SIC}$ with typed agents:

⚠️ Revisions from case study translations (Part 6): Mat type changed — was ⊗/⊸, now uses & (additive branch offer). Fix type changed — function now receives a copyable recursive handle !(A -o B). New agents Inl, Inr, IOToken, FixMutual added.

5.2 Rewrite Rules (Core)

Beta reduction (Lam ⊳ App):

Lam(body, var) ⊳ App(func, arg)
─────────────────────────────────
body[var := arg]   (substitute via port rewiring)

Duplication (Dup ⊳ Lam):

Dup(a, b) ⊳ Lam(body, var)
───────────────────────────
Lam(body1, var1) ── a
Lam(body2, var2) ── b
Dup(body1, body2) ⊳ body
Dup(var1,  var2)  ⊳ var

Erasure (Era ⊳ Lam):

Era ⊳ Lam(body, var)
─────────────────────
Era ⊳ body
Era ⊳ var

Constructor dispatch (Con_i ⊳ Mat_T):

Con_i(a₁,...,aₙᵢ) ⊳ Mat_T(br₁, ..., brₖ)
────────────────────────────────────────────
Fire branch brᵢ with arguments (a₁ ⊗ ... ⊗ aₙᵢ)
Era ⊳ brⱼ  for all j ≠ i   (erase all other branches)

Exactly one branch fires; no duplication occurs. The &-type of the branch set guarantees this: & is a non-duplicating offer of multiple possibilities; exactly one is consumed by annihilation with Con_i.

Sum injection dispatch (Inl/Inr ⊳ Case):

Inl(a) ⊳ Case(left_fn, right_fn)     Inr(b) ⊳ Case(left_fn, right_fn)
──────────────────────────────────    ──────────────────────────────────
App(left_fn, a); Era ⊳ right_fn       App(right_fn, b); Era ⊳ left_fn

CA Cell transition (Cell ⊳ Cell): local Von Neumann rule application between adjacent Cell agents (only at CA execution substrate level, not at language semantics level).

5.3 Type System

NELA types are dependent linear types: dependent products and sums over a linear base.

Typing judgment: $\Gamma \vdash N : T$ means net $N$ with free ports typed by context $\Gamma$ has output type $T$.

Linear context: $\Gamma = x_1 : A_1, \ldots, x_n : A_n$ where each $x_i$ appears exactly once in the derivation.

Port typing: Each free port $p$ of net $N$ is assigned a type. Principal ports have output types; auxiliary ports have input types.

Correctness: A closed net $N$ is well-typed iff:

1. All active pairs $\alpha \bowtie \beta$ have a matching rule in $R_\Sigma$
2. All port connections respect the linear type assignments
3. No proof net correctness violation (Girard's criterion)

5.4 Program Serialization Format

Version note: v0.1 used raw interaction net JSON (signature / nodes / edges). This was abandoned — hand-writing 17-node nets produced 0 reductions. v0.2 introduced a JSON expression DAG surface language. v0.3 (current) uses S-expression syntax. The JSON dict AST is the internal IR; .nela files are the authoring format. The NELA-C interaction net is compiler output, never hand-authored.

A NELA-S v0.3 program is an S-expression .nela file:

(def fn_name (param ...)
  body-expr)

; Multi-def (mergesort example):
(def split (lst) ...)
(def merge (a b) ...)
(def mergesort (lst) ...)

The parser (nela_parser.parse_file) produces the internal dict representation consumed by eval_expr. The NELA-C format (signature / nodes / edges / interface) is generated by the compiler from that dict and is never hand-authored.

5.5 Self-Reproduction (Von Neumann Property, Restated)

A NELA net $N$ is self-reproducing iff there exists a finite reduction sequence:

$$N ;\rightarrow_R^*; N \otimes N$$

This is constructible using Dup agents on all top-level !-typed ports. The self-reproducing net is the direct analog of Von Neumann's Universal Constructor, but formalized via the !A modality of Linear Logic.

Part 5.6 — Standard Library ADTs

All ADTs are $\mu$-recursive types (isorecursive or inductive) encoded as $\oplus$-sums of their constructors. Each is handled with Con_i and Mat_T agents.

Boolean

$$\mathbf{Bool} = \mathbf{1} \oplus \mathbf{1}$$

Natural Numbers (Peano)

$$\mathbf{Nat} = \mu X.; \mathbf{1} \oplus X$$

Note (from quicksort translation): A Nat used as pivot must be explicitly promoted to !Nat before duplication. Promotion promote : Nat -o !Nat is valid only when the value originates from a !-context. All comparison operations therefore require !Nat arguments.

List

$$\mathbf{List}(A) = \mu X.; \mathbf{1} \oplus (A \otimes X)$$

Option

$$\mathbf{Option}(A) = \mathbf{1} \oplus A$$

Used for HTTP router route lookup (see Part 6, Case Study 2).

Result

$$\mathbf{Result}(A, E) = A \oplus E$$

Stream (linear sequential cursor)

$$\mathbf{Stream}(A) = \mu X.; \mathbf{1} \oplus (A \otimes X)$$

Isomorphic to List(A) structurally, but strict-spine by convention: each element is consumed before the tail is examined. A Stream cannot be rewound without explicit Dup. Used as parser input (see Part 6, Case Study 3).

IO (linear world token)

$$\mathbf{IO}(A) = \mathbf{IOToken} \multimap A \otimes \mathbf{IOToken}$$

All effectful nodes have type $A \otimes \mathbf{IO} \multimap B \otimes \mathbf{IO}$, threading IOToken linearly. The token cannot be Dup-ed (not !IO) — this enforces sequential I/O ordering and eliminates data races structurally.

Part 6 — Translation Case Studies and Framework Corrections

These three translations exposed structural flaws in the original specification. Each flaw is documented with its root cause and the correction applied.

Case Study 1: Quicksort (recursive divide-and-conquer)

Source intent (Python, TheAlgorithms pattern):

def quicksort(lst):
    if not lst: return []
    pivot, *rest = lst
    left  = [x for x in rest if x <= pivot]
    right = [x for x in rest if x >  pivot]
    return quicksort(left) + [pivot] + quicksort(right)

NELA TypedSpec:

{
  "name": "quicksort",
  "inputs":  [{"name": "lst", "type": "List(!Nat)", "banged": false}],
  "outputs": [{"type": "List(!Nat)"}],
  "invariants": ["sorted(output)", "permutation(input, output)"],
  "side_effects": []
}

NELA net (key active pairs):

Fix ⊳ QS              → unroll once; QS receives !(List(!Nat) -o List(!Nat)) self-handle
QS ⊳ Nil              → return Nil
QS ⊳ Cons(h, t)       → promote h to !Nat; Dup(!h) → h1 ⊗ h2
                         Filter(≤ h1)(t) → left;  Filter(> h2)(t) → right
                         Append(App(QS, left), Cons(h_orig, App(QS, right)))

Flaws exposed:

Case Study 2: HTTP Router (partial matching, side effects)

Source intent (Express.js / Flask pattern):

routes = [
    {"method": "GET",  "path": "/users",     "handler": get_users},
    {"method": "POST", "path": "/users",     "handler": create_user},
    {"method": "GET",  "path": "/users/:id", "handler": get_user},
]
def router(req, io):
    match = next((r for r in routes if r matches req), None)
    return match.handler(req, io) if match else (not_found_response, io)

NELA TypedSpec:

{
  "name": "router",
  "inputs": [
    {"name": "req", "type": "Request", "banged": false},
    {"name": "io",  "type": "IO",      "banged": false}
  ],
  "outputs": [{"type": "Response"}, {"type": "IO"}],
  "side_effects": ["database_read", "database_write"]
}

NELA net structure:

Mat_Request(method, path) dispatches via chain of Inl/Inr agents
Each branch: Mat_Option(Route) → Some → handler(req, io) / None → not_found(req, io)
IO token threaded through every handler node linearly

Flaws exposed:

Case Study 3: JSON Parser (mutual recursion, stream consumption)

Source intent (recursive descent, Python tiny-json pattern):

def parse_value(stream):
    tok = peek(stream)
    if   tok == '"': return parse_string(stream)
    elif tok == '{': return parse_object(stream)  # mutually recursive
    elif tok == '[': return parse_array(stream)   # mutually recursive
    elif tok.isdigit(): return parse_number(stream)
    else: raise ParseError(tok)

NELA TypedSpec:

{
  "name": "parse_value",
  "inputs": [{"name": "stream", "type": "Stream(Token)", "banged": false}],
  "outputs": [{"type": "Result(JSON, ParseError)"}, {"type": "Stream(Token)"}],
  "mutual_with": ["parse_object", "parse_array"],
  "side_effects": []
}

NELA net structure:

FixMutual(parse_value, parse_object, parse_array)
  each receives !(respective recursive handle)
Mat_Stream → peek first token
Inl/Inr dispatch tree on Token type
Result(Ok(json), Err(e)) threaded as output
Stream(Token) threaded linearly as residual input

Flaws exposed:

Summary of All Corrections

Part 7 — References and Further Reading