arXiv subjects

Lionel Vaux Auclair

Publications and source records attributed to Lionel Vaux Auclair.

9 recordsLinked to original sources

arXiv2026

An explicit shuffle construction of the homotopy span model of differential linear logic

We give a direct and explicit construction of the homotopy span model of linear logic originally formulated by Melliès using abstract homotopy theory in the Quillen category Cat of small categories equipped with its natural model structure. Following the principles of homotopy theory, the formulas and proofs of linear logic are interpreted in the model as small categories up to categorical equivalence, the notion of weak homotopy equivalence underlying the natural Quillen model structure on Cat. Here, we explain how the original interpretation of proofs as fibrant spans can be replaced by a more liberal interpretation of proofs as separately fibrant spans. This relaxation from fibrant spans to separately fibrant spans enables us to give a simple and intuitive description of the homotopy span model, where the axiom and cut links are interpreted as identity spans, and where the symmetries of the exponential modality are captured by a shuffle structure on the interpretation of proofs.

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

Extensional Taylor Expansion

We introduce a calculus of extensional resource terms. These are resource terms à la Ehrhard-Regnier, but in infinitely eta-long form. The calculus still retains a finite syntax and dynamics: in particular, we prove strong confluence and normalization. Then we define an extensional version of Taylor expansion, mapping ordinary lambda-terms to (possibly infinite) linear combinations of extensional resource terms: like in the ordinary case, the dynamics of our resource calculus allows us to simulate the beta-reduction of lambda-terms; the extensional nature of this expansion shows in the fact that we are also able to simulate eta-reduction. In a sense, extensional resource terms contain a language of finite approximants of Nakajima trees, much like ordinary resource terms can be seen as a richer version of finite Böhm trees. We show that the equivalence induced on lambda-terms by the normalization of extensional Taylor-expansion is nothing but H*, the greatest consistent sensible lambda-theory -- which is also the theory induced by Nakajima trees. This characterization provides a new, simple way to exhibit models of H*: it becomes sufficient to model the extensional resource calculus and its dynamics. The extensional resource calculus moreover allows us to recover, in an untyped setting, a connection between Taylor expansion and game semantics that was previously limited to the typed setting. Indeed, simply typed, eta-long, beta-normal resource terms are known to be in bijective correspondence with plays in the sense of Hyland-Ong game semantics, up to Melliès' homotopy equivalence. Extensional resource terms are the appropriate counterpart of eta-long resource terms in an untyped setting: we spell out the bijection between normal extensional resource terms and isomorphism classes of augmentations (a canonical presentation of plays up to homotopy) in the universal arena.

cs.LO↗

arXiv2026

Yeo's Theorem for Locally Colored Graphs: the Path to Sequentialization in Linear Logic

We revisit sequentialization proofs associated with the Danos-Regnier correctness criterion in the theory of proof nets of linear logic. Our approach relies on a generalization of Yeo's theorem for graphs, based on colorings of half-edges. This happens to be the appropriate level of abstraction to extract sequentiality information from a proof net without modifying its graph structure. We thus obtain different ways of recovering a sequent calculus derivation from a proof net inductively, by relying on a splitting vertex, which we can impose to be a par-vertex, or a terminal vertex, or a non-axiom vertex, etc., in a modular way. This approach applies in presence of the mix-rules as well as for proof nets of unit-free multiplicative-additive linear logic (through an appropriate further generalization of Yeo's theorem). The proof of our Yeo-style theorem relies on a key lemma that we call cusp minimization. Given a coloring of half-edges, a cusp in a path is a vertex whose adjacent half-edges in the path have the same color. And, given a cycle with at least one cusp and subject to suitable hypotheses, cusp minimization constructs a cycle with strictly less cusps. In the absence of cusp-free cycles, cusp minimization is then enough to ensure the existence of a splitting vertex, i.e. a vertex that is a cusp of any cycle it belongs to. Our theorem subsumes several graph-theoretical results, including some known to be equivalent to Yeo's theorem. The novelty is that they can be derived in a straightforward way, just by defining a dedicated coloring, again without any modification of the underlying graph structure (vertices and edges) -- similar results from the literature required more involved encodings.

