The Coq mailing list

[nicolas tabareau <nicolas.tabareau AT inria.fr>]

Dear Christopher,

The Coq-club mailing list, like all communication within the Coq ecosystem, is governed by a code of conduct [1].

Your recent message does not adhere to this code and should not have been sent.

Please note that the Coq-club mailing list is not moderated for subscribed users, as we trust community members to self-regulate and follow the code of conduct.

We hope to maintain this level of trust moving forward.

Best regards,

The Coq Code of Conduct Team

[1] https://github.com/coq/coq/blob/master/CODE_OF_CONDUCT.md

On 9 Jul 2024, at 06:37, Christopher Mary <admin AT AnthropLOGIC.onmicrosoft.com> wrote:

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 >