λ Lisp & Lambda Calculus

Overview

The agent has two intertwined symbolic computation subsystems:

HyperLisp Sandbox — S-expression evaluator with topos bridge
Lambda Calculus Engine — Pure untyped λ-calculus on the Poincaré disk

Package: lisp/

HyperLisp Sandbox

Type System (LispTypes.kt)

LVal (sealed)
  ├── LNum(value: Double)       — numeric scalar
  ├── LSym(name: String)        — symbol
  ├── LStr(value: String)       — string
  ├── LBool(value: Boolean)     — boolean
  ├── LCons(car: LVal, cdr: LVal) — cons cell (list building block)
  ├── LLambda(params, body, env)   — closure
  ├── LVec(data: FloatArray)    — vector (manifold-typed)
  └── LBuiltin(name, fn)        — built-in function

Parser (LispParser.kt)

Tokenizer + recursive-descent S-expression parser:

Max nesting depth: 64
Supports: numbers, strings, symbols, quoted expressions, dotted pairs

Runtime (LispRuntime.kt)

Eval/apply core with:

Special forms: define, lambda, let, begin, if, cond, quote, set!
Manifold builtins: make-vec, vec-get, vec-set!, vec-len, vec-dot, vec-norm
Topos bridge: f* (pullback) and f_* (pushforward) — adjunction f* ⊣ f_*

Sandbox (LispSandbox.kt)

Safe evaluation wrapper:

κ tracking: Each eval costs energy
Session history: Persistent across DMN ticks
Effect drain: ToposEffect side-effects collected and applied

Topos Bridge (LispToposTypes.kt)

6 sorts, 6 geometric sequents. ToposEffect sealed hierarchy:

sealed class ToposEffect {
    data class WriteManifold(val key: String, val vec: FloatArray)
    data class ReadManifold(val key: String)
    data class EmitSignal(val channel: String, val payload: String)
    data class GoalProposal(val description: String)
    data class AffectDelta(val dValence: Float, val dArousal: Float)
    data class SelfAnnotation(val key: String, val value: String)
}

Lambda Calculus Engine

AST (LambdaTerm.kt)

LambdaTerm (sealed)
  ├── Var(name: String)                  — variable
  ├── Abs(param: String, body: LambdaTerm)  — abstraction
  ├── App(func: LambdaTerm, arg: LambdaTerm) — application
  ├── GodelNum(n: Long)                  — Gödel number literal
  ├── ChurchNum(n: Int)                  — Church numeral
  └── Quote(term: LambdaTerm)            — quoted term (meta-level)

Engine (LambdaEngine.kt)

class LambdaEngine(
    val maxReductions: Int = 500,
    val maxTermSize: Int = 512,
    val hyperbolicCurvature: Float = -1f  // K = -1 standard hyperbolic plane
)

Hyperbolic Reduction

Each β-reduction step is a geodesic movement on the Poincaré disk:

Position: (r, θ) in the unit disk {(x,y) : x² + y² < 1}
Cost per step: proportional to hyperbolic distance traveled
Curvature tensor: tracked at each reduction step

The Y-combinator is the fixed-point attractor on this manifold.

Key Operations

Operation	Description
`reduce(term)`	Normal-order β-reduction with step tracking
`godelEncode(term)`	Assign unique natural number ⌈t⌉ ∈ ℕ
`godelDecode(n)`	Reconstruct term from Gödel number
`diagonalize()`	Construct self-referential term D = λn.(decode(n) ⌈n⌉)
`quine()`	Fixed point of self-application Q = D ⌈D⌉
`detectFixedPoint()`	Cycle detection via Gödel codes

Gödel Numbering

Every λ-term receives a unique natural number:

⌈Var(x)⌉ = 2 × encode(x)
⌈Abs(x, M)⌉ = 3 × 2^⌈M⌉
⌈App(M, N)⌉ = 5 × 2^⌈M⌉ × 3^⌈N⌉

The diagonal lemma constructs self-referential terms — the foundation of Gödelian incompleteness.

Geometric Theory (T_lambda)

8 sorts, 8 geometric sequents:

Sequent	Meaning
β-progress	Every β-redex reduces in one step
Y-fixed	Y f reduces to f(Y f)
curvature-bound	Reduction cost ≤ hyperbolic curvature integral
normal-form	No redex ⊢ normal form
church-encode	Church numeral n ⊢ correct encoding
godel-round-trip	decode(encode(t)) = t
quine-existence	∃Q: Q reduces to Q
size-bound	Term size bounded by maxTermSize

Session Budget & DMN Coupling

The Lambda/Lisp subsystem is loosely coupled to the DMN cycle to prevent trapping:

Parameter	Value	Purpose
`consecutiveLispLambdaTicks`	max 5	Force cooldown after 5 consecutive ticks
`maxLispSessionDurationTicks`	40	Hard session timeout
Cooldown	15 ticks	Wait period after forced yield
Priority	Reflection > Daydream > Lambda	Lambda is lowest priority
Recovery	`detectStuckState()`	Force exit on Lambda trapping

WebVM Integration

A local Scheme REPL can run via WebVM for offline prototyping. See docs/webvm-lisp-lambda-vm.md.

WebVM (browser) → prototype S-expr → paste into app → LispSandbox.eval()

FilesExpand file tree

07-lisp-lambda.md

Latest commit

History