Coherent Taylor expansion as a bimonad in models of LL
Date(s) : 08/02/2024 iCal
11h00 - 12h30
The differential lambda calculus was introduced by Ehrhard and Regnier. This
calculus features an operation of differentiation that extracts the best linear
interpretation of a program. Linearity should be understood as the linearity of
Linear Logic: a linear program is a program that uses its input exactly once
during computation. This led to the discovery of an analogue of Taylor
expansion in the lambda calculus: a program can be compiled into an infinite
sum of approximants called resource terms, in which the application is always
linear.
Because of the Leibniz rule of the differential calculus, differentiation is
always defined in settings with an unrestricted sum, both in syntax and
semantics. The issue is that such a sum can only be interpreted as non
determinism. This leaves behind many interesting models of linear logic, such
as coherent spaces and probabilistic coherent spaces. Recently, Ehrhard
introduced coherent differentiation, an axiomatization of differentiation in
models of linear logic in which sums are only partial. This notion of
differentiation generalizes the existing one and includes the aforementioned
models.
We show that the formalism of coherent differentiation can be adapted in a
surprisingly straightforward way to handle not only differentiation, but the
whole Taylor expansion. This leads to an axiomatization of Taylor expansion that
covers a wide spectrum of models of Linear Logic. We show that in many
situations, Taylor expansion amounts to a simple coalgebra on the exponential
modality. In particular, models with a Lafont exponential are very prone to
feature Taylor expansion.
Emplacement
I2M Luminy - TPR2, Amphithéâtre Herbrand 130-134 (1er étage)
Catégories
