pith. sign in

arxiv: 2606.22908 · v2 · pith:WUMLGLCYnew · submitted 2026-06-22 · 💻 cs.PL · cs.LO

Cyclic Graphs and Memoization in Pure λ-Calculus

Bo Yang This is my paper

Pith reviewed 2026-06-29 04:57 UTC · model grok-4.3

classification 💻 cs.PL cs.LO
keywords lambda calculustablingcyclic graphsmemoizationoperational semanticsweak-head reductiondynamic programming
0
0 comments X

The pith

Tabling weak-head reduction in the pure λ-calculus produces finite cyclic graphs and automatic memoization without extensions.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows that the pure λ-calculus requires no added recursion constructs or memoization tables to represent cyclic data or share repeated work. Applying tabling to weak-head reduction yields an operational semantics in which any term that reaches only finitely many distinct states appears as a finite, possibly cyclic graph. The graphs preserve each term's standard lazy meaning and remain sound no matter the order of reductions. The resulting interpreter performs dynamic programming automatically, decides unproductive loops such as returning bottom for Ω in finite time, and lets pure λ-terms serve as a DSL for graph computations including self-compilation.

Core claim

Applying tabling, the standard method for solving a least-fixpoint equation, to weak-head reduction defines a new operational semantics for the pure λ-calculus that keeps each term's standard lazy meaning. A term that reaches finitely many distinct states comes out as a finite graph, possibly cyclic; the calculus stays pure, and the graph is sound and independent of reduction order.

What carries the argument

Tabling applied to weak-head reduction, which solves the least-fixpoint equation to emit graphs from terms while preserving lazy semantics.

If this is right

  • Dynamic programming occurs automatically by sharing repeated subproblems with no explicit memo table.
  • Cyclic graphs are created and transformed with no added recursion construct.
  • Unproductive loops are decided, returning bottom for Ω in finite time.
  • The λ-calculus becomes a DSL for graph computation such as transposition tables and bootstrap compilers written as pure terms.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same tabling mechanism might be applied to other reduction strategies to obtain graphs under different evaluation orders.
  • Pure λ-terms could express additional graph algorithms such as points-to analysis without side effects.
  • The approach may allow modeling of infinite data structures as finite cyclic graphs in typed settings.

Load-bearing premise

That tabling weak-head reduction produces graphs whose meaning matches each term's standard lazy semantics and stays sound for any reduction order.

What would settle it

An implementation of the tabling semantics on a term with finitely many states that either returns a graph whose meaning differs from the term's lazy behavior or produces different graphs under different reduction orders.

Figures

Figures reproduced from arXiv: 2606.22908 by Bo Yang.

Figure 1
Figure 1. Figure 1: The subproblem call graph of ed on 𝑎 = ab, 𝑏 = cd, generated by running the interpreter. Each node is one of the (𝑚+1) (𝑛+1) = 9 distinct suffix-pair states, labeled with its edit distance; rows are suffixes of 𝑎, columns suffixes of 𝑏. An interior state calls the three subproblems it points to. Because a suffix is a shared sub-term, a subproblem reached along several paths is one interned state, here the … view at source ↗
Figure 2
Figure 2. Figure 2: The graph the interpreter returns for 𝑟 = 𝑌 (cons 0), generated by running the interpreter. The states it tables are 𝑟 and the self-application 𝑊 𝑊 (with 𝑊 = 𝜆𝑥. cons 0 (𝑥 𝑥)), each exposing the cons cell with head 0; 𝑟 leads in, and the tail of 𝑊 𝑊 is 𝑊 𝑊 again, the back edge the interpreter closes on re-entering that state, the highlighted self-loop. The finite cyclic graph unfolds to 0, 0, 0, . . . , wh… view at source ↗
Figure 3
Figure 3. Figure 3: The graph the interpreter returns for Ω = (𝜆𝑥. 𝑥 𝑥) (𝜆𝑥. 𝑥 𝑥), generated by running the interpreter. The single state’s head reduction contracts to the same interned term, so the interpreter re-enters it on the stack with no layer exposed and decides it ⊥, in finite time, where ordinary reduction would contract forever. Stepping through the interpreter. Solving Ω (Algorithm 1) puts it on the stack and runs… view at source ↗
read the original abstract

