The Coq mailing list

[Christopher Mary <admin AT AnthropLOGIC.onmicrosoft.com>]

Capo,

https://hal.science/hal-04292862

instead of a one-liner reject « not sufficiently clear » as you did to my 
HOTT-2023 paper, here is my thorough review of Marie Kerjean's “Functorial 
Models of Differential Linear Logic” at TLLA 2024, although their Proposition 
3 (functorial differentiation is a left-adjoint in a chirality) is still "not 
sufficiently clear" and probably false, lol

The logic of polynomials (a.k.a. differential linear logic) is often 
expressed via an algebraic "deriving" transformation d: k[V] → k[V] ⊗ V 
(meaning approximately d: f(x) ↦ f'(x) ⊗ dx) with the usual rules (formulated 
in the notations for a monad k[-] which is also a ⊗-monoid) when applied to 
constant (scalar in k) polynomials, identity (linear) polynomials, product 
(multiplication) of polynomials, or substitution of polynomials (chain rule).‎

Its more logical dual operation  d: !V ⊗ V → !V instead pre-compose any f: !V 
→ W, understood as the underlying relation/profunctor of a polynomial which 
stores the coefficients at each of the "monomials" (xy, xx, y, xyz, ...) in 
!V, such to produce, at any (outer/extensional) parameter point a: 1 → !V, 
another derived relation  D_a f ≔ f∘(a⊗d): V → W which now only uses linear 
monomials (x, y, z, ...) in V. 

Essentially, Kerjean's "Functorial Models of Differential Linear Logic" 
exploits an overlooked choice in this formulation: should the deriving 
transformation be formulated as d: V → !V (derivation at 0, intentionally 
together with other translation/codiagonal operations), or as d: !V ⊗ V → !V 
(derivation anywhere at any intentional variable), or operationally 
extensionally as a functor D(a: I → V |f: !V → W): V → W, defined on the 
co-slice (pointed objects) of the co-Kleisli category of the comonad !, where 
its functoriality becomes the "chain rule" of differentiation?

Clearly, tautologically, the intentional and extensional formulations should 
be equivalent when everything is "well-pointed", and this is the content of 
Kerjean paper until page 15 where they improvise an attempt to relate this 
functorial differentiation D to the notion of chirality (*-autonomy) for 
linear-non-linear adjunctions: they claim in Proposition 3 that the 
differentiation functor D becomes some left-adjoint in a new framework of a 
generalized chirality produced by any *-autonomous differential category... 
But their Proposition 3, which is essential to justify this improvised forced 
relevance of "chirality" for this paper, is far from "clearly demonstrated" 
and is most possibly incorrect.‎

Nevertheless, this operational extensional formulation of differentiation, 
reminds of Kosta Dosen's cut-elimination-in-categories techniques, and could 
be a good candidate for the computer implementation of the (substructural) 
logic of differentiation (which is not available via the alternative of 
cartesian closed differential categories) of analytic functors (or "stable" 
or "flat" functor). But there is a difference between a polynomial formulated 
above as an analytic functor and a polynomial formulated as a polynomial 
functor (B ∈ Set, E: B → Set) here:
‎
https://github.com/1337777/cartier/blob/master/cartierSolution15.lp ‎

This is a draft implementation of polynomial functors as bicomodules in a 
double category of categories, functors, cofunctors and profunctors. Here the 
underlying profunctors store the exponents X^(E[b]) of each summand/position 
b of the polynomial, instead of storing the aggregated coefficients C[e]⋅X^e 
at each exponent e of the polynomial as is the situation above for analytic 
functors.‎ ‎ (This file also contains a draft implementation of 
inductively-constructed topological covering sieves as profunctors dependent 
over the hom-profunctors, solving Olivia Caramello's question.)

Differentiation of polynomial functors has been studied (for example 
(∂List)(X) ≔ Σ(n:N)(h:[n]), [n]\{h} → X = (List(X))^2) in the framework of 
cartesian differential categories. Differentiation of analytic (or "flat") 
functors has been studied (for example dF(-, YZ) ≔ F(-, XYZ) for the 
coefficient at the monomial YZ when derived along X) in the substructural 
logic of differential categories with exponential comonad !, the free 
(symmetric) monoidal category monad/comonad in the bicategory of profunctors. 
None of these earlier studies would qualify as a solution in this sense:‎

Could there exists a hybrid implementation setup with the categorial algebra 
of polynomial functors and the differential linear logic of analytic 
functors? In simple words: grouping summands 1 + X + X ≃ 1 + 2⋅X in a 
polynomial is highly questionable...‎

Here is a copy of this review on re365.net < https://dailyReviews.link > the 
free open source Microsoft 365 app, developed by a community < 
https://meetup.com/dubai-ai > of 2,000+ contributors, to Schedule reviews 
with authors and businesses, with the end-goal to co-author or by-product an 
AI interface for their papers and apps API; it is some kind of tiktok-style 
calendar overlay of arxiv, producthunt, researchseminars (and soon 
semanticscholar) for users (and editors/marketers) to schedule reviews with 
VIP authors/developers:

https://re365.net/doi/?q=63D9544F-3905-425B-80F2-EA116A6CDC08
https://re365.net/doi/?q=Kerjean+Functorial+Models+of+Differential+Linear+Logic
  or non-permanent < 
https://anthroplogic.sharepoint.com/:w:/s/cycle1/EU9U2WMFOVtCgPLqEWps3AgB6qbLLUoVUJVB2YfA1aB2-A
 >