Table of Contents
Fetching ...

The $\mathbf{Y}$-Combinator for LLMs: Solving Long-Context Rot with $λ$-Calculus

Amartya Roy, Rasul Tutunov, Xiaotong Ji, Matthieu Zimmer, Haitham Bou-Ammar

Abstract

LLMs are increasingly used as general-purpose reasoners, but long inputs remain bottlenecked by a fixed context window. Recursive Language Models (RLMs) address this by externalising the prompt and recursively solving subproblems. Yet existing RLMs depend on an open-ended read-eval-print loop (REPL) in which the model generates arbitrary control code, making execution difficult to verify, predict, and analyse. We introduce $λ$-RLM, a framework for long-context reasoning that replaces free-form recursive code generation with a typed functional runtime grounded in $λ$-calculus. It executes a compact library of pre-verified combinators and uses neural inference only on bounded leaf subproblems, turning recursive reasoning into a structured functional program with explicit control flow. We show that $λ$-RLM admits formal guarantees absent from standard RLMs, including termination, closed-form cost bounds, controlled accuracy scaling with recursion depth, and an optimal partition rule under a simple cost model. Empirically, across four long-context reasoning tasks and nine base models, $λ$-RLM outperforms standard RLM in 29 of 36 model-task comparisons, improves average accuracy by up to +21.9 points across model tiers, and reduces latency by up to 4.1x. These results show that typed symbolic control yields a more reliable and efficient foundation for long-context reasoning than open-ended recursive code generation. The complete implementation of $λ$-RLM, is open-sourced for the community at: https://github.com/lambda-calculus-LLM/lambda-RLM.

The $\mathbf{Y}$-Combinator for LLMs: Solving Long-Context Rot with $λ$-Calculus

Abstract

LLMs are increasingly used as general-purpose reasoners, but long inputs remain bottlenecked by a fixed context window. Recursive Language Models (RLMs) address this by externalising the prompt and recursively solving subproblems. Yet existing RLMs depend on an open-ended read-eval-print loop (REPL) in which the model generates arbitrary control code, making execution difficult to verify, predict, and analyse. We introduce -RLM, a framework for long-context reasoning that replaces free-form recursive code generation with a typed functional runtime grounded in -calculus. It executes a compact library of pre-verified combinators and uses neural inference only on bounded leaf subproblems, turning recursive reasoning into a structured functional program with explicit control flow. We show that -RLM admits formal guarantees absent from standard RLMs, including termination, closed-form cost bounds, controlled accuracy scaling with recursion depth, and an optimal partition rule under a simple cost model. Empirically, across four long-context reasoning tasks and nine base models, -RLM outperforms standard RLM in 29 of 36 model-task comparisons, improves average accuracy by up to +21.9 points across model tiers, and reduces latency by up to 4.1x. These results show that typed symbolic control yields a more reliable and efficient foundation for long-context reasoning than open-ended recursive code generation. The complete implementation of -RLM, is open-sourced for the community at: https://github.com/lambda-calculus-LLM/lambda-RLM.
Paper Structure (30 sections, 9 theorems, 26 equations, 2 figures, 10 tables, 6 algorithms)

This paper contains 30 sections, 9 theorems, 26 equations, 2 figures, 10 tables, 6 algorithms.

Key Result

Theorem 1

Under Assumption asm:regularity(A1-A2), for any input $P \in \Sigma^*$ with $|P| = n < \infty$, the function $\Phi$ in Algorithm alg:executor terminates when executed in the REPL. Moreover, the total number of $\mathcal{M}$ invocations is exactly:

Figures (2)

  • Figure 1: A summary of our results comparing $\lambda\text{-}\textsf{RLMs}$ to base LLMs and recursive LLMs. Those results demonstrate improvements reaching $\textbf{+21.9}$ in accuracy, with $\textbf{4.1}\times$ in latency reductions.
  • Figure : Pairwise Tasks

Theorems & Definitions (26)

  • Definition 1: Fixed-Point Combinator
  • Definition 2: Base Language Model
  • Definition 3: Cost Function
  • Definition 4: Accuracy Decay
  • Definition 5: Composition Operator
  • Theorem 1: Termination
  • proof : Sketch; a complete proof is in Appendix \ref{['app:proofs']}
  • Remark 1
  • Theorem 2: Cost Bound
  • proof : Sketch; a complete proof is in Appendix \ref{['app:proofs']}
  • ...and 16 more