Skip to content

A zoo of formal systems.

This zoo maps calculi and logics as a unified morphospace based on primitive count, rewrite laws, behavioral quotient, and carrier profiles. Here, λ-calculus, SKI, Iota, π-calculus, and sequent calculus are presented as operational neighbors within a shared semantic space.

0Systems
0Families
0Turing-complete

Specimen Anatomy: Every formal system is treated as a specimen with observable features: basis size, rewrite laws, normalization behavior, and quotient under bisimulation or behavioral equivalence.

Morphospace

Nodes are formal systems placed by primitive count and carrier participation. Edges indicate direct reduction, compilation, or known interpretive embeddings.

Specimens

Each card is a candidate exhibit label: basis, rewrite semantics, quotient, and the carrier fingerprint that situates it relative to ISAR.

Selected system

The detailed panel is where the zoo becomes research-grade: you can inspect the system’s local anatomy and how it embeds into neighboring systems.

Select a system from the graph or cards.

Use the tabs in the detail panel to inspect the system's local anatomy, translation maps, and interactive execution environments.

Zoo Classification Axes

specification
  • Primitive basis size
  • Rewrite locality
  • Normalization behavior
  • Bisimulation quotient
  • ISAR carrier fingerprint
  • Compilation / interpretation neighbors

Interactive Lab

active

This atlas integrates real-time compilers, abstract syntax tree parsers, and reduction simulators. You can compile lambda terms (λ → SKI → Iota), run leftmost-outermost combinator reductions, and explore structural tree views dynamically.