11/03/2004
Jakob Grue-Simonsen (University of Copenhagen)
Infinitary Term Rewriting

Infinitary term rewriting is an extension of ordinary (first-order) term rewriting allowing for transfinite reduction sequences converging to limits. The last 15 years have witnessed the slow development of the field, culminating in the general setting of so-called strongly convergent rewriting.

In the talk, we will review basic definitions and problems of infinitary term rewriting, sketch a proof of confluence by orthogonality, and briefly touch upon infinitary lambda calculus. In addition, we will present some recent results on modularity issues and the differences between weak and strong convergence.