arXiv subjects

Aymeric Walch

Publications and source records attributed to Aymeric Walch.

5 recordsLinked to original sources

arXiv2026

Absolute convergence and Taylor expansion in web based models of Linear Logic

The differential $\lambda$-calculus studies how the quantitative aspects of programs correspond to differentiation and to Taylor expansion inside models of linear logic. Recent work has generalized the axioms of Taylor expansion so they apply to many models that only feature partial sums. However, that work does not cover the classic web based models of K{\"o}the spaces and finiteness spaces . First, we provide a generic construction of web based models with partial sums. It captures models, ranging from coherence spaces to probabilistic coherence spaces, finiteness spaces and K{\"o}the spaces. Second, we generalize the theory of Taylor expansion to models in which coefficients can be non-positive. We then use our generic web model construction to provide a unified proof that all the aforementioned web based models feature such Taylor expansion.

cs.LO↗

arXiv2025

Compositional Taylor expansion in cartesian differential categories

This paper provides a compositional approach to Taylor expansion, in the setting of cartesian differential categories. Taylor expansion is captured here by a functor that generalizes the tangent bundle functor to higher order derivatives. The fundamental properties of Taylor expansion then boils down to naturality equations that turns this functor into a monad. This monad provides a categorical approach to higher order dual numbers and the jet bundle construction used in automated differentiation.

cs.LO↗

arXiv2024

Internship report: Coherent differentiation in models of Linear Logic

Coherent differentiation was introduced by Ehrhard in order to generalize differential categories to a setting in which the sum is only partially defined, in order to account for the deterministic nature of most models of computation. This internship report proves that the deriving transformation of a differential category with a categorical product always induces a coherent differentiation. This ensures that coherent differentiation is indeed a generalization of differential categories.

cs.LO↗

arXiv2023

Coherent Taylor expansion as a bimonad

We extend the recently introduced setting of coherent differentiation for taking into account not only differentiation, but also Taylor expansion in categories which are not necessarily (left)additive. The main idea consists in extending summability into an infinitary functor which intuitively maps any object to the object of its countable summable families. This functor is endowed with a canonical structure of bimonad. In a linear logical categorical setting, Taylor expansion is then axiomatized as a distributive law between this summability functor and the resource comonad (aka.~exponential), allowing to extend the summability functor into a bimonad on the Kleisli category of the resource comonad: this extended functor computes the Taylor expansion of the (nonlinear) morphisms of the Kleisli category. We also show how this categorical axiomatizations of Taylor expansion can be generalized to arbitrary cartesian categories, leading to a general theory of Taylor expansion formally similar to that of differential cartesian categories, although it does not require the underlying cartesian category to be left additive.We provide several examples of concrete categories which arise in denotational semantics and feature such analytic structures.

cs.LO↗

arXiv2023

Cartesian Coherent Differential Categories

We extend to general Cartesian categories the idea of Coherent Differentiation recently introduced by Ehrhard in the setting of categorical models of Linear Logic. The first ingredient is a summability structure which induces a partial left-additive structure on the category. Additional functoriality and naturality assumptions on this summability structure implement a differential calculus which can also be presented in a formalism close to Blute, Cockett and Seely's Cartesian differential categories. We show that a simple term language equipped with a natural notion of differentiation can easily be interpreted in such a category.

cs.LO↗