pith. sign in

arxiv: 2606.23573 · v2 · pith:HY4K6QLDnew · submitted 2026-06-22 · 💻 cs.LO

An Infinitary Lambda Calculus with Global Trace Condition (Extended Abstract)

Stefano Berardi , Ugo de' Liguoro , Daisuke Kimura , Daniel Osorio-Valencia This is my paper

Pith reviewed 2026-06-26 06:20 UTC · model grok-4.3

classification 💻 cs.LO
keywords infinitary lambda calculusglobal trace conditionstrong convergencesystem Tcyclic proofsnormalizationtotal functions
0
0 comments X

The pith

Any infinite reduction of a well-typed term satisfying the Global Trace Condition is strongly convergent.

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

The paper extends the infinitary lambda calculus with constants for zero, successor and conditionals, together with a type system modeled on Goedel's System T. It adapts the Global Trace Condition from cyclic proof theory and proves that this condition forces every infinite reduction of a well-typed term to converge strongly. A direct corollary is that every closed term of type Nat reaches a numeral under any reduction performed level by level. The same condition also yields Church-Rosser in the limit and, for regular terms, exact equivalence with the total functions of Das's cyclic System T.

Core claim

The central claim is that any infinite reduction of a well-typed term satisfying the Global Trace Condition is strongly convergent. As a corollary, any closed term of type Nat reduces to some numeral through any reduction by levels. The authors argue that Church-Rosser in the limit holds for the calculus and that, when restricted to regular terms, it defines exactly the total functions of Das's Cyclic System T and hence of Goedel's System T.

What carries the argument

The Global Trace Condition (GTC), an adaptation from Brotherston and Simpson's cyclic proofs that tracks infinite descent of traces along reduction paths to enforce convergence.

If this is right

  • Any infinite reduction of a well-typed term satisfying the GTC is strongly convergent.
  • Any closed term of type Nat reduces to some numeral through any reduction by levels.
  • The Church-Rosser property holds in the limit.
  • When restricted to regular terms the calculus defines exactly the total functions of Goedel's System T.

Where Pith is reading between the lines

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

  • The same trace condition could be tested on other infinitary calculi to obtain similar normalization results without additional typing restrictions.
  • Regular terms under this discipline correspond to the same class of total functions already known from System T, suggesting the infinitary setting adds no extra computational power once the trace condition is imposed.
  • The level-by-level reduction strategy for Nat terms offers a concrete way to extract numerals that might be adapted to other base types.

Load-bearing premise

The adaptation of the Global Trace Condition from cyclic proofs is correctly defined for this typed infinitary lambda calculus and is sufficient to imply strong convergence.

What would settle it

A concrete well-typed term that satisfies the stated Global Trace Condition yet possesses an infinite reduction sequence that fails to be strongly convergent.

read the original abstract

We consider an extension of the infinitary lambda calculus by Kennaway et al., with zero, successor, and conditional, and a type system akin to Goedel's system T. For terms that can be typed in this system, we define the Global Trace Condition (GTC), adapting the concept from Brotherston and Simpson's Cyclic Proofs, and show that any infinite reduction of a well-typed term satisfying the GTC is strongly convergent. As a corollary, we obtain the proof that any closed term of type Nat reduces to some numeral through any reduction by levels. We argue that the Church-Rosser in the limit holds for our calculus and, when restricted to regular terms, the calculus defines exactly the total functions defined in Das's Cyclic System T (an infinitary version of System T without $\lambda$), and hence in Goedel's System T.

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 extends the infinitary lambda calculus of Kennaway et al. with zero, successor, and conditional, along with a type system similar to Gödel's System T. It defines the Global Trace Condition (GTC) by adapting the notion from Brotherston and Simpson's cyclic proofs, and states that any infinite reduction of a well-typed term satisfying the GTC is strongly convergent. A corollary is that any closed term of type Nat reduces to some numeral through any reduction by levels. The paper also claims that Church-Rosser in the limit holds, and that when restricted to regular terms, the calculus defines exactly the total functions from Das's Cyclic System T, hence from Gödel's System T.

Significance. If the central theorem is correct, this work offers a promising link between infinitary lambda calculus and cyclic proof theory, providing a trace-based condition to guarantee strong convergence for typed terms. The corollary on Nat terms and the equivalence to System T functions would be notable contributions to the study of normalization and computability in infinitary settings. The adaptation of GTC is a key innovation if properly justified.

major comments (2)
  1. Abstract: the main theorem asserting strong convergence under GTC is stated without any proof details, derivation steps, or counter-example verification, making it impossible to assess the soundness of the GTC adaptation or the convergence argument from the provided manuscript.
  2. Abstract (GTC definition and main theorem): the definition of the Global Trace Condition is described only at a high level as an adaptation from cyclic proofs; without the specific formulation for typed redexes or the argument showing that violation of convergence produces a GTC-violating trace, the load-bearing claim cannot be evaluated.
minor comments (1)
  1. The manuscript is labeled as an extended abstract, which explains the brevity but limits the ability to fully evaluate the results for journal publication.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their comments. This submission is an extended abstract, which by design presents results at a high level without full proofs. We address the major comments point by point below, noting that detailed arguments appear in the complete version of the paper.

