Richard Kennaway

Term rewriting and graph rewriting as models of computation

This is a field in which I am no longer active. My work in this area included the following topics:

  • Category-theoretic descriptions of graph rewriting.
  • Transfinite term rewriting. With my co-authors I established the basic concepts and theorems for a generalisation of term rewriting which allows infinitely long computations converging to possibly infinite results. This has close connections with lazy functional programming, in which one can in effect compute with infinite data structures.
  • Transfinite lambda calculus. We established similar results for the lambda calculus (essentially, term rewriting with bound variables and higher-order functions).
  • Formal notions of undefinedness in rewrite systems, giving a notion of denotational semantics for term rewrite systems, an interpretation of Böhm trees in lambda calculus as transfinite normal forms, and a unification of the concepts of Böhm tree, Lévy-Longo tree, and Berarducci tree.
  • Translatability of term rewrite systems to lambda calculus.
  • The complexity of translating lambda calculus to combinators.
  • DACTL, a compiler target language based on graph reduction.
  • I was the local organiser of the 11th International Conference on Rewriting Techniques and Applications, and the associated 3rd Workshop on Explicit Substitutions and Applications, which took place on 10-13 July 2000 at UEA.