nela-foundations

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

Content truncated.