# Formal Theory

lambdagentpaas is grounded in a three-paper formal framework that establishes agent configurations as serialized Lambda calculus expressions. This document summarizes the core theoretical foundations.

---

## Paper I: The Lambda-Agent (LA) Calculus

### Core Insight

Every agent configuration (YAML, JSON, or programmatic) is a serialized Lambda calculus expression. Compiling an agent config with `from_config()` is desyntactic sugar -- it recovers the underlying Lambda term. Running the agent is beta-reduction.

### 11 Constructs

The LA calculus defines 11 constructs, each with an independent Lambda semantics:

| # | Construct | LA Term | Lambda Correspondence |
|---|-----------|---------|----------------------|
| 1 | **Lam** | `lambda_D . F_{M,D}` | Lambda abstraction -- LLM oracle call |
| 2 | **Application** | `(f x)` | Function application = beta-reduction = autoregressive decoding |
| 3 | **Compose** | `lambda x. g(f(x))` | Function composition: `f >> g` |
| 4 | **If** | `IF c t e = lambda c.lambda t.lambda e. c t e` | Church conditional |
| 5 | **Loop** | `Y = lambda f. (lambda x. f(x x)) (lambda x. f(x x))` | Y combinator with bounded unfolding |
| 6 | **Pair** | `PAIR = lambda a.lambda b.lambda f. f a b` | Church pair -- parallel execution |
| 7 | **Fst/Snd** | `FST = lambda p. p TRUE` / `SND = lambda p. p FALSE` | Pair projections |
| 8 | **Tool** | `lambda x. oracle(x)` | External function lifted into Lambda world |
| 9 | **Route** | `CASE (classifier x) [(l1, a1), ...]` | Generalized Church boolean -- multi-way dispatch |
| 10 | **Guard** | `{x : T | P(x)}` | Dependent type / refinement type with retry |
| 11 | **Memory** | `Gamma' = Gamma union s` | Environment extension -- persistent state injection |

### Type System

Each agent has a function type `tau1 ->^epsilon tau2` (Paper III Definition 3), where:

- `tau` ranges over base types: `Str | Int | Bool | Float | Any | Json(S) | tau1 x tau2 | tau1 | tau2`
- `Json(S)` reuses JSON Schema as the structural type language (Definition 2)
- Subtyping (Definition 5) supports width/depth structural subtyping, numeric promotion (`Int <: Float`), and union introduction

### Lint Rules and the 835-Config Evaluation

The compiler includes 26 lint rules (L001--L026) organized into three severity levels:

- **ERROR (6 rules)**: True defects requiring fix before deployment (e.g., missing `terminate` tool = no Y combinator base case)
- **WARN (11 rules)**: Potential issues (e.g., `maxSteps > 10` without CEK engine)
- **INFO (9 rules)**: Informational (e.g., detected framework, suggested optimizations)

These rules were validated against 2,225 real-world YAML configs scraped from open-source repositories. Of these, 881 parsed successfully and 835 passed lint -- providing an empirical validation of the static analysis pipeline.

---

## Paper II: Operational Semantics

### 23 Reduction Rules

Paper II defines small-step operational semantics via 23 reduction rules, formalized as a labeled transition system:

```
<C, E, K, sigma, c>  --[alpha]-->  <C', E', K', sigma', c'>
```

The rules fall into three categories:

1. **Dispatch rules** (C-Lam, C-Tool, C-Comp, C-If, C-Route, C-Loop, C-Pair, C-Guard, C-Mem, C-Generic): examine the control component and set up the continuation stack.
2. **Return rules** (C-CompRet, C-LoopRet, C-PairMid, C-PairRet, C-GuardOK, C-GuardRetry, C-GuardFail, C-MemRet, C-IfRet, C-RouteRet, C-Halt): pop the continuation stack and deliver values.
3. **Special rules** (C-LoopBase, C-LoopBound, C-Fst, C-Snd): handle loop termination and projections.

### CEK Machine

The Agent CEK Machine (`cek_machine.py`) implements these rules as an abstract machine in the style of Felleisen & Friedman (1986). Machine state is a 5-tuple:

```
<C, E, K, sigma, c>
  C: control     -- current term or value
  E: environment -- variable bindings dict
  K: continuation -- stack of frames (CompK, LoopK, PairLK, PairRK, GuardK, MemK, IfK, RouteK, HaltK)
  sigma: store   -- memory store dict
  c: cost        -- cumulative CostVector(tokens, latency_s, money_usd)
```

