Infinitary Rewriting of Terms, Trees and Graphs

Abstract

Computations that are supposed to transform an input into an output are usually considered meaningless if they fail to terminate within a finite amount of time. However, in certain applications infinite computations may be used to approximate the desired output arbitrarily well: the longer we let the computation run the better the approximation gets that was computed so far. Examples of this approach are the various approximation algorithms for pi. Non-strict functional programming languages, such as Haskell, make use of this technique and allow programs with conceptually infinite computations and data structures. This in fact makes for more elegant and highly modular programs. In order to do this efficiently, though, these programming languages try to minimise duplicating computation by representing the intermediate results as graphs rather than trees. In this talk, I will contrast the conceptual computations on trees with the actual computations on graphs. In particular, I will show the issues that arise once we deal with infinite computations and I will present an alternative approach that will overcome these issues.

Category: Rewriting

Tags: Infinitary Rewriting, Metric, Partial Order, Term Graph Rewriting, Term Rewriting, Completeness, Soundness