Technical reports

The Dialectica categories

Valeria Correa Vaz de Paiva

January 1991, 82 pages

This technical report is based on a dissertation submitted November 1988 by the author for the degree of Doctor of Philosophy to the University of Cambridge, Lucy Cavendish College.

DOI: 10.48456/tr-213

Abstract

This work consists of two main parts. The first one, which gives it its name, presents an internal categorical version of Gödel’s “Dialectica interpretation” of higher-order arithmetic. The idea is to analyse the Dialectica interpretation using a cetegory DC where objects are relations on objects of a basic category C and maps are pairs of maps of C satisfying a pullback condition. If C is finitely complete, DC exists and has a very natural symmetric monoidal structure. If C is locally cartesian closed then DC is symmetric monoidal closed. If we assume C with stable and disjoint coproducts, DC has cartesian products and weak-coproducts and satisfies a weak form of distributivity. Using the structure above, DC is a categorical model for intuitionistic linear logic.

Moreover if C has free monoids then DC has cofree comonoids and the corresponding comonad “!” on DC, which has some special properties, can be used to model the exponential “of course!” in Intuitionistic Linear Logic. The category of “!”-coalgebras is isomorphic to the category of comonoids in DC and, if we assume commutative monoids in C, the “!”-Kleisli category, which is cartesian closed, corresponds to the Diller-Nahm variant of the Dialectica interpretation.

The second part introduces the categories GC. The objects of GC are the same objects of DC, but morphisms are easier to handle, since they are maps in C in opposite directions. If C is finitely complete, the category GC exists. If C is cartesian closed, we can define a symmetric monoidal structure and if C is locally cartesian closed as well, we can define inernal homs in GC that make it a symmetric monoidal closed category. Supposing C with stable and disjoint coproducts, we can define cartesian products and coproducts in GC and, more interesting, we can define a dual operation to the tensor product bifunctor, called “par”. The operation “par” is a bifunctor and has a unit “⊥”, which is a dualising object. Using the internal hom and ⊥ we define a contravariant functor “(−)⊥” which behaves like negation and thus it is used to model linear negation. We show that the category GC, with all the structure above, is a categorical model for Linear Logic, but not exactly the classical one.

In the last chapter a comonad and a monad are defined to model the exponentials “!” and “?”. To define these endofunctors, we use Beck’s distributive laws in an interesting way. Finally, we show that the Kleisli category GC! is cartesian closed and that the categories DC and GC are related by a Kleisli construction.

Full text

PDF (3.5 MB)

BibTeX record

@TechReport{UCAM-CL-TR-213,
  author =	 {de Paiva, Valeria Correa Vaz},
  title = 	 {{The Dialectica categories}},
  year = 	 1991,
  month = 	 jan,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-213.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-213},
  number = 	 {UCAM-CL-TR-213}
}