Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2604.26829 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866917447599128576 |
|---|---|
| author | Tsukada, Takeshi Asada, Kazuyuki Hirata, Kengo |
| author_facet | Tsukada, Takeshi Asada, Kazuyuki Hirata, Kengo |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_26829 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Full Definability in a Profunctorial Model Tsukada, Takeshi Asada, Kazuyuki Hirata, Kengo Logic in Computer Science 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. |
| title | Full Definability in a Profunctorial Model |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2604.26829 |