Logo eprints

Logical completeness for string diagrams

Seeber, Jens (2020) Logical completeness for string diagrams. Advisor: De Nicola, Prof. Rocco. Coadvisor: Bonchi, Dr. Filippo . pp. 154. [IMT PhD Thesis]

[img] Text (Doctoral thesis)
Seeber_phdthesis.pdf - Published Version
Available under License Creative Commons Attribution Non-commercial Share Alike.

Download (823kB)

Abstract

String diagrams can be used as a compositional syntax for different kinds of computational structures. This thesis views string diagrams through a logical/universal algebraic perspective – diagrams represent formulas, allowing the use of diagrammatic reasoning for proofs. The category theoretic backdrop of this playground is given by the concept of Cartesian bicategory – a categorical algebra of relations – that we consider as a relational theory through the lens of functorial semantics. Given a Cartesian bicategory, functorial semantics provides us with an appropriate notion of model as a structure-preserving functor to the category of sets and relations. Functoriality implies that diagrammatic reasoning is sound. The central question this approach raises and that we shall settle is the question of completeness in the logical sense: does every property that is shared by all models have a diagrammatic proof? The main result of the thesis is a positive answer to the above question. To show this, we give a combinatorial characterisation of Cartesian bicategories in terms of hypergraphs equipped with interfaces, inspired by a seminal result by Chandra and Merlin. This reduces the problem of logical completeness to a categorical lifting problem that we solve using a transfinite construction and a compactness argument.

Item Type: IMT PhD Thesis
Subjects: Q Science > QA Mathematics > QA75 Electronic computers. Computer science
PhD Course: Computer science and systems engineering
Identification Number: 10.6092/imtlucca/e-theses/317
Date Deposited: 24 Jul 2020 09:42
URI: http://e-theses.imtlucca.it/id/eprint/317

Actions (login required, only for staff repository)

View Item View Item