Math and Logic


Monoidal computer I: Basic computability by string diagrams

We present a new model of computation, described in terms of monoidal categories. It conforms the Church-Turing Thesis, and captures the same computable functions as the standard models. It provides a succinct categorical interface to most of them, free of their diverse implementation details, using the ideas and structures that in the meantime emerged from research in semantics of computation and programming. The salient feature of the language of monoidal categories is that it is supported by a sound and complete graphical formalism, string diagrams, which provide a concrete and intuitive interface for abstract reasoning about computation. The original motivation and the ultimate goal of this effort is to provide a convenient high level programming language for a theory of computational resources, such as one-way functions, and trapdoor functions, by adopting the methods for hiding the low level implementation details that emerged from practice. Only a modest first step towards this ambitious goal is presented.


A new description of orthogonal bases --- with Bob Coecke and Jamie Vicary

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.


Maps II: chasing diagrams in categorical proof theory

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.


A categorical setting for the 4-Colour Theorem

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

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

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.


Chu I: cofree equivalences, dualities and *-autonomous categories

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.


On the structure of paradoxes

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.


Constructions and Predicates

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.


Categorical Interpolation: Descent and the Beck-Chevalley Condition without Direct Images

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.

Predicates and Fibrations (thesis, 18MB scan)

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.