York Semigroup: Self-referentiality and reflexivity in inverse monoids

Event details

This talk describes and discusses 'reflexive' mathematical structures -- i.e. those that are isomorphic to their own function space.  Such structures originally arose in logic and theoretical computer science, in particular as models of untyped lambda calculus and similar logical / computational systems.  More recently, such structures have been discussed in the context of cognitive science, systems biology, and cryptography.The best-known examples of such structures are the C-monoids of Jim Lambek and Phillip Scott, with particular examples being the provided by the Scott domains of Dana Scott. From a categorical point of view, these may be seen as single-object categories (i.e. monoids) that satisfy the axioms of Cartesian closure. We describe how the Cartesian closure of sets and functions provides models for the simply typed lambda calculus, and how C-monoids provide an 'untyped' version where the operations are not restricted by any typing system.The principal question this talk addresses is whether we may find the same properties in the reversible setting - i.e. based on inverse monoids?  This is indeed the case, although doing so requires moving from Cartesian closure to more general forms of categorical closure. The computational interpretation also requires considering models of computability that are strictly 'lower-level' than untyped lambda calculus.  The resulting structures are inverse monoids that were originally derived from models of J.-Y. Girard's linear logic.  They provide a link between the seemingly distinct descriptions of computability given by Turing machines and lambda calculus, and also have a close connection with structures underlying quantum computation.Unavoidably, this talk is quite heavily algebraic and categorical. The basics of category theory (categories, functors, products, & tensors) will be assumed, along with the definitions of generalised inverses, and inverse semigroups.  However, no a priori knowledge of the logical / computational applications will be assumed (e.g. lambda calculus, combinators, Turing machines, natural deduction, & linear logic).