Representing and transforming cyclic and infinite data in the pure $\lambda$-calculus normally requires an added recursion construct, a \texttt{letrec}, a $\mu$-binder, or a built-in $Y$ for graph reduction, and sharing the repeated work of a memoized or dynamic-programming function normally requires an impure cache. We show that no extension is needed. We apply tabling, the standard method for solving a least-fixpoint equation, to weak-head reduction; this defines a new operational semantics for the pure $\lambda$-calculus that keeps each term's standard lazy meaning. A term that reaches finitely many distinct states comes out as a finite graph, possibly cyclic; the calculus stays pure, and the graph is sound and independent of reduction order. We implemented this operational semantics as a $\lambda$-calculus interpreter. It does dynamic programming automatically, sharing repeated subproblems with no memoization table. It creates and transforms cyclic graphs with no added recursion construct. And it decides an unproductive loop, returning $\bot$ for $\Omega$ in finite time. What the evaluator returns is a graph, so the $\lambda$-calculus becomes a DSL for graph computation: the memo table of dynamic programming, the transposition table of game search, and the visited set of graph reachability and points-to analysis are all tabling on state identity, and none of them is written by hand. Compilation is one more such problem: we write a bootstrap compiler that compiles its own source, all as a pure $\lambda$-term.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The paper claims that applying tabling (as a method for solving least-fixpoint equations) to weak-head reduction defines a new operational semantics for the pure λ-calculus. This semantics produces finite (possibly cyclic) graphs for terms reaching finitely many distinct states, preserves each term's standard lazy meaning, remains independent of reduction order, enables automatic dynamic programming and graph computation (e.g., memo tables, transposition tables) without extensions or impurity, decides unproductive loops such as Ω by returning ⊥ in finite time, and supports writing a bootstrap compiler as a pure λ-term.

Significance. If the central claims hold, the result would allow cyclic data structures and memoized computations to be represented and transformed directly in the pure λ-calculus without letrec, μ-binders, or built-in Y, turning the calculus into a DSL for graph algorithms. The reported implementation of an interpreter and a self-compiling bootstrap compiler as a pure λ-term would constitute concrete demonstrations of practicality. However, the absence of any formal rules, confluence arguments, or preservation proofs in the manuscript makes the significance conditional on future verification of the soundness and order-independence properties.

major comments (2)
  1. [Abstract] Abstract and operational semantics definition: the central claim that tabling on weak-head reduction yields graphs that are 'sound and independent of reduction order' and 'preserve each term's standard lazy meaning' is load-bearing, yet the manuscript supplies no formal transition rules for state-identity comparison, no confluence proof, and no derivation establishing preservation of lazy denotations.
  2. [Implementation] Implementation description: the claim that the approach 'decides an unproductive loop, returning ⊥ for Ω in finite time' and performs dynamic programming 'with no memoization table' requires an explicit account of how 'seen states' are identified and updated; without this, it is impossible to verify that the semantics avoids meta-level effects or remains order-independent.
minor comments (1)
  1. The abstract would benefit from a short pointer to the section containing the formal tabling rules.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful review and for identifying the need for explicit formalization to support the central claims. We address each major comment below and will revise the manuscript to incorporate the requested details.

