lambdagent/docs/theory.md

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)}`
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 awaits 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`
T-App	`Gamma	- f : A ->^e B, Gamma
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.