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:
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
- 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