read point-by-point responses

  1. Referee: [Abstract] Abstract and operational semantics definition: the central claim that tabling on weak-head reduction yields graphs that are 'sound and independent of reduction order' and 'preserve each term's standard lazy meaning' is load-bearing, yet the manuscript supplies no formal transition rules for state-identity comparison, no confluence proof, and no derivation establishing preservation of lazy denotations.

    Authors: The observation is correct: the current manuscript presents the semantics at a conceptual level in the abstract and introductory sections without supplying the explicit transition rules or proofs. In the revision we will add a new section that defines the tabling operational semantics via formal transition rules, including the mechanism for state-identity comparison on λ-terms. We will also include a proof sketch establishing confluence of the resulting relation and preservation of the standard lazy denotational semantics, building on the known properties of weak-head reduction and tabling as a least-fixpoint solver. revision: yes

  2. Referee: [Implementation] Implementation description: the claim that the approach 'decides an unproductive loop, returning ⊥ for Ω in finite time' and performs dynamic programming 'with no memoization table' requires an explicit account of how 'seen states' are identified and updated; without this, it is impossible to verify that the semantics avoids meta-level effects or remains order-independent.

    Authors: We agree that the implementation description is currently too high-level on the state-identification mechanism. The revision will expand the relevant section to give a precise account of how states are represented, how identity is decided (via a pure λ-term encoding of term equivalence), and how the table is updated during reduction. This will make explicit that the construction stays inside the pure calculus, inherits order-independence from the underlying tabling algorithm, and detects the unproductive loop for Ω by reaching a fixed point in finite steps. revision: yes

Circularity Check

0 steps flagged

No circularity: semantics derived from standard tabling on weak-head reduction

full rationale

The paper defines a new operational semantics by applying the standard technique of tabling (least-fixpoint solving) directly to weak-head reduction in the pure λ-calculus. This produces graphs for terms with finite distinct states without extensions or memo tables. No self-definitional equations, fitted parameters renamed as predictions, or load-bearing self-citations appear in the derivation chain. The soundness, laziness preservation, and reduction-order independence are claimed as consequences of the tabling construction itself rather than presupposed inputs. The approach is self-contained against external λ-calculus benchmarks; the implementation is presented as validation, not as the source of the result.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Based solely on the abstract; no explicit free parameters, ad-hoc axioms, or invented entities are described. The work relies on standard lambda-calculus reduction and the least-fixpoint properties of tabling.

pith-pipeline@v0.9.1-grok · 5800 in / 1016 out tokens · 27864 ms · 2026-06-29T04:57:57.523724+00:00 · methodology

Review history (2 revisions) →

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

