Symmetries in Reversible Programming
University of Glasgow
Abstract:
Classical models of computation are not resource-conscious, which
led to a long line of research in logic and computer science on
designing various languages for expressing resource-conscious
computation. Embracing the physical nature of computation, and
using the information-theoretic notion of resource, the idea
behind reversible computing is that computation should be done in
an information-preserving way, using invertible
functions. Reversible programs are usually expressed as
reversible boolean functions, reversible boolean gates, or
sequences of reversible operations on bits, which can be run
forwards or backwards on a reversible computer.
What should be the right high-level language for reversible
programming? Sabry and collaborators designed a family of
languages using type isomorphisms in the lambda calculus, for
writing total reversible programs. In this talk, I will discuss
my work on understanding their semantic foundations.
I will discuss categorical and denotational semantics for this
family of languages, showing a Lambek correspondence between
reversible computation and symmetric rig groupoids, and giving a
fully-complete denotational semantics. I will show some
applications of this semantics to perform
normalisation-by-evaluation, verification, and synthesis of
reversible boolean gates motivated by examples from quantum
computing.