Organizations: The School of Interdisciplinary Research, Indian Institute of Technology (IIT) Delhi, Robert Bosch GmbH, India · Huawei Noah’s Ark Lab · Huawei Noah’s Ark · UCL Centre for Artificial Intelligence
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.
Figures & tables
Figure 1: A summary of our results comparing λ-RLMs to base LLMs and recursive LLMs. Those results demonstrate improvements reaching +21.9 in accuracy, with 4.1× in latency reductions.
Combinator
Type Signature
Description
Split
Σ∗×N→[Σ∗]
Partition a string into k contiguous chunks
Peek
Σ∗×N2→Σ∗
Extract a substring by start and end position
Map
(α→β)×[α]→[β]
Apply a function to every element of a list
Filter
(α→B)×[α]→[α]
Retain elements satisfying a predicate
Reduce
(β×β→β)×[β]→β
Fold a list into a single value via a binary operator
Concat
[Σ∗]→Σ∗
Join a list of strings into one string
Table 1: A compact combinator library L and examples of task-specific execution plans.