Lambda Calculus Visualizer

An in-browser teaching tool for exploring untyped lambda calculus through bold, colored Tromp diagrams, step-by-step beta reduction, and synchronized 2D and 3D reduction maps.

The interface separates those jobs into focused Diagram, 2D Map, and 3D Space workspaces. They share one evaluator session, selected state, explored graph, and share link without mounting all three visualizations at once. Everything runs locally in the browser and the production site is a static GitHub Pages build.

Technology

• Svelte 5, SvelteKit, TypeScript, and Vite for the application
• Inline SVG for detailed, accessible Tromp diagrams
• A custom deterministic TypeScript layout and inline SVG for the precise 2D reduction map
• 3d-force-graph and Three.js for the supplementary WebGL map
• Rust compiled to WebAssembly for parsing, evaluation, provenance, and scene projection
• Vitest, Playwright, Cargo tests, strict Clippy, ESLint, Prettier, and Dependency Cruiser for quality

See ARCHITECTURE.md for module ownership and the ADR index for the decisions behind the stack.

Prerequisites

• Node.js 24.15.0 and npm 11.16.0
• Rust 1.96.0 (the repository toolchain file installs Clippy, rustfmt, and the Wasm target)
• wasm-pack 0.15.0

With rustup and Cargo installed:

cargo install wasm-pack --version 0.15.0 --locked
npm ci

Use npm install instead of npm ci only when intentionally updating dependencies and the lockfile.

Develop

Build the development Wasm package and start Vite:

npm run dev:full

For frontend-only work after a Wasm package already exists:

npm run dev

The editor accepts λx.x and the ASCII spelling \x.x; application associates to the left and parentheses make grouping explicit.

From either map workspace, open Demos for six prepared 3D computations: a three-choice branching cube, a four-dimensional identity hypercube, a duplication fan, a terminating escape from Ω, Church 3 × 2, and the full Factorial 3 search. Every demo opens at beta zero with only its complete one-step frontier visible. Search all branches then reveals the remaining canonical BFS layers; no demo silently starts at its finished graph.

The examples deliberately produce different shapes. The branching cube finishes at 8 states and 12 edges; the hypercube at 16/32; duplication at 20/28; Escape from Ω at 6/11 including four cycle edges; and Church 3 × 2 at 32/58 across seven beta levels.

The two kinds of Play have intentionally different meanings. Play reduction in Diagram follows one normal-order strategy path. Search all branches in either map performs a deterministic, layer-atomic breadth-first search: for every state in the current layer, it contracts every available redex, merges canonically identical terms, reveals the complete next layer, and stops at the first layer containing a normal form. Explore next layer performs exactly one such breadth wave when manual inspection is preferable; this small manual view preserves separate path occurrences, while automatic search switches to canonical nodes. Searches also stop explicitly on a closed cycle or a safety limit; they never claim that a bounded frontier is an answer.

Factorial computes 3 × 2 × 1 with Church multiplication and reaches Church numeral six in 24 normal-order Diagram steps. Its all-branches map starts in layered layout with the beta-zero root and both legal one-step successors. Search reaches its first normal form at beta depth 13 with 5,375 canonical states and 21,698 reduction edges, then selects that answer. The equivalent raw occurrence tree would contain 82,011,576 nodes through the answer layer, so canonical merging is essential; the dense result automatically switches to Points and a deterministic beta-depth cloud. Free-force layout remains available for smaller maps but is disabled for a graph this large because its simulation would make the page unresponsive. Diagrams remains available for smaller maps as an atlas of unboxed Tromp thumbnails. The selected/current state is electric blue, while other possible states remain pale. Presentation, selection, and exploration state stay synchronized when switching between 2D and 3D.

Quality commands

Command	Purpose
npm run check	Synchronize SvelteKit and run strict app and configuration checks
npm run format:check	Check repository formatting
npm run lint	Run ESLint and dependency-boundary checks
npm run test:unit	Run Vitest unit tests
npm run test:e2e:install	Install Playwright Chromium and its system dependencies
npm run test:e2e	Run browser tests against the production preview
npm run build	Build release Wasm and the static site
npm run validate	Run the ordinary frontend formatting, lint, type, and unit-test gate
npm run validate:rust	Run Rust formatting, native tests, and strict Clippy
npm run release:check	Run both validation gates, the production build, and Playwright end-to-end tests

Rust checks run separately:

cargo fmt --all --check
cargo test --workspace --all-targets
cargo clippy --workspace --all-targets -- -D warnings

Run npm run test:e2e:install once on a new machine before npm run release:check.

GitHub Pages

The deployment workflow runs on pushes to main and can also be started manually. It derives the correct BASE_PATH from the repository name, validates both Rust and TypeScript, builds the Wasm package and static SvelteKit site, then deploys build/ through GitHub Pages.

In the repository settings, select GitHub Actions as the Pages source. A project repository is served at /<repository>/; an <owner>.github.io repository is served at /. The same distinction can be tested locally:

BASE_PATH=/lambda-calculus npm run build
BASE_PATH=/lambda-calculus npm run preview

For a custom domain, set the repository Actions variable PUBLIC_BASE_PATH to / (or to the custom subpath) before deploying.

Product constraints

• Rendering is a projection of evaluator state; no renderer evaluates lambda terms.
• Color is reinforced with labels, focus, selection, and stroke treatment.
• Reduced motion, text history, and the 2D map remain available when WebGL is unavailable.
• Graph exploration is automatically bounded by depth, node, term-size, cycle, and step limits because many terms diverge or branch indefinitely.

Licensing note

The Cargo manifests declare MIT OR Apache-2.0, but canonical project license files have not been added because the repository owner's copyright and licensing choice still need confirmation. wasm-pack therefore emits a non-blocking license-file notice. Confirm the ownership details and add the standard license texts before publishing a package or making a public release.