read point-by-point responses

  1. Referee: Abstract: the main theorem asserting strong convergence under GTC is stated without any proof details, derivation steps, or counter-example verification, making it impossible to assess the soundness of the GTC adaptation or the convergence argument from the provided manuscript.

    Authors: The observation is correct for an extended abstract: the main theorem (any infinite reduction of a well-typed term satisfying the GTC is strongly convergent) is stated without derivation steps. The proof proceeds by contraposition, constructing from a non-strongly-convergent reduction an infinite trace that fails to descend in the type order, violating the GTC. Full details, including the precise inductive argument on typed redexes, are reserved for the complete paper. revision: no

  2. Referee: Abstract (GTC definition and main theorem): the definition of the Global Trace Condition is described only at a high level as an adaptation from cyclic proofs; without the specific formulation for typed redexes or the argument showing that violation of convergence produces a GTC-violating trace, the load-bearing claim cannot be evaluated.

    Authors: The GTC is obtained by lifting the global trace condition of Brotherston and Simpson to the typed setting: each redex occurrence is annotated with its type, and a trace is a sequence of such occurrences linked by reduction steps; the condition requires that every infinite trace eventually descends in the type order (Nat > Bool, etc.). The argument that non-convergence yields a GTC violation constructs the trace by selecting, at each step, a position whose residual does not converge, producing an infinite non-descending trace. The precise formulation for the constants (zero, successor, conditional) and the descent measure appear in the full manuscript. revision: no

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The paper introduces a novel adaptation of the Global Trace Condition from external prior work (Brotherston and Simpson) and states a theorem establishing strong convergence for well-typed terms under this condition, with the Nat corollary derived directly from it. No equations, definitions, or derivations in the provided abstract or described manuscript reduce the central claims to self-definitions, fitted parameters renamed as predictions, or load-bearing self-citations; the proof is presented as independent of the paper's own inputs. The derivation chain is therefore self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

The central claim depends on the correctness of the GTC adaptation and the typing discipline; these are introduced in the paper rather than derived from external benchmarks.

axioms (2)
  • standard math Standard infinitary lambda calculus reduction rules from Kennaway et al.
    The paper explicitly builds on this prior calculus as its base.
  • domain assumption The type system is akin to Goedel's System T
    Used to restrict the terms to which GTC applies.
invented entities (1)
  • Global Trace Condition (GTC) no independent evidence
    purpose: Condition on infinite reductions that forces strong convergence
    Newly defined by adapting Brotherston and Simpson; no independent evidence outside the paper is supplied in the abstract.

pith-pipeline@v0.9.1-grok · 5685 in / 1415 out tokens · 25589 ms · 2026-06-26T06:20:43.393486+00:00 · methodology

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

