arxiv: 2604.26829 · v1 · submitted 2026-04-29 · 💻 cs.LO

Recognition: unknown

Full Definability in a Profunctorial Model

Takeshi Tsukada , Kazuyuki Asada , Kengo Hirata

Authors on Pith no claims yet

Pith reviewed 2026-05-07 11:09 UTC · model grok-4.3

classification 💻 cs.LO

keywords full definabilityprofunctorsmultiplicative linear logicproof-netsMIXstabilityrelational modelgroupoids

0 comments

The pith

All logical families of stable and total profunctors are definable by proof-nets of multiplicative linear logic with MIX.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows that a profunctor model on groupoids, a proof-relevant strengthening of the relational model, captures every semantic element that meets the stability, totality and logical-family conditions as the denotation of an actual proof-net. Full definability follows from a direct extension of the relational-model argument once stability is imposed. A reader would care because this means the model contains no extraneous elements that lack a syntactic counterpart, so semantic reasoning stays faithful to the syntax of the logic.

Core claim

The central discovery is that stability, together with totality and the logical-family condition, supplies a complete characterisation: every such profunctor is the denotation of some proof-net in multiplicative linear logic with the MIX rule. The same stability condition also functions as a correctness criterion that decides whether a given profunctor arises from a proof.

What carries the argument

Stability for profunctors, which, combined with totality and the logical-family restriction, plays the role of the definability filter and simultaneously serves as a proof-net correctness criterion.

If this is right

The profunctor model becomes a fully faithful semantic setting for MLL with MIX.
Stability alone decides whether a given profunctor is the interpretation of a proof.
Any property proved in the model for stable total logical profunctors transfers directly to the syntax.
The same technique may be reused for other proof-relevant relational-style models.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

Stability may serve as a general filter for definability in other categories that enrich the relational model.
The result supplies a concrete bridge between proof-net syntax and a higher-dimensional relational semantics.
If similar stability notions can be found for other fragments, full definability could extend beyond multiplicative linear logic.

Load-bearing premise

The stability condition for profunctors, together with totality and the logical-family property, extends the relational-model definability techniques without creating new gaps that the added structure of profunctors would introduce.

What would settle it

Exhibit a stable, total, logical profunctor on groupoids that is not the denotation of any MLL+MIX proof-net, or show that stability fails to exclude at least one non-definable profunctor.

Figures

Figures reproduced from arXiv: 2604.26829 by Kazuyuki Asada, Kengo Hirata, Takeshi Tsukada.

**Figure 1.** Figure 1: The proof rules of the sequent calculus MLL + Mix. ` ⊗ ` 𝑋1 𝑋2 𝑋 ⊥ 2 ` ` 𝑋2 𝑋 ⊥ 2 𝑋 ⊥ 1 view at source ↗

