arXiv subjects

Rémy Cerda

Publications and source records attributed to Rémy Cerda.

6 recordsLinked to original sources

arXiv2026

Staying Productive Under the Palm Trees: On Graded Coeffect Typing in the Tropical Semiring

We show that the tropical semiring over the natural numbers, when used as the grading space in graded coeffect typing, faithfully models the passage of time while simultaneously guaranteeing productivity of well-typed programs. A grade a, when assigned to a function parameter, indicates that the parameter is not necessarily available immediately, but will become available after a time steps. We investigate this idea through two formal systems. We first introduce a graded type system featuring recursive and polymorphic types, and show that, in this setting, a natural restriction on recursive types is sufficient to guarantee productivity, while still allowing the definition of streams and recursive programs on them. In particular, we prove that Nakano's later modality can be embedded directly into our system. We then show that tropical grading naturally suggests a novel form of intersection typing, in which the role traditionally played by sets or multisets of types is instead taken by "timed" sets, i.e., functions assigning to each type A the earliest time, represented as a grade, from which the underlying term is available with type A. For the resulting system, we prove not only that productivity is guaranteed, but that it is also characterized: the typable terms are exactly those with hereditarily head normal forms. Remarkably, the system is recursion-theoretically optimal, i.e., typability can be directly proved to be a $Π_0^2$ property in the arithmetical hierarchy.

cs.LO↗

arXiv2026

Compression for Coinductive Rewriting and the Cut-Elimination of Non-Wellfounded Proofs

We introduce a generic presentation of "syntactic objects built by mixed induction and coinduction" encompassing all standard kinds of infinitary terms, as well as derivation trees in non-wellfounded proof systems. We then define a coinductive notion of infinitary rewriting of such objects, which is equivalent to the original presentation of infinitary rewriting relying on metric convergence and ordinal-indexed sequences of rewriting steps. This provides a unified coinductive presentation of e.g. first-order infinitary rewriting, infinitary λ-calculi, and cut-elimination in non-wellfounded proofs. We then formulate and study the coinductive counterpart of compression, i.e. the property of an infinitary rewriting system such that all rewriting sequences of any ordinal length can be "compressed" to equivalent sequences of length at most ω(which ensures that they can be finitely approximated). We characterise compression in our generic setting for coinductive rewriting, "factorising" the part of the proof that can be performed at this level of generality. Our proof is fully coinductive, avoiding any detour via rewriting sequences. Finally we focus on the non-wellfounded proof system \muMALL\infty for multiplicative-additive linear logic with fixed points, and we put our results to work in order to prove that compression holds for cut-elimination in this setting, which is a key lemma of several extensions of cut-elimination to similar systems.

cs.LO↗

arXiv2026

How to play the Accordion: Uniformity and the (non-)conservativity of the linear approximation of the λ-calculus (extended version)

Twenty years after its introduction by Ehrhard and Regnier, differentiation in $λ$-calculus and in linear logic is now a celebrated tool. In particular, it allows to establish a Taylor expansion formula for various $λ$-calculi, hence providing a theory of linear approximations for these calculi. In the pure $λ$-calculus, the linear approximants of $λ$-terms supporting this Taylor expansion are the terms of a so-called resource calculus, which is equipped with a finitary (strongly normalising) reduction; and the efficiency of this linear approximation is expressed by results stating that the (possibly) infinitary $β$-reduction of $λ$-terms is simulated by the reduction of their Taylor expansions, which is induced by the iterated reduction of resource terms. In terms of rewriting systems, resource reduction (operating on infinite linear combinations of Taylor approximants) is an extension of $β$-reduction. In this article, we address the converse property, conservativity: do all reductions between Taylor expansions arise from actual $β$-reductions? We show that if we restrict the setting to finite terms and $β$-reduction sequences, then the linear approximation is conservative. However, as soon as one allows infinitary reduction sequences this property is broken. We design a counter-example, the Accordion. Then we show how restricting the reduction of the Taylor approximants allows to build a conservative extension of the $β$-reduction preserving good simulation properties; this restriction relies on uniformity, a property that was already at the core of Ehrhard and Regnier's pioneering work. Finally, we extend our work to $β\bot$-reductions, which play a key role in $λ$-calculus as they relate a $λ$-term to its Böhm tree.

cs.LO↗

arXiv2026

Ohana trees, linear approximation and multi-types for the $λ$I-calculus: No variable gets left behind or forgotten!

Although the $λ$I-calculus is a natural fragment of the $λ$-calculus, obtained by forbidding the erasure of arguments, its equational theories did not receive much attention. The reason is that all proper denotational models studied in the literature equate all non-normalizable $λ$I-terms, whence the associated theory is not very informative. The goal of this paper is to introduce a previously unknown theory of the $λ$I-calculus, induced by a notion of evaluation trees that we call "Ohana trees". The Ohana tree of a $λ$I-term is an annotated version of its Böhm tree, remembering all free variables that are hidden within its meaningless subtrees, or pushed into infinity along its infinite branches. We develop the associated theories of program approximation: the first approach -- more classic -- is based on finite trees and continuity, the second adapts Ehrhard and Regnier's Taylor expansion. We then prove a Commutation Theorem stating that the normal form of the Taylor expansion of a $λ$I-term coincides with the Taylor expansion of its Ohana tree. As a corollary, we obtain that the equality induced by Ohana trees is compatible with abstraction and application. Subsequently, we introduce a denotational model designed to capture the equality induced by Ohana trees. Although presented as a non-idempotent type system, our model is based on a suitably modified version of the relational semantics of the $λ$-calculus, which is known to yield proper models of the $λ$I-calculus when restricted to non-empty finite multisets. To track variables occurring in subterms that are hidden or pushed to infinity in the evaluation trees, we generalize the system in two ways: first, we reintroduce annotated versions of the empty multiset indexed by sets of variables; second, (...)

cs.LO↗

arXiv2025

Nominal Algebraic-Coalgebraic Data Types, with Applications to Infinitary Lambda-Calculi

Ten years ago, it was shown that nominal techniques can be used to design coalgebraic data types with variable binding, so that alpha-equivalence classes of infinitary terms are directly endowed with a corecursion principle. We introduce "mixed" binding signatures, as well as the corresponding type of mixed inductive-coinductive terms. We extend the aforementioned work to this setting. In particular, this allows for a nominal description of the sets Lambda_abc of abc-infinitary lambda-terms (for a, b, c in {0,1}) and of capture-avoiding substitution on alpha-equivalence classes of such terms.

cs.LO↗

arXiv2023

Finitary Simulation of Infinitary $β$-Reduction via Taylor Expansion, and Applications

Originating in Girard's Linear logic, Ehrhard and Regnier's Taylor expansion of $λ$-terms has been broadly used as a tool to approximate the terms of several variants of the $λ$-calculus. Many results arise from a Commutation theorem relating the normal form of the Taylor expansion of a term to its Böhm tree. This led us to consider extending this formalism to the infinitary $λ$-calculus, since the $Λ_{\infty}^{001}$ version of this calculus has Böhm trees as normal forms and seems to be the ideal framework to reformulate the Commutation theorem. We give a (co-)inductive presentation of $Λ_{\infty}^{001}$. We define a Taylor expansion on this calculus, and state that the infinitary $β$-reduction can be simulated through this Taylor expansion. The target language is the usual resource calculus, and in particular the resource reduction remains finite, confluent and terminating. Finally, we state the generalised Commutation theorem and use our results to provide simple proofs of some normalisation and confluence properties in the infinitary $λ$-calculus.

cs.LO↗