TallCat
Webpage of the Compositional Systems and Methods group at TalTech.
27 May 2021, 14:00, online
Speaker
Torie Barrett, University of Bath
Title
Atomic flows and normalisation
Abstract
Atomic flows, developed by Tom Gundersen and Alessio Guglielmi, are graphical constructions which correspond to derivations and track occurrences of atoms. They allow us to talk about paths through derivations and connected components of atoms.
First I will discuss the result of Gundersen and Guglielmi that atomic flows can be used to prove cut elimination in a surprisingly beautiful way. The procedure for this is global; we take very little information from inside the proof.
One current line of research, investigated by Andrea Aler Tubella, Ben Ralph, and Alessio Guglielmi, is into the cyclic structures that can occur between identities and cuts. What role do these play in the compression of proofs, and can they be removed in a way that does not affect the overall complexity of the proof as much as the global procedure? Flows play a crucial role here but it is necessary to look at part of the proof that are not recorded in atomic flows.
I will also discuss my current work in extending flows to all connectives, and the similarities between different logical systems that this highlights. This work is rooted in the work of Aler Tubella and Guglielmi on subatomic logic, regarding atoms as self-dual non-commutative connectives and allowing many rules from many logical systems to follow a single linear rule shape. In particular we are able to give generalised reduction rules by means of generalised flows for connectives. One obstacle in designing flows that capture all connectives arises from non-linear equality rules; I will show a recent result that these non-linear equality rules can be eliminated, leaving only the subatomic rule shape.