Full Definability in a Profunctorial Model

TL;DR

This paper demonstrates that a profunctorial model based on groupoids achieves full definability, meaning every semantic element corresponds to some proof or program, using stability as a correctness criterion.

Contribution

It provides a complete characterization of definable profunctors in a proof-relevant relational model using stability and totality, extending ideas from the relational model.

Findings

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

Stability serves as an effective correctness criterion in the model.

The model captures programs and proofs in a highly detailed manner.

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.