cs.LO↗

arXiv2025

Strategies as Resource Terms, and their Categorical Semantics

As shown by Tsukada and Ong, simply-typed, normal and eta-long resource terms correspond to plays in Hyland-Ong games, quotiented by Melliès' homotopy equivalence. The original proof of this inspiring result is indirect, relying on the injectivity of the relational model w.r.t. both sides of the correspondence -- in particular, the dynamics of the resource calculus is taken into account only via the compatibility of the relational model with the composition of normal terms defined by normalization. In the present paper, we revisit and extend these results. Our first contribution is to restate the correspondence by considering causal structures we call augmentations, which are canonical representatives of Hyland-Ong plays up to homotopy. This allows us to give a direct and explicit account of the connection with normal resource terms. As a second contribution, we extend this account to the reduction of resource terms: building on a notion of strategies as weighted sums of augmentations, we provide a denotational model of the resource calculus, invariant under reduction. A key step -- and our third contribution -- is a categorical model we call a resource category, which is to the resource calculus what differential categories are to the differential lambda-calculus.

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↗

arXiv2023

The algebraic $λ$-calculus is a conservative extension of the ordinary $λ$-calculus

The algebraic $λ$-calculus is an extension of the ordinary $λ$-calculus with linear combinations of terms. We establish that two ordinary $λ$-terms are equivalent in the algebraic $λ$-calculus iff they are $β$-equal. Although this result was originally stated in the early 2000's (in the setting of Ehrhard and Regnier's differential $λ$-calculus), the previously proposed proofs were wrong: we explain why previous approaches failed and develop a new proof technique to establish conservativity.

cs.LO↗

arXiv2022

On the Taylor expansion of $λ$-terms and the groupoid structure of their rigid approximants

We show that the normal form of the Taylor expansion of a $λ$-term is isomorphic to its Böhm tree, improving Ehrhard and Regnier's original proof along three independent directions. First, we simplify the final step of the proof by following the left reduction strategy directly in the resource calculus, avoiding to introduce an abstract machine ad hoc. We also introduce a groupoid of permutations of copies of arguments in a rigid variant of the resource calculus, and relate the coefficients of Taylor expansion with this structure, while Ehrhard and Regnier worked with groups of permutations of occurrences of variables. Finally, we extend all the results to a nondeterministic setting: by contrast with previous attempts, we show that the uniformity property that was crucial in Ehrhard and Regnier's approach can be preserved in this setting.

cs.LO↗

arXiv2021

An application of parallel cut elimination in multiplicative linear logic to the Taylor expansion of proof nets

We examine some combinatorial properties of parallel cut elimination in multiplicative linear logic (MLL) proof nets. We show that, provided we impose a constraint on some paths, we can bound the size of all the nets satisfying this constraint and reducing to a fixed resultant net. This result gives a sufficient condition for an infinite weighted sum of nets to reduce into another sum of nets, while keeping coefficients finite. We moreover show that our constraints are stable under reduction. Our approach is motivated by the quantitative semantics of linear logic: many models have been proposed, whose structure reflect the Taylor expansion of multiplicative exponential linear logic (MELL) proof nets into infinite sums of differential nets. In order to simulate one cut elimination step in MELL, it is necessary to reduce an arbitrary number of cuts in the differential nets of its Taylor expansion. It turns out our results apply to differential nets, because their cut elimination is essentially multiplicative. We moreover show that the set of differential nets that occur in the Taylor expansion of an MELL net automatically satisfies our constraints. Interestingly, our nets are untyped: we only rely on the sequentiality of linear logic nets and the dynamics of cut elimination. The paths on which we impose bounds are the switching paths involved in the Danos--Regnier criterion for sequentiality. In order to accommodate multiplicative units and weakenings, our nets come equipped with jumps: each weakening node is connected to some other node. Our constraint can then be summed up as a bound on both the length of switching paths, and the number of weakenings that jump to a common node.

cs.LO↗