ETD

• category theory
• diagrammatic reasoning
• polyhedral cones
• string diagrams

Diagrammatic reasoning has been successful in many areas of sciences, from engineering to computer science to mathematics. Many examples include Petri nets for concurrency theory, signal flow graphs for control theory, proof nets in proof theory and many more.

These kinds of languages provide an intuitive way to express and reason about some foundational structures that are often formalised via usual mathematical language.

In this thesis we focus on an extension of Interacting Hopf Algebras (IH), a theory of linear relations which is faithfully represented in terms of string diagrams and whose semantics is given as arrows of a PROP (a symmetric monoidal category).

The extension consists in adding one new operator to IH that represents an order relation over a field. The extended theory allows for a characterisation of a special kind of convex cones: polyhedral cones.

We propose a sound and complete axiomatization of the denotational semantics, which also allows to rephrase some well-know properties/theorems about polyhedral cones (e.g. the Weyl-Minkowski theorem) in a completely diagrammatic and axiomatic way.

In the end we discuss a possible application of the theory to concurrency.