• category theory
• concurrency
• semantics

The notion of permutation equivalence for term rewriting systems represents a cornerstone in the formalization of the theory of concurrency. In this context, a categorical formulation for (full) permutation equivalence can be readily achieved by constructing a free 2-category over a given Lawvere theory, using rewriting rules as generating 2-cells. This is a technique introduced by Meseguer.

A similar construction can be obtained by replacing 2-categories with sesquicategories, yielding a different notion of permutation equivalence which we call "flat".

However, even a simple formal system like the untyped lambda-calculus can be represented as a rewriting system only if one is allowed to add axioms for alpha-conversion. The presence of axioms invalidates the neat correspondence between the classical notion of permutation equivalence for the lambda-calculus and the Meseguer construction.

Namely, it can be shown that two additional axiom schemes need to be added to the Meseguer system, in order to account for the critical pairs arising from the interaction between axioms and transitions.

In this thesis, we propose a free construction of a Meseguer-like sesquicategory, without additional ad-hoc axioms, giving a purely categorical description of permutation equivalence for the lambda-calculus, and more generally for combinatory reduction systems. We base our construction on the "presheaf" semantics by Fiore et al.

The idea is to use a richer structure in the base category to represent the "behaviour" of terms, so that when this structure is transposed on the level of sesquicategories by a free construction, the same behaviour holds for transitions (i.e. 2-cells).

This thesis only deals with the flat case. The case of full permutation equivalence can be obtained by working with 2-categories instead of sesquicategories, but the proof of the correspondence theorem seems to present some technical difficulties.