MSc Defence by Xiaomo Yao

Reversible Computation with Types


Reversible computing is an emerging research area that studies about the backward as well as the forward determinism of models of computation. A traditional computing device, such like the regular Turing machine, does not inherently preserve the information of its input throughout the computational process; in other words, conventional computations are subject to information effects. We study the notion of reversibility, in the hope of finding pure models of computation that are free of such information effects.

The approach taken in this thesis arises from a functional programmer’s perspective: The invertibility and compositionality of partial functions are surveyed as crucial properties in a functional programming language for reversible computation. A type system, BT, inspired by computation in symmetric monoidal categories, is formally defined. By embedding the information-preserving injection types by subkinding, conventional higher-order functions are distinguished from invertible ones by types. In the same fashion resembling type checking of terms, inversion of type isomorphisms may also be done decidably by deduction.

Based upon the specified type system, we propose a general-purpose functional programming language, BEYOND, that is reversibility-aware, in the sense that both conventional and reversible computations are supported, and types also provide a static guarantee for the reversibility of programs aside from their correctness. The invertibility of pattern matching on algebraic data types, as well as on refined primitive types, can be inferred algorithmically.

Furthermore, heuristics based on induction are developed so as to infer the invertibility of recursive functions with fixed-point semantics.

Supervisors: Robin Kaarsgaard and Robert Glück.