Key design choices:
- **Step-by-step execution** via `machine.step()` with full state inspection at every transition
- **Observable labels** (`tau` for silent steps, `llm(name)` for LLM calls, `tool(name)` for tool calls, `mem(key)` for store updates)
- **Transition trace** records every step with rule name, label, cost delta, and wall-clock duration

### YIELD Mechanism

LLM and Tool calls are effectful operations that "yield" control to external oracles. In the CEK machine, these correspond to the C-Lam and C-Tool rules, which:

1. Suspend the machine (conceptually -- in practice, the call blocks synchronously or `await`s asynchronously via `run_async()`)
2. Invoke the oracle (LLM API or Python function)
3. Resume with the oracle's return value as the new control

This maps naturally to `async/await`: each C-Lam and C-Tool step is an await point.

### 6 Algebraic Laws

The reduction rules satisfy 6 algebraic laws that enable equational reasoning about agent programs:

1. **Associativity of Compose**: `(f >> g) >> h = f >> (g >> h)` -- pipeline order doesn't matter for grouping
2. **Identity of Compose**: `id >> f = f = f >> id` -- identity agent is the unit
3. **Pair symmetry**: `Pair(f, g)` produces `(f(x), g(x))` regardless of evaluation order when store-independent
4. **Loop unfolding**: `Loop(body, cond, n)(x) = if cond(x, 0) then x else Loop(body, cond, n-1)(body(x))`
5. **Guard idempotence**: `Guard(Guard(f, P), P) = Guard(f, P, retry=2*retry)` -- nesting guards compounds retries
6. **Route exhaustiveness**: `Route(cls, routes, default)` always produces a value when default is provided

### Pair Confluence (Proposition 30)

When `writes(f) intersection writes(g) = emptyset` (store independence), then `Pair(f, g)` is confluent -- the result is independent of scheduling strategy. This is verified at runtime by `check_store_independence()` and is the theoretical basis for `AsyncPar`'s safety guarantee.

---

## Paper III: Type and Effect System

### 15 Type Rules

Paper III defines a type-and-effect system with 15 typing rules:

| Rule | Judgment | Description |
|------|----------|-------------|
| T-Lam | `Gamma |- Lam(name, prompt, model) : Str ->^{llm(m)} Str` | LLM abstraction |
| T-App | `Gamma |- f : A ->^e B, Gamma |- x : A => f(x) : B` | Application |
| T-Compose | `f: A ->^e1 B, g: B' ->^e2 C, B <: B' => f >> g : A ->^{e1 . e2} C` | Composition with subtype check |
| T-If | `cond: A -> Bool, t: A ->^e1 B, e: A ->^e2 C => If: A ->^{max(e1,e2)} (B \| C)` | Conditional |
| T-Loop | `body: A ->^e A => Loop(body, cond, n) : A ->^{e^n} A` | Bounded iteration |
| T-Pair | `f: A ->^e1 B, g: A ->^e2 C => Pair(f, g) : A ->^{e1 \|\| e2} (B, C)` | Parallel pair |
| T-Fst | `Fst : (A, B) -> A` | Left projection |
| T-Snd | `Snd : (A, B) -> B` | Right projection |
| T-Tool | `Tool(name, fn) : A ->^io B` | External oracle |
| T-Route | `cls: A ->^e1 Label, routes: {l: A ->^ei Bi} => Route: A ->^{e1 . max(ei)} Union(Bi)` | Multi-way dispatch |
| T-Guard | `agent: A ->^e B, P: B -> Bool => Guard(agent, P, k): A ->^{e^(1+k)} B` | Refinement with retry |
| T-Memory | `agent: A ->^e B, store: S => Memory(agent, store): A ->^{state . e} B` | State injection |
| T-Sub | `e : A, A <: B => e : B` | Subsumption |
| T-StrJson | `Str <: Json(string)` | String embedding |
| T-NumPromo | `Int <: Float` | Numeric promotion |

### Effect Algebra

Effects model the observable side effects of agent execution:

```
epsilon ::= pure | llm(m) | io | state(s) | epsilon1 . epsilon2 | epsilon1 || epsilon2 | epsilon^n
```

