Cyclic Graphs and Memoization in Pure $λ$-Calculus

Source: arXiv:2606.22908 · Published 2026-06-22 · By Bo Yang

TL;DR

The paper addresses fundamental difficulties in representing cyclic and shared computations purely within the standard λ-calculus, which traditionally requires extensions such as letrec, μ-binders, or built-in fixed point combinators to handle recursion and explicit memoization caches to enable sharing of repeated work. Bo Yang presents a novel operational semantics for the pure λ-calculus that accomplishes recursion and sharing purely by tabling weak-head reduction states, without extending the calculus or requiring impure state. This tabling approach folds repeated and cyclic sub-terms into finite graphs that represent the same lazy meaning (the Lévy–Longo tree) as ordinary reduction but terminates in situations where ordinary evaluation diverges, such as unproductive loops. The approach simultaneously automates dynamic programming and graph computations as a natural consequence of state memoization on structural identity.

The main contribution is an interpreter implementing this tabling semantics, which constructs cyclic graphs from pure λ-terms with no additional recursion construct and no externally written memo tables. It correctly folds infinite but rational structures into finite cyclic graphs, detects and returns bottom (⊥) for unproductive loops in finite time, and shares repeated subproblems automatically in classic examples like edit distance. The paper rigorously proves soundness and uniqueness of the semantics and shows applications including graph reachability, game search and a bootstrap compiler. Overall, the work steps beyond the standard view that pure λ-calculus is inherently unable to express sharing or cycles efficiently without impurity or extensions, by exploiting tabling as a pure meta-level operational mechanism.

Key findings

• Tabling weak-head reduction yields a sound operational semantics for pure λ-calculus that maps terms to finite or cyclic graphs representing their Lévy–Longo tree (Thm A.9).
• The interpreter folds repeated states by structural identity, implemented by interned terms with constant-time equality, enabling sharing without mutable memo tables.
• Edit distance computation in pure λ-calculus goes from exponential to O(mn) time and space by the interpreter sharing (m+1)(n+1) suffix pairs as tabled states (Fig 1).
• The infinite stream of zeros Y(cons 0) evaluates to a finite cyclic graph with a back edge representing the recursive tail (Fig 2).
• The interpreter detects unproductive loops like Ω = (λx.xx)(λx.xx), returning ⊥ in finite time rather than diverging (Fig 3).
• The solution computed is unique and independent of reduction order, matching least and greatest fixpoints of the weak-head reduction semantics (Thm 2.1).
• Encoding choices affect the granularity of state identity, with a defunctionalized compiler representation reducing interned objects and speeding evaluation by about 5x (Appendix B).
• The interpreter naturally subsumes memo tables of dynamic programming, transposition tables of game search, and visited sets of graph algorithms as instances of state tabling.

Methodology — deep read

The core methodology builds on viewing weak-head reduction as a monotone one-layer map from terms to their weak-head normal forms (WHNF). Each term t exposes one layer out(t) consisting of its WHNF top constructor (variable, lambda, or application with variable head) and its immediate subterms.

(1) Threat model & assumptions: Not a security paper; the key assumption is a pure λ-calculus setting without added recursion constructs or mutable state, evaluating lazy terms represented with de Bruijn indices. The adversary is the undecidability of β-equivalence and infinite unfolding; the method guarantees decidability and folding only up to rational terms.

(2) Data: The 'data' are λ-terms themselves, with no external datasets. Terms are interned (hash-consed) to ensure terms share structure and to make structural identity decidable in constant time. Finite acyclic terms reachable under reduction form the state space, key for tabling.

(3) Algorithm: The main component is the Tabled evaluation driver (Algorithm 1). It repeatedly applies 'Resolve' to terms, caching results by structural identity:

• Resolve(t): if t cached, returns cached layer.
• If t being processed on the stack, returns current approximation layer (⊥ initially).
• Otherwise pushes t to stack, computes out(t) by WHNF (Algorithm 2), merges new layer with previous approximation using an ordering (⊥ ≤ layer), and caches result.
• Repeat until fixed point (no change). The WHNF function (Algorithm 2) performs weak-head reduction steps:
• If t is variable or lambda, returns it.
• If application of a lambda, β-contract and recurse.
• If application of variable or application, return that application.
• If no WHNF, return ⊥. This combination of tabling and weak-head unfolding computes the least fixpoint representation of the term's Lévy–Longo tree, folding cycles into back edges in the graph.

(4) Training regime: Not applicable; interpreter implementation in Claude Code runs these algorithms with interned terms. Evaluations involve running the interpreter with example terms including Y(cons 0), edit distance, Ω.

