CANA Seminar - 19_03_2024.mp4 [19 mars 2024]

 Description

‘‘A categorical framework to study logical properties of systems and processes’‘
by Nicolas Blanco (Postdoc at CEA)

 

Abstract:

Categorical quantum mechanics and applied category theory are fields that study systems and processes by abstracting the main structures and properties of their models. A focus is put on compositionality: how to compose processes together and to describe complex systems from their subsystems. An important structure studied in these fields is given by compact closed categories. They correspond to models of one-to-one processes that can be sequentially composed (a category), where systems and processes can be composed in parallel (a tensor/monoidal product) and each system has a dual system that reverse the flow of information. Processes with many inputs and outputs can then be modelled as processes between the tensor product of the inputs and the tensor product of the outputs.

Linear logic is a substructural logic where the information in a proof cannot be duplicated nor erased. That is, every hypothesis has to be used exactly once. It is closely connected to linear type theory through a Curry-Howard correspondence. Through categorical semantics one can study the structures and properties of its models. An important structure in this field is given by *-autonomous categories. These correspond to models of one-to-one proofs that can be sequentially composed (a category), where logical propositions can be composed in two ways, the conjunction and disjunction (two monoidal products, the tensor and the par), and where each proposition can be negated (a duality). Proofs with many hypotheses and many conclusions can then be modelled as proofs from the conjunction of the hypotheses to the disjunction of the conclusions.

It turns out that a compact closed category is exactly a *-autonomous category where the two monoidal products coincide, i.e. the conjunction and disjunction have the same interpretation. This lead to a line of research exploring the connection between linear logic and quantum mechanics, amongst others. For example, Aleks Kissinger and Sander Uijlen showed that starting with a compact closed category modelling systems and processes, one can studied their causal structure logically by organising the causal systems and processes into a *-autonomous category.

In this talk, I will consider these connections by adopting a slightly different perspective. Instead of considering one-to-one processes or proofs, I will take many-to-many ones as a primitive, in a structure called a polycategory. The monoidal products (and the duals) will then be recovered through a universal property akin to the one of the tensor products of vector spaces. This will determine the interpretation of the composition of systems or logical propositions uniquely, up-to unique isomorphism, instead of having it provided as extra data. Furthermore, it will make apparent another defining distinction between the compact closed and the *-autonomous models: in the latter the sequential composition is done along one specific object while in the former two processes can be composed along multiple systems. In particular compact closed categories allow for feedback and loops while *-autonomous categories don't.

I will then introduce bifibred polycategories explaining how they can be used to model the emergence of a logical framework structuring systems equipped with specific conditions. They are in part inspired by Hoare logic, a framework used in computer science to reason about and verify properties of programs. As an example, I will consider the case of finite dimensional Banach spaces and contractive polylinear maps. Finite dimensional vector spaces and polylinear maps will provide a model of systems and processes while the norms will be used to express conditions on states of the systems via (sub-)unitality. Another example is given by the aforementioned construction of causal structures.

If time permits, I will present some research directions I am considering to extend this framework.