Three composition operators:

- **Serial** (`epsilon1 . epsilon2`): Compose(f, g) -- execute f's effects then g's
- **Parallel** (`epsilon1 || epsilon2`): Pair(f, g) -- effects occur simultaneously
- **Iterate** (`epsilon^n`): Loop(body, n) -- body's effect repeated n times

The effect lattice defines a partial order: `pure <= state <= io <= llm`, with `pure` as the bottom element (Proposition 10: monotonicity -- adding effects only increases the position in the lattice).

### Graded Types

Cost is tracked as a graded type via `CostVector(tokens, latency_s, money_usd)`. The `cost_grade` module provides compile-time cost estimation -- an upper bound on execution cost derived from the agent's structure:

- Lam: cost = `max_tokens * price_per_token(model)`
- Compose: cost = `sum(stage costs)`
- Loop: cost = `body_cost * max_steps`
- Pair: cost = `max(f_cost, g_cost)` for latency, `sum` for tokens/money
- Guard: cost = `inner_cost * (1 + retry)`

### Algebraic Effect Handlers

Paper III Section 6 introduces algebraic effect handlers that decouple agent semantics from execution strategy. The `EffectHandler` interface defines four effect operations:

- `handle_llm(prompt, input, model, ...)` -- how to handle LLM effects
- `handle_tool(tool_name, fn, input)` -- how to handle IO effects
- `handle_state_read/write(store, key, ...)` -- how to handle state effects
- `handle_cost(tokens, latency, model)` -- cost tracking hook

Three built-in handlers:

| Handler | LLM | Tool | State | Use Case |
|---------|-----|------|-------|----------|
| `ProductionHandler` | Real API call | Real execution | Real storage | Production |
| `TestHandler` | Deterministic mock | Mock result | In-memory dict | Testing |
| `TraceHandler` | Real call + full logging | Real + audit trail | Real + audit | Debugging |

**Handler Type Preservation Theorem**: If `agent : A ->^epsilon B`, then for any well-typed handler `h`, `h(agent) : A ->^{epsilon'} B` -- the input/output types are preserved, only effects may change.

---

## Key Theorems

### Type Safety (Progress + Preservation)

- **Progress**: If `Gamma |- M : tau` and M is not a value, then there exists M' such that `M -> M'`. No well-typed agent gets "stuck."
- **Preservation**: If `Gamma |- M : tau` and `M -> M'`, then `Gamma |- M' : tau`. Types are preserved across beta-reduction steps. For stores: if `Sigma |- M : tau` and `M -> M'`, then `Sigma' |- M' : tau` where `Sigma' supseteq Sigma` (stores only grow).

### Bounded Termination (Theorem 5.4)

Every agent program with finite `maxSteps` terminates in at most `O(maxSteps * pipeline_depth)` CEK transitions. This follows from:

1. Loop unfolding decreases `remaining` by 1 at each iteration
2. Compose pushes at most `|stages|` CompK frames
3. Guard retries are bounded by the `retry` parameter
4. The CEK machine enforces a global `max_steps` limit (default 10,000)

Unbounded execution requires an explicit `maxSteps: infinity` annotation, which the linter flags as a warning.

### Cost Monotonicity (Proposition 23)

The cumulative cost vector is monotonically non-decreasing across transitions:

```
c' >= c   (component-wise: tokens' >= tokens, latency' >= latency, money' >= money)
```

This invariant is checked at every CEK step when `check_cost_monotonicity=True`. A `CostMonotonicityViolation` is raised if any component decreases -- indicating a bug in cost accounting, not in the agent program. This property enables reliable cost budgeting: if `c` has reached the budget threshold at any point, the execution can be safely paused.

---

## Summary: The Lambda-Agent Correspondence

The central contribution is a formal, executable mapping:

```
Agent Configuration  <-->  Lambda Calculus Expression
     YAML/JSON                Lambda Term
     from_config()            deserialization
     agent(input)             beta-reduction
     CEK machine              abstract machine
     effect handler           algebraic effects
     lint rules               static analysis
     type checker             type system
     cost estimator           graded types
```

This correspondence is not merely an analogy -- it is implemented as 10,000+ lines of Python in the `lambdagent` library, validated against 835 real-world configs, and supported by formal proofs of type safety, termination, and cost monotonicity.