(5) Evaluation Protocol: Measures include termination behavior, graph shape, and complexity. Examples:

• Edit distance runs with strings of length m, n are analyzed, with tabling reducing exponential calls (19 naive) to O(mn) distinct states (9 in one example).
• The infinite stream is reduced to a cyclic graph.
• Ω irreducible unproductive loop detected and returned as ⊥. No formal statistical tests; evaluation focused on functional correctness and graph shape.

(6) Reproducibility: Interpreter’s code and examples publicly available [26], implementations fully specified by the Algorithm pseudocode and descriptions. Proofs of soundness and uniqueness are in appendix but code is executable.

Concrete example: For edit distance of 'ab' vs 'cd', the interpreter steps through suffix pairs, unfolding recursive calls and caching calls by structural identity of suffix pairs (which are shared sub-terms). Instead of recomputing states, table hits return precomputed layers. This produces the finite memo graph of 9 nodes instead of naive 19 calls, fully tabling the dynamic programming problem.

Technical innovations

• Applying tabling directly to weak-head reduction to yield a pure λ-calculus operational semantics that folds cycles into finite graphs without recursion operators or side effects.
• Using structural identity via interning for constant-time detection of repeated states, enabling memoization without impure caches or additional language features.
• Characterizing unproductive loops as bottom (⊥) values detected in finite time by bottom-up fixpoint iteration of the term’s WHNF layers.
• Encoding higher-order λ-terms into first-order defunctionalized forms to coarsen state identity and boost sharing and performance in compilation.

Baselines vs proposed

• Naive recursive evaluation of edit distance: exponential number of calls (e.g., 19 calls for 'ab' vs 'cd') vs tabled evaluation: only distinct suffix pairs computed once (9 states), achieving O(mn) complexity.
• Ordinary weak-head reduction of infinite stream (Y(cons 0)) unfolds infinitely vs tabled evaluation produces finite cyclic graph representing infinite sequence.
• Ordinary weak-head reduction of Ω diverges; tabled evaluation detects unproductive loop and returns ⊥ in finite time.

Limitations

• Structural identity used for tabling is a decidable but coarse equivalence, falling short of full β-equivalence and the entire rational fragment (Appendix A.3).
• The approach requires finite-state terms (rational terms with finitely many distinct subterms) for producing finite graphs; it cannot represent truly infinite-distinct-state computations as finite structures.
• Performance and memory use depend heavily on choice of encoding for state identity; coarse encodings increase sharing but may lose semantic distinctions.
• No adversarial evaluation or robustness testing beyond classical example problems; behavior on arbitrary complex λ-terms or pathological cases is not covered.
• Interpreter and proofs rely on interned terms; overhead and scalability to very large systems not experimentally validated.
• No direct evaluation of overheads compared to conventional evaluators with explicit memo tables; practical runtime tradeoffs are unclear.

Open questions / follow-ons

• How can the notion of equivalence for tabling be extended beyond structural identity to approach β-equivalence while retaining decidability?
• What are the practical performance tradeoffs and limits of tabling-based pure λ-calculus interpreters on large scale graph and program analyses?
• Can this approach be generalized to richer calculi, including effects, types, or concurrency, while preserving purity and tabling benefits?
• How does altering the state encoding or reduction strategy impact sharing and the expressiveness of the resulting graph DSL?

Why it matters for bot defense

For bot-defense engineers and CAPTCHA practitioners, the paper's core insight that pure functional terms can represent and share infinite and cyclic computation graphs without impurity or extensions is intellectually useful. It demonstrates how memoization and dynamic programming emerge naturally from structural identity-based tabling without explicit caching code. Practically, it suggests potential designs for computational backends or analyzers that extract shared computational graphs from recursive functional formulations, which could inform efforts to detect or simulate bot behaviors exhibiting recursive or looping patterns without relying on impure state.

Though purely theoretical, the method underlines how declarative specifications of state machines, reachability, or game searches can be compiled into tabling-driven interpreters that optimize repeated work automatically. This may help guide CAPTCHA generation or bot detection systems leveraging graph-structured representations of behavior or challenges, especially in the design of interpretable or analyzable domain-specific languages that embed memoization purely at the operational semantics level.

Cite

@article{arxiv2606_22908,
  title={ Cyclic Graphs and Memoization in Pure $λ$-Calculus },
  author={ Bo Yang },
  journal={arXiv preprint arXiv:2606.22908},
  year={ 2026 },
  url={https://arxiv.org/abs/2606.22908}
}

Read the full paper

• arXiv:2606.22908 (abstract)
• arXiv:2606.22908 (PDF)