**Figure 2.** Figure 2: A proof structure of ( (𝑋1 `𝑋2) ⊗𝑋 ⊥ 2 ) ` ( (𝑋2 `𝑋 ⊥ 2 ) ` 𝑋 ⊥ 1 ). ` ⊗ ` 𝑋1 𝑋2 𝑋 ⊥ 2 ` ` 𝑋2 𝑋 ⊥ 2 𝑋 ⊥ 1 view at source ↗

**Figure 3.** Figure 3: An incorrect proof structure of ( (𝑋1 ` 𝑋2) ⊗ 𝑋 ⊥ 2 ) ` ( (𝑋2 ` 𝑋 ⊥ 2 ) ` 𝑋 ⊥ 1 ). For a Danos-Regnier switching choosing the right branch for the left-most `, there is a cycle `–𝑋2– 𝑋 ⊥ 2 –⊗–` on the left. A sequent Γ is a finite sequence of formulas. The concatenation of sequents Γ and Δ is written as Γ, Δ. The (one-sided) sequent calculus MLL + Mix is defined by the rules in view at source ↗

**Figure 4.** Figure 4: An element experiment. Here 𝛼 : 𝑎1 → 𝑎2 is in A1, and 𝛽 : 𝑏1 → 𝑏2 and 𝛾 : 𝑐1 → 𝑐2 are morphisms in A2. This describes an element in Exp(𝜋) ( ( (𝑎2, 𝑏2), 𝑏1), ( (𝑐2, 𝑐1), 𝑎1)). ` ⊗ ` 𝑋1 𝑋2 𝑋 ⊥ 2 ` ` 𝑋2 𝑋 ⊥ 2 𝑋 ⊥ 1 𝑓1𝛼 𝑓2 𝑔1𝛽𝑔2 ℎ1𝛾ℎ2 view at source ↗

**Figure 5.** Figure 5: The result of the action of ( ( (𝑓2, 𝑔2), 𝑔1), ( (ℎ2, ℎ1), 𝑓1)) on the element experiment in view at source ↗

**Figure 6.** Figure 6: The result of the orientation. For readability, unori view at source ↗

read the original abstract

A semantic model enjoys full definability if every semantic element in the model is a denotation of some proof or program. Full definability indicates that the model captures programs and proofs in a highly detailed manner. This paper studies full definability in a model based on the (bi)category of profunctors on groupoids, which is a proof-relevant variant of the relational model. Despite the fact that a profunctor is far more complicated than a relation, we show that a rather straightforward application of the ideas for the relational model, together with the notion of stability in profunctors, provides a complete characterisation of definable profunctors. More precisely, all logical families of stable and total profunctors are definable by proof-nets of multiplicative linear logic with MIX. As a part of the full definability proof, we show that the stability serves as a correctness criterion, which we think is of independent interest.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

They characterize the definable profunctors using stability in a way that extends the relational model cleanly.

read the letter

Hey, the main result is that full definability holds in the profunctorial model: every logical family of stable and total profunctors is the denotation of some MLL with MIX proof-net. They achieve this by adapting the relational model approach and introducing stability to handle the extra information in profunctors. What stands out is the explicit construction and the proof that stability serves as a correctness criterion. This seems to go through without issues, as per the assessment that there are no visible gaps or new obstructions from the profunctor structure. It's good that they don't overstate the novelty; it's a straightforward lift with the stability notion added in. The potential weak point is the reliance on the specific definitions of logical families and totality in this setting. If those are standard, then it's fine, but it might require some work to verify the extension doesn't introduce hidden problems. Overall, the central argument appears to hold up. This kind of paper is useful for people studying semantics of linear logic and proof theory. A reader focused on full definability or profunctor models would get concrete value from the characterization. I'd say send it to peer review. It's a precise result in a niche but established area, and the method is reproducible from the relational case.

Referee Report

0 major / 1 minor

Summary. The paper claims that the bicategory of profunctors on groupoids provides a proof-relevant model of multiplicative linear logic with MIX in which full definability holds: every logical family of stable and total profunctors is the denotation of some MLL+MIX proof-net. The argument lifts the relational-model construction by adding a stability predicate on profunctors; stability is shown both to characterise the definable elements and to function as a correctness criterion for the semantics.

Significance. If the result holds, it supplies a concrete full-definability theorem in a strictly richer, proof-relevant setting than the relational model while preserving the same definable fragment. The dual use of stability—as both a filter for definability and an independent correctness criterion—is of independent interest and may transfer to other enriched or higher-dimensional models of linear logic. The explicit construction via relational techniques gives a direct, checkable bridge between syntax and this semantic framework.

minor comments (1)

The abstract states that stability 'serves as a correctness criterion' but does not indicate in which section the proof appears; a forward reference would help readers locate the argument quickly.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment of the manuscript and the recommendation to accept. The provided summary accurately captures our main result: that the bicategory of profunctors on groupoids yields a proof-relevant model of MLL+MIX with full definability for logical families of stable and total profunctors, lifting the relational model via the stability predicate, which also serves as a correctness criterion.

Circularity Check

0 steps flagged

Minor self-citation present but central claim remains independent

full rationale

The paper lifts relational-model definability techniques to profunctors by introducing the stability predicate, then proves that logical families of stable total profunctors are exactly the denotations of MLL+MIX proof-nets. This supplies an explicit construction together with a correctness-criterion argument for stability. While prior relational results are necessarily cited, the added profunctor structure and stability condition are handled directly inside the manuscript without reducing the main theorem to a self-citation chain or to a definitional equivalence. The derivation therefore contains independent content and receives only the minimal score for routine self-citation.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Without the full manuscript, specific free parameters, axioms, or invented entities cannot be audited; the work appears to rest on standard properties of profunctors, groupoids, and linear logic.

pith-pipeline@v0.9.0 · 5460 in / 1030 out tokens · 82776 ms · 2026-05-07T11:09:12.427139+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

36 extracted references · 32 canonical work pages

[1]

Samson Abramsky and Radha Jagadeesan. 1994. Games and full completeness for multiplicative linear logic.Journal of Symbolic Logic59, 2 (June 1994), 543–574. doi:10.2307/2275407

work page doi:10.2307/2275407 1994
[2]

Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. 2000. Full Ab- straction for PCF.Information and Computation163, 2 (dec 2000), 409–470. doi:10.1006/inco.2000.2930

work page doi:10.1006/inco.2000.2930 2000
[3]

1978.Stable models of typed 𝜆-calculi

Gérard Berry. 1978.Stable models of typed 𝜆-calculi. Springer Berlin Heidelberg, 72–89. doi:10.1007/3-540-08860-1_7

work page doi:10.1007/3-540-08860-1_7 1978
[4]

Pierre Clairambault and Simon Forest. 2023. The Cartesian Closed Bicategory of Thin Spans of Groupoids. In2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). IEEE, 1–13. doi:10.1109/lics56636.2023.10175754

work page doi:10.1109/lics56636.2023.10175754 2023
[5]

Pierre Clairambault and Simon Forest. 2024. An Analysis of Symmetry in Quan- titative Semantics. InProceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS ’24). ACM, 1–13. doi:10.1145/3661814.3662092

work page doi:10.1145/3661814.3662092 2024
[6]

Vincent Danos and Thomas Ehrhard. 2011. Probabilistic coherence spaces as a model of higher-order probabilistic computation.Information and Computation 209, 6 (jun 2011), 966–991. doi:10.1016/j.ic.2011.02.001

work page doi:10.1016/j.ic.2011.02.001 2011
[7]

Vincent Danos and Laurent Regnier. 1989. The structure of multiplicatives. Archive for Mathematical Logic28, 3 (Oct. 1989), 181–203. doi:10.1007/bf01622878 Full Definability in a Profunctorial Model

work page doi:10.1007/bf01622878 1989
[8]

Daniel de Carvalho. 2017. Execution time of 𝜆-terms via denotational semantics and intersection types.Mathematical Structures in Computer Science28, 7 (Jan. 2017), 1169–1203. doi:10.1017/s0960129516000396

work page doi:10.1017/s0960129516000396 2017
[9]

Devarajan, D

H. Devarajan, D. Hughes, G. Plotkin, and V. Pratt. 1999. Full completeness of the multiplicative linear logic of Chu spaces. InProceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158) (LICS-99). IEEE Comput. Soc, 234–243. doi:10.1109/lics.1999.782619

work page doi:10.1109/lics.1999.782619 1999
[10]

Clovis Eberhart and Tom Hirschowitz. 2018. What’s in a game?: A theory of game models. InProceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS ’18). ACM, 374–383. doi:10.1145/3209108.3209114

work page doi:10.1145/3209108.3209114 2018
[11]

Clovis Eberhart, Tom Hirschowitz, and Thomas Seiller. 2017. An intensionally fully-abstract sheaf model for𝜋 (expanded version).Logical Methods in Computer ScienceVolume 13, Issue 4 (Nov. 2017). doi:10.23638/lmcs-13(4:9)2017

work page doi:10.23638/lmcs-13(4:9)2017 2017
[12]

Thomas Ehrhard. 1993. Hypercoherences: a strongly stable model of linear logic.Mathematical Structures in Computer Science3, 4 (Dec. 1993), 365–385. doi:10.1017/s0960129500000281

work page doi:10.1017/s0960129500000281 1993
[13]

Thomas Ehrhard and Laurent Regnier. 2008. Uniformity and the Taylor expansion of ordinary lambda-terms.Theoretical Computer Science403, 2-3 (aug 2008), 347–

2008
[14]

doi:10.1016/j.tcs.2008.06.001

work page doi:10.1016/j.tcs.2008.06.001 2008
[15]

Marcelo Fiore, Zeinab Galal, and Hugo Paquet. 2022. A Combinatorial Approach to Higher-Order Structure for Polynomial Functors. InFSCD. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. doi:10.4230/LIPICS.FSCD.2022.31

work page doi:10.4230/lipics.fscd.2022.31 2022
[16]

Marcelo Fiore, Zeinab Galal, and Hugo Paquet. 2024. Stabilized profunctors and stable species of structures.Logical Methods in Computer ScienceVolume 20, Issue 1 (Feb. 2024). doi:10.46298/lmcs-20(1:17)2024

work page doi:10.46298/lmcs-20(1:17)2024 2024
[17]

Fiore, N

M. Fiore, N. Gambino, and M. Hyland. 2024. Monoidal bicategories, differential linear logic, and analytic functors. doi:10.48550/ARXIV.2405.05774

work page doi:10.48550/arxiv.2405.05774 2024
[18]

Fiore, N

M. Fiore, N. Gambino, M. Hyland, and G. Winskel. 2007. The cartesian closed bi- category of generalised species of structures.Journal of the London Mathematical Society77, 1 (Oct. 2007), 203–220. doi:10.1112/jlms/jdm096

work page doi:10.1112/jlms/jdm096 2007
[19]

Arnaud Fleury and Christian Retoré. 1994. The mix rule.Mathematical Structures in Computer Science4, 2 (June 1994), 273–285. doi:10.1017/s0960129500000451

work page doi:10.1017/s0960129500000451 1994
[20]

Jean-Yves Girard. 1987. Linear logic.Theoretical Computer Science50, 1 (1987), 1–101. doi:10.1016/0304-3975(87)90045-4

work page doi:10.1016/0304-3975(87)90045-4 1987
[21]

Jean-Yves Girard. 1988. Normal functors, power series and 𝜆-calculus.Annals of Pure and Applied Logic37, 2 (Feb. 1988), 129–177. doi:10.1016/0168-0072(88)90025- 5

work page doi:10.1016/0168-0072(88)90025- 1988
[22]

Hyland and C.-H.L

J.M.E. Hyland and C.-H.L. Ong. 2000. On Full Abstraction for PCF: I, II, and III. Information and Computation163, 2 (dec 2000), 285–408. doi:10.1006/inco.2000. 2917

work page doi:10.1006/inco.2000 2000
[23]

Martin Hyland and Andrea Schalk. 1999. Abstract Games for Linear Logic Extended Abstract.Electronic Notes in Theoretical Computer Science29 (1999), 127–150. doi:10.1016/s1571-0661(05)80312-3

work page doi:10.1016/s1571-0661(05)80312-3 1999
[24]

Martin Hyland and Andrea Schalk. 2003. Glueing and orthogonality for models of linear logic.Theoretical Computer Science294, 1-2 (feb 2003), 183–231. doi:10. 1016/s0304-3975(01)00241-9

2003
[25]

2018.Categorical Combinatorics for Non Deterministic Strategies on Simple Games

Clément Jacq and Paul-André Melliès. 2018.Categorical Combinatorics for Non Deterministic Strategies on Simple Games. Springer International Publishing, 39–70. doi:10.1007/978-3-319-89366-2_3

work page doi:10.1007/978-3-319-89366-2_3 2018
[26]

R. Loader. 1994. Linear logic, totality and full completeness. InProceedings Ninth Annual IEEE Symposium on Logic in Computer Science (LICS-94). IEEE Comput. Soc. Press, 292–298. doi:10.1109/lics.1994.316060

work page doi:10.1109/lics.1994.316060 1994
[27]

P.-A. Melliès. 2005. Asynchronous Games 4: A Fully Complete Model of Proposi- tional Linear Logic. In20th Annual IEEE Symposium on Logic in Computer Science (LICS’ 05). IEEE, 386–395. doi:10.1109/lics.2005.6

work page doi:10.1109/lics.2005.6 2005
[28]

Federico Olimpieri. 2021. Intersection Type Distributors. In2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). IEEE, 1–15. doi:10. 1109/lics52264.2021.9470617

work page arXiv 2021
[29]

Luke Ong

C.-H. Luke Ong. 2017. Quantitative semantics of the lambda calculus: Some gen- eralisations of the relational model. In2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). IEEE, 1–12. doi:10.1109/lics.2017.8005064

work page doi:10.1109/lics.2017.8005064 2017
[30]

Christian Retoré. 1997. A semantic characterisation of the correctness of a proof net.Mathematical Structures in Computer Science7, 5 (Oct. 1997), 445–452. doi:10.1017/s096012959700234x

work page doi:10.1017/s096012959700234x 1997
[31]

Paul E. Schupp. 1987. A characterization of inner automorphisms.Proc. Amer. Math. Soc.101, 2 (1987), 226–228. doi:10.1090/s0002-9939-1987-0902532-x

work page doi:10.1090/s0002-9939-1987-0902532-x 1987
[32]

Paul Taylor. 1989. Quantitative domains, groupoids and linear logic. InCategory Theory and Computer Science, David H. Pitt, David E. Rydeheard, Peter Dybjer, Andrew M. Pitts, and Axel Poigné (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 155–181

1989
[33]

Luke Ong

Takeshi Tsukada, Kazuyuki Asada, and C.-H. Luke Ong. 2017. Generalised species of rigid resource terms. In2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). IEEE. doi:10.1109/lics.2017.8005093

work page doi:10.1109/lics.2017.8005093 2017
[34]

Luke Ong

Takeshi Tsukada, Kazuyuki Asada, and C.-H. Luke Ong. 2018. Species, Profunc- tors and Taylor Expansion Weighted by SMCC. InProceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science. ACM. doi:10.1145/3209108. 3209157

work page doi:10.1145/3209108 2018
[35]

Luke Ong

Takeshi Tsukada and C.-H. Luke Ong. 2015. Nondeterminism in Game Semantics via Sheaves. In2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science. IEEE. doi:10.1109/lics.2015.30

work page doi:10.1109/lics.2015.30 2015
[36]

Glynn Winskel. 2013. Strategies as Profunctors. InFoundations of Software Science and Computation Structures. Springer Berlin Heidelberg, 418–433. doi:10.1007/ 978-3-642-37075-5_27 Takeshi Tsukada, Kazuyuki Asada, and Kengo Hirata A Proof of Proposition 8 We first recall the claim. Claim.LetAbe a groupoid. (1)A family𝐶=(𝐶 𝑎 ⊆A(𝑎, 𝑎)) 𝑎 is a creed if and o...

2013