Jonas Frey, Basic relational objects and partial combinatory algebras
Schedule
- Feb. 16, 2012, 16:15 - 17:00
Abstract
Categorical logic attempts to understand realizability constructions by asso-
ciating fibred preorders (functors of type Setop → Preord, e.g. triposes or more
general hyperdoctrines) to them which abstract their essential features. These
fibred preorders can then be analyzed using various tools and constructions such
as categories of partial equivalence relations, assemblies and exact completions.
A special class of of fibred preorders is given by those which are represented
by ordinary preorders, i.e. are of the form Set(−, D) for a preorder D. The
2-category of representable fibred preorders (being equivalent to the 2-category
of preorders and monotone functions) and its relation to categorical logic via
presheaf and sheaf constructions is fairly well understood, but the 2-category of
general fibred preorders is more difficult to handle.
To overcome these difficulties, we introduce basic relational objects (BROs),
which are representations of fibred preorders that generalize (and in our opinion
simplify) Hofstra’s basic combinatory objects [1]. The 2-category BRO of BROs,
which is equivalent to a full sub-2-category of the 2-category of fibred posets, has
good closure properties – in particular it has an involution (−)op : BROco →
BRO corresponding to fibrewise (−)op on the level of fibred preorders, which
allows us to dualize Hofstra’s existential quantification monad D to obtain a
monad which classifies universal quantification. Moreover, BRO is sufficiently
large to contain all triposes.
We argue that BROs provide a good conceptual framework to understand
and relate the constructions of exact completion, assemblies and partial equiv-
alence relations, and to understand the relation to the (pre)sheaf theoretic con-
structions in the representable case.
Furthermore, the framework of basic relational objects permits to give an
extensional characterization of realizability over partial combinatory algebras.
References
[1] P.J.W. Hofstra. All realizability is relative. In Mathematical Proceedings of
the Cambridge Philosophical Society, volume 141, pages 239–264. Cambridge
Univ Press, 2006.
Attachments
Categorical logic attempts to understand realizability constructions by asso- ciating fibred preorders (functors of type Setop → Preord, e.g. triposes or more general hyperdoctrines) to them which abstract their essential features. These fibred preorders can then be analyzed using various tools and constructions such as categories of partial equivalence relations, assemblies and exact completions. A special class of of fibred preorders is given by those which are represented by ordinary preorders, i.e. are of the form Set(−, D) for a preorder D. The 2-category of representable fibred preorders (being equivalent to the 2-category of preorders and monotone functions) and its relation to categorical logic via presheaf and sheaf constructions is fairly well understood, but the 2-category of general fibred preorders is more difficult to handle. To overcome these difficulties, we introduce basic relational objects (BROs), which are representations of fibred preorders that generalize (and in our opinion simplify) Hofstra’s basic combinatory objects [1]. The 2-category BRO of BROs, which is equivalent to a full sub-2-category of the 2-category of fibred posets, has good closure properties – in particular it has an involution (−)op : BROco → BRO corresponding to fibrewise (−)op on the level of fibred preorders, which allows us to dualize Hofstra’s existential quantification monad D to obtain a monad which classifies universal quantification. Moreover, BRO is sufficiently large to contain all triposes. We argue that BROs provide a good conceptual framework to understand and relate the constructions of exact completion, assemblies and partial equiv- alence relations, and to understand the relation to the (pre)sheaf theoretic con- structions in the representable case. Furthermore, the framework of basic relational objects permits to give an extensional characterization of realizability over partial combinatory algebras.
References
[1] P.J.W. Hofstra. All realizability is relative. In Mathematical Proceedings of the Cambridge Philosophical Society, volume 141, pages 239–264. Cambridge Univ Press, 2006.