Math and Logic
2008
A new description of orthogonal bases
— with Bob Coecke and Jamie Vicary
Abstract
We show that an orthogonal basis for a finite-dimensional Hilbert space can be equivalently characterised as a commutative dagger-Frobenius monoid in the category FHilb, which has finite-dimensional Hilbert spaces as objects and continuous linear maps as morphisms, and tensor product for the monoidal structure. The basis is normalised exactly when the corresponding commutative dagger-Frobenius monoid is special. Hence orthogonal and orthonormal bases can be axiomatised in terms of composition of operations and tensor product only, without any explicit reference to the underlying vector spaces. This axiomatisation moreover admits an operational interpretation, as the comultiplication copies the basis vectors and the counit uniformly deletes them. That is, we rely on the distinct ability to clone and delete classical data as compared to quantum data to capture basis vectors. For this reason our result has important implications for categorical quantum mechanics.
1997
*Chu I: cofree equivalences, dualities and -autonomous categories
Abstract
We study three comonads derived from the comma construction. The induced coalgebras correspond to the three concepts displayed in the title of the paper. The comonad that yields the cofree *-autonomous categories is, in essence, the Chu construction, which has recently awaken much interest in computer science. We describe its couniversal property. It is right adjoint to the inclusion of *-autonomous categories among autonomous categories, with lax structure-preserving morphisms. Moreover, this inclusion turns out to be comonadic: *-autonomous categories are exactly the Chu-coalgebras.
1996
Maps II: chasing diagrams in categorical proof theory
Abstract
In categorical proof theory, propositions and proofs are presented as objects and arrows in a category. It thus embodies the strong constructivist paradigms of propositions-as-types and proofs-as-constructions, which lie in the foundation of computational logic. Moreover, in the categorical setting, a third paradigm arises, not available elsewhere: logical-operations-as-adjunctions. It offers an answer to the notorious question of the equality of proofs. Diagram chasing comes about in algebra of proofs.
On the basis of these ideas, the present paper investigates proof theory of regular logic: the {\and,\exists}-fragment of the first order logic with equality. The corresponding categorical structure is regular fibration. The examples include stable factorisations, sites, triposes. Regular logic is exactly what is needed to talk about maps, as total and single-valued relations. However, when enriched with proofs-as-arrows, this familiar concept must be supplied with an additional conversion rule, connecting the proof of the totality with the proof of the single-valuedness. We explain the logical meaning of this rule, and then determine precise conditions under which a regular fibration supports the principle of function comprehension (that each map corresponds to a unique function viz arrow in the base), thus lifting a basic theorem from regular categories (that Map(Rel(C) = C), which was recently relativized to factorisation systems. The obtained results open an interesting possibility of extending the P-set construction from triposes to non-posetal fibrations.
1995
A categorical setting for the 4-Colour Theorem
Abstract
The 4-Colour Theorem has been proved in the late seventies , after more than a century of fruitless efforts. But the proof has provided very little new information about the map colouring itself. While trying to understand this phenomenon, we analyze colouring in terms of universal properties and adjoint functors.
It is well known that the 4-colouring of maps is equivalent to the 3-colouring of the edges of some graphs. We show that every slice of the category of 3-coloured graphs is a topos. The forgetful functor to the category of graphs is cotripleable; every loop-free graph is covered by a 3-coloured one in a universal way. In this context, the 4-Color Theorem becomes a statement about the existence of coalgebra structure on graphs.
In a sense, this approach seems complementary to the known combinatorial colouring procedures.
On completeness and cocompleteness in and around small categories
Abstract
The simple connection of completeness and cocompleteness of lattices grows in categories into the Adjoint Functor Theorem. The connection of completeness and cocompleteness of Boolean algebras - even simpler
- is similarly related to Pare’s Theorem for toposes. We explain these relations and then study the fibrational versionso of both theorems, for small complete categories. They can be interpreted as definability results in logic with proofs-as-constructions, and transferred into type theory.
Maps I: relative to a factorisation system
Abstract
Originally, categorical calculus of relations was developed using the canonical factorisations in regular categories. More recently, relations restricted to a proper factorisation systems have been studied by several authors. In the present paper, we consider the general situation, where relations are induced by an arbitrary stable factorisation. This extension of the calculus of relations is necessary for categorical development of strongly constructivist logic, and of semantics of computation, where non-monic relations come about naturally.
In this setting we analyze the correspondence of * maps*, i.e. the total, single-valued relations, and functions, as given by the arrows of the underlying category.
1992
On the structure of paradoxes
Abstract
Paradox is a logical phenomenon. Usually, it is produced in type theory, over a type of “truth values”. A formula p, as a term p:Prop is constructed, such that p is equivalent to its negation - whereupon everything can be proved. We describe a general pattern which many constructions of the formula follow: for example, the well known arguments of Cantor, Russell, and Goedel. We generalize their common underlying structure, and prove that Reynolds’ construction of the type isomorphic to its second power type, contrary to his conjecture, cannot be extended to give a fixed point of every variable type derived from exponentiation. In particular, for contravariant types, such a fixed point would lead to a paradox.
1991
[*Categorical Interpolation: Descent and the Beck-Chevalley
Condition without Direct Images*](../papers/BCDE-Como90.pdf)
Abstract
Fibred categories have been introduced by Grothendieck (1959, 1970) as the setting for his theory of descent. The present paper contains (in section 4) a characterisation of the effective descent morphisms under an arbitrary fibred category. This essentially geometric result complements a logical analysis of the Beck-Chevalley property (presented in section 1). This property was crucial in the well-known theorem on sufficient conditions for the descent under bifibrations, due to Benabou and Roubaud (1970) and Beck (unpublished). We describe the notion of interpolant as the common denominator of the concepts of descent and the Beck-Chevalley property.
Constructions and Predicates
Abstract
In this paper, Coquand and Huet’s Theory of Constructions is reinterpreted as a type theory of “sets” and “predicates”. Following some set-theoretical intuitions, this popular type system is modified at two points: (1) a simple new operation is added - to represent a constructive version of the comprehension principle; (2) a restriction on contexts is imposed - “sets” must not depend on “proofs” of “predicates”. The resulting theory is called Theory of Predicates. Sufficiently constructive arguments from naive set theory can be directly written down in it. On the other hand, modification (2) is relevant from a computational point of view, since it corresponds to a necessary condition of the modular approach to programming.
Our main result tells that, despite (2), Theory of Predicates is as expressive as Theory of Constructions: the type constructors preempted by (2) are recovered in an isomorphic form using (1). In fact, Theory of Constructions is equivalent to a quotient of Theory of Predicates.
1990
Predicates and Fibrations (thesis, 18MB scan)
Abstract
The commonplace simplification of constructivist logic as a logic without the excluded middle conceals a more authentic idea of constructivism: that proofs are constructive functions, while the quantifiers should be sums and products. An exact realisation of this idea requires a very special mathematical setting. Expressed categorically, the idea is that there is a small category (of “propositions” and “proofs”), with all small sums and products (as “quantifiers”). In ordinary category theory (or over a Grothendieck topos) such a category must be a preorder, and there can be at most one “proof” leading from one “proposition” to another. In Hyland’s Effective Topos, however, a nondegenerate small complete category has been discovered recently. It can be regarded as the first mathematical model of logic with constructive proofs. On the other hand, a significant impluse to a formal development of such logics came from Computer Science, especially through the work of Coquand, Huet and their collaborators on the Calculus of Constructions.
In this thesis, we consider two mathematical formulations of constructivist logic: a type theoretical and a category theoretical. In the end, the former is completely interpreted in the latter. The purpose of such a connection is to yield a characterisation of type theoretic structures by categorical properties.