31 extracted references · 14 canonical work pages

  1. [1]

    1972 , type =

    Jean-Yves Girard , title =. 1972 , type =

    1972

  2. [2]

    W. W. Tait , journal =. Intensional Interpretations of Functionals of Finite Type I , urldate =

  3. [3]

    Infinitary Rewriting: From Syntax to Semantics

    Kennaway, Richard and Severi, Paula and Sleep, Ronan and de Vries, Fer-Jan. Infinitary Rewriting: From Syntax to Semantics. Processes, Terms and Cycles: Steps on the Road to Infinity: Essays Dedicated to Jan Willem Klop on the Occasion of His 60th Birthday. 2005. doi:10.1007/11601548_11

    work page doi:10.1007/11601548_11 2005

  4. [4]

    doi:10.1006/inco.1997.2651 Stefan Banach

    Lambda Calculus with Explicit Recursion , journal =. 1997 , issn =. doi:https://doi.org/10.1006/inco.1997.2651 , url =

    work page doi:10.1006/inco.1997.2651 1997

  5. [5]

    Ariola and Stefan Blom , editor =

    Zena M. Ariola and Stefan Blom , editor =. Cyclic lambda calculi , booktitle =. 1997 , publisher =

    1997

  6. [6]

    An Alpha-Corecursion Principle for the Infinitary Lambda Calculus , booktitle =

    Alexander Kurz and Daniela Petrisan and Paula Severi and Fer. An Alpha-Corecursion Principle for the Infinitary Lambda Calculus , booktitle =. 2012 , url =. doi:10.1007/978-3-642-32784-1\_8 , timestamp =

    work page doi:10.1007/978-3-642-32784-1 2012

  7. [7]

    Kennaway and Jan Willem Klop and M.R

    J.R. Kennaway and Jan Willem Klop and M.R. Sleep and F.J. Infinitary lambda calculus , journal =. 1997 , issn =. doi:https://doi.org/10.1016/S0304-3975(96)00171-5 , url =

    work page doi:10.1016/s0304-3975(96)00171-5 1997

  8. [8]

    2003 , isbn =

    Terese , title =. 2003 , isbn =

    2003

  9. [9]

    Kennaway and F-J

    J.R. Kennaway and F-J. de Vries , title =. Term rewriting systems , editor =. 2003 , volume =

    2003

  10. [10]

    2013 , doi =

    Expressibility in the Lambda Calculus with Letrec , author =. 2013 , doi =

    2013

  11. [11]

    2013 , doi =

    Expressibility in the Lambda Calculus with mu , author =. 2013 , doi =

    2013

  12. [12]

    2016 , url =

    Unfolding Semantics of the Untyped lambda-Calculus with letrec , author =. 2016 , url =

    2016

  13. [13]

    Proceedings of the ACM on Programming Languages, 2021 , doi =

    Denis Kuperberg and Laureline Pinault and Damien Pous , title =. Proceedings of the ACM on Programming Languages, 2021 , doi =

    2021

  14. [14]

    CoRR , volume =

    Anupam Das , title =. CoRR , volume =. 2020 , url =

    2020

  15. [15]

    James Brotherston and Alex Simpson , title =. J. Log. Comput. , volume =. 2011 , url =. doi:10.1093/LOGCOM/EXQ052 , timestamp =

    work page doi:10.1093/logcom/exq052 2011

  16. [16]

    2006 , address =

    Sequent calculus proof systems for inductive definitions , author =. 2006 , address =

    2006

  17. [17]

    2006 , url =

    Gilles Dowek , title =. 2006 , url =

    2006

  18. [18]

    1989 , publisher =

    Proofs and types , author=. 1989 , publisher =

    1989

  19. [19]

    Jones and Amir M

    Chin Soon Lee and Neil D. Jones and Amir M. Ben. The size-change principle for program termination , booktitle =. 2001 , url =. doi:10.1145/360204.360210 , timestamp =

    work page doi:10.1145/360204.360210 2001

  20. [20]

    6th International Conference on Formal Structures for Computation and Deduction,

    Anupam Das , editor =. 6th International Conference on Formal Structures for Computation and Deduction,. 2021 , url =. doi:10.4230/LIPICS.FSCD.2021.29 , timestamp =

    work page doi:10.4230/lipics.fscd.2021.29 2021

  21. [21]

    Cyclic Implicit Complexity , booktitle =

    Gianluca Curzi and Anupam Das , editor =. Cyclic Implicit Complexity , booktitle =. 2022 , url =. doi:10.1145/3531130.3533340 , timestamp =

    work page doi:10.1145/3531130.3533340 2022

  22. [22]

    Gianluca Curzi and Anupam Das , editor =. 31st. 2023 , url =. doi:10.4230/LIPICS.CSL.2023.16 , timestamp =

    work page doi:10.4230/lipics.csl.2023.16 2023

  23. [23]

    Structure-aware lower bounds and broadening the horizon of tractability for QBF

    Gianluca Curzi and Anupam Das , title =. 38th Annual. 2023 , url =. doi:10.1109/LICS56636.2023.10175772 , timestamp =

    work page doi:10.1109/lics56636.2023.10175772 2023

  24. [24]

    The Lambda Calculus: Its Syntax and Semantics , publisher =

    Hendrik Barendregt , editor =. The Lambda Calculus: Its Syntax and Semantics , publisher =

  25. [25]

    A Generic Cyclic Theorem Prover

    James Brotherston and Nikos Gorogiannis and Rasmus Petersen. A Generic Cyclic Theorem Prover. Programming Languages and Systems. 2012

    2012

  26. [26]

    Rowe, Reuben N. S. and Brotherston, James , title =. Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs , pages =. 2017 , isbn =. doi:10.1145/3018610.3018623 , abstract =

    work page doi:10.1145/3018610.3018623 2017

  27. [27]

    Cohen, Liron and Jabarin, Adham and Popescu, Andrei and Rowe, Reuben N. S. , title =. Proc. ACM Program. Lang. , month = jan, articleno =. 2024 , issue_date =. doi:10.1145/3632888 , abstract =

    work page doi:10.1145/3632888 2024

  28. [28]

    Cohen, Liron and Rowe, Reuben N. S. and Shaked, Matan. Cyclone: A Heterogeneous Tool for Verifying Infinite Descent. Tools and Algorithms for the Construction and Analysis of Systems. 2025

    2025

  29. [29]

    Itzhaky, Shachar and Peleg, Hila and Polikarpova, Nadia and Rowe, Reuben N. S. and Sergey, Ilya , title =. Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation , pages =. 2021 , isbn =. doi:10.1145/3453483.3454087 , abstract =

    work page doi:10.1145/3453483.3454087 2021

  30. [30]

    and Brotherston J

    Tellez, G. and Brotherston J. , title =. J. Autom. Reason. 64(3) , pages =. 2020 , doi =

    2020

  31. [31]

    E-Cyclist: Implementation of an Efficient Validation of FOLID Cyclic Induction Reasoning , volume=

    Stratulat, Sorin , year=. E-Cyclist: Implementation of an Efficient Validation of FOLID Cyclic Induction Reasoning , volume=. doi:10.4204/eptcs.342.11 , journal=

    work page doi:10.4204/eptcs.342.11