25 extracted references · 20 canonical work pages

  1. [1]

    doi:10.1006/inco.1993.1044 Roberto M

    Full Abstraction in the Lazy Lambda Calculus.Information and Computation 105, 2 (1993), 159–267. doi:10.1006/inco.1993.1044 Roberto M. Amadio and Luca Cardelli

    work page doi:10.1006/inco.1993.1044 1993

  2. [2]

    doi:10.1145/155183.155231 Lars Ole Andersen

    Subtyping Recursive Types.ACM Transactions on Programming Languages and Systems15, 4 (1993), 575–631. doi:10.1145/155183.155231 Lars Ole Andersen. 1994.Program Analysis and Specialization for the C Programming Language. Ph. D. Dissertation. DIKU, University of Copenhagen. DIKU Report 94/19. Zena M. Ariola and Matthias Felleisen

    work page doi:10.1145/155183.155231 1993

  3. [3]

    doi:10.1017/S0956796897002724 Zena M

    The Call-by-Need Lambda Calculus.Journal of Functional Programming7, 3 (1997), 265–301. doi:10.1017/S0956796897002724 Zena M. Ariola and Jan Willem Klop

    work page doi:10.1017/s0956796897002724 1997

  4. [4]

    doi:10.1006/inco.1997.2651 Stefan Banach

    Lambda Calculus with Explicit Recursion.Information and Computation139, 2 (1997), 154–233. doi:10.1006/inco.1997.2651 Stefan Banach

    work page doi:10.1006/inco.1997.2651 1997

  5. [5]

    doi:10.4064/fm-3-1-133-181 12 Bo Yang Henk P

    Sur les opérations dans les ensembles abstraits et leur application aux équations intégrales.Fundamenta Mathematicae3 (1922), 133–181. doi:10.4064/fm-3-1-133-181 12 Bo Yang Henk P. Barendregt. 1984.The Lambda Calculus: Its Syntax and Semantics(revised ed.). Studies in Logic and the Foundations of Mathematics, Vol

    work page doi:10.4064/fm-3-1-133-181 1922

  6. [6]

    doi:10.1007/BF00264249 Michael Brandt and Fritz Henglein

    Using Circular Programs to Eliminate Multiple Traversals of Data.Acta Informatica21, 3 (1984), 239–250. doi:10.1007/BF00264249 Michael Brandt and Fritz Henglein

    work page doi:10.1007/bf00264249 1984

  7. [7]

    doi:10.3233/fi-1998-33401 Martin Bravenboer and Yannis Smaragdakis

    Coinductive Axiomatization of Recursive Type Equality and Subtyping.Fundamenta Informaticae33, 4 (1998), 309–338. doi:10.3233/fi-1998-33401 Martin Bravenboer and Yannis Smaragdakis

    work page doi:10.3233/fi-1998-33401 1998

  8. [8]

    In Proceedings of the 24th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA)

    Strictly Declarative Specification of Sophisticated Points-to Analyses. In Proceedings of the 24th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA). ACM, 243–262. doi:10.1145/1640089.1640108 Randal E. Bryant

    work page doi:10.1145/1640089.1640108

  9. [9]

    Comput.C-35, 8 (1986), 677–691

    Graph-Based Algorithms for Boolean Function Manipulation.IEEE Trans. Comput.C-35, 8 (1986), 677–691. doi:10.1109/TC.1986.1676819 Weidong Chen and David S. Warren

    work page doi:10.1109/tc.1986.1676819 1986

  10. [10]

    ACM43, 1 (1996), 20–74

    Tabled Evaluation with Delaying for General Logic Programs.J. ACM43, 1 (1996), 20–74. doi:10.1145/227595.227597 Alain Colmerauer

    work page doi:10.1145/227595.227597 1996

  11. [11]

    doi:10.1016/0304-3975(83)90059-2 Andy Gill

    Fundamental Properties of Infinite Trees.Theoretical Computer Science25, 2 (1983), 95–169. doi:10.1016/0304-3975(83)90059-2 Andy Gill

    work page doi:10.1016/0304-3975(83)90059-2 1983

  12. [12]

    InProceedings of the 2nd ACM SIGPLAN Symposium on Haskell

    Type-Safe Observable Sharing in Haskell. InProceedings of the 2nd ACM SIGPLAN Symposium on Haskell. ACM, 117–128. doi:10.1145/1596638.1596653 Vladimir I Levenshtein et al

    work page doi:10.1145/1596638.1596653

  13. [13]

    Jean-Jacques Lévy

    Soviet Union, 707–710. Jean-Jacques Lévy. 1978.Réductions correctes et optimales dans le lambda-calcul. Ph. D. Dissertation. Université Paris VII. Thèse de doctorat d’État. Giuseppe Longo

    1978

  14. [14]

    doi:10.1016/0168-0072(83)90030-1 Torben Æ

    Set-Theoretical Models of 𝜆-Calculus: Theories, Expansions, Isomorphisms.Annals of Pure and Applied Logic24, 2 (1983), 153–188. doi:10.1016/0168-0072(83)90030-1 Torben Æ. Mogensen

    work page doi:10.1016/0168-0072(83)90030-1 1983

  15. [15]

    doi:10.1017/S0956796800000423 F

    Efficient Self-Interpretation in Lambda Calculus.Journal of Functional Programming2, 3 (1992), 345–364. doi:10.1017/S0956796800000423 F. Lockwood Morris. 1978.On List Structures and Their Use in the Programming of Unification. Technical Report 4-78. Syracuse University. https://surface.syr.edu/cgi/viewcontent.cgi?article=1004&context=eecs_techreports John...

    work page doi:10.1017/s0956796800000423 1992

  16. [16]

    doi:10.1023/A:1010027404223 Reprint of the 1972 ACM National Conference paper that introduced defunctionalization

    Definitional Interpreters for Higher-Order Programming Languages.Higher-Order and Symbolic Computation11, 4 (1998), 363–397. doi:10.1023/A:1010027404223 Reprint of the 1972 ACM National Conference paper that introduced defunctionalization. Hisao Tamaki and Taisuke Sato

    work page doi:10.1023/a:1010027404223 1998

  17. [17]

    InThird International Conference on Logic Program- ming (ICLP) (Lecture Notes in Computer Science, Vol

    OLD Resolution with Tabulation. InThird International Conference on Logic Program- ming (ICLP) (Lecture Notes in Computer Science, Vol. 225). Springer, 84–98. doi:10.1007/3-540-16492-8_66 M. H. van Emden and R. A. Kowalski

    work page doi:10.1007/3-540-16492-8_66

  18. [18]

    ACM23, 4 (1976), 733–742

    The Semantics of Predicate Logic as a Programming Language.J. ACM23, 4 (1976), 733–742. doi:10.1145/321978.321991 Christopher P. Wadsworth. 1971.Semantics and Pragmatics of the Lambda-Calculus. Ph. D. Dissertation. University of Oxford. Robert A. Wagner and Michael J. Fischer

    work page doi:10.1145/321978.321991 1976

  19. [19]

    ACM21, 1 (1974), 168–173

    The String-to-String Correction Problem.J. ACM21, 1 (1974), 168–173. doi:10.1145/321796.321811 Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, and Pavel Panchekha

    work page doi:10.1145/321796.321811 1974

  20. [20]

    doi:10.1145/3434304 Bo Yang

    egg: Fast and Extensible Equality Saturation.Proceedings of the ACM on Programming Languages5, POPL (2021), 1–29. doi:10.1145/3434304 Bo Yang

    work page doi:10.1145/3434304 2021

  21. [21]

    Better Together: Unifying Datalog and Equality Saturation.Proceedings of the ACM on Programming Languages7, PLDI (2023), 468–492. doi:10.1145/3591239 A Proofs This appendix proves the three claims of Section 2: the evaluator is sound (the graph it builds unfolds to the Lévy–Longo tree), the solution is unique (least equals greatest fixpoint), and the eval...

    work page doi:10.1145/3591239 2023

  22. [22]

    Proof of Theorems A.9 and A.10

    Theorem A.10 (Termination).When the silent head reduction from each reachable term termi- nates, exposing a constructor or returning to a visited term, the evaluator returns a finite graph at 𝑡0 iff finitely many terms are reachable from 𝑡0, and that graph, possibly cyclic, unfolds to the rational Lévy–Longo tree. Proof of Theorems A.9 and A.10. The prere...

    1996

  23. [23]

    Then out(𝑡) is defined for every reachable 𝑡: each silent run either exposes a constructor or revisits a term on a deterministic path and returns ⊥, in either case halting

    Termination (Theorem A.10).Suppose finitely many terms are reachable from 𝑡0 and the silent head reduction from each terminates. Then out(𝑡) is defined for every reachable 𝑡: each silent run either exposes a constructor or revisits a term on a deterministic path and returns ⊥, in either case halting. It remains to show the outer loop halts, that is, that ...

    1983

  24. [24]

    Interpreted versus compiled execution. Each row runs one application interpreted (interned term nodes) against compiled (interned Thunks and closures).Speedup,memory ratio, andtabled ratiocompare interpreted to compiled; a ratio above one means the compiled form wins. Time and peak memory are a single measured snapshot on CPython 3.11, and the compiled co...

    1998

  25. [25]

    Dynamic programming.A perfect binary tree of depth 𝑛 whose nodes share both children is a graph of𝑛+1states that unfolds to2 𝑛 leaves: node=𝜆𝑙 .𝜆𝑟 .𝜆𝑚.𝜆𝑓

    folds to a finite circular list, one cell holding 𝑓 0whose tail points to itself; on a finite list it is the textbook map. Dynamic programming.A perfect binary tree of depth 𝑛 whose nodes share both children is a graph of𝑛+1states that unfolds to2 𝑛 leaves: node=𝜆𝑙 .𝜆𝑟 .𝜆𝑚.𝜆𝑓 . 𝑚 𝑙 𝑟,leaf=𝜆𝑣 .𝜆𝑚.𝜆𝑓 . 𝑓 𝑣, any=𝑌 𝜆self.𝜆𝑡 . 𝑡(𝜆𝑙 .𝜆𝑟 .or(self𝑙) (self𝑟)) (𝜆𝑣 ...

    1994