Rewriting The Finite and The Infinite

Doctoral thesis defence by Jakob Grue Simonsen

Abstract

Rewriting is the common name for a number of general methods for non-deterministic replacement of objects from a given set by other objects from the same set. The most well-studied subfield of rewriting, called term rewriting, is, roughly, the study of those phenomena that occur when replacing subformulas with other formulas according to pre-specified rules. Such sets of rules are called term rewriting systems and have been the object of much study in the scientific literature for a multitude of purposes, including modelling of proof systems, of programming language syntax and semantics, of computations in abstract models, and for concrete execution of computations in commercial software such as Maple and Mathematica.

This dissertation consists of 8 published, peer-reviewed papers and 2 introductory chapters. The dissertation is divided into three parts; Part 1 contains a broad introduction to term rewriting for the scientifically inclined layman and a short description of the scientific results of the 8 included papers; Part 2 pertains to resource
consumption in traditional rewriting systems; and Part 3 pertains to socalled infinitary rewriting where both objects and computation sequences may be infinite.

The main contributions are:
(A) A complete classification within the Arithmetical Hierarchy if undecidable problems of fundamental importance to term rewriting, specifically normalization, termination, local and global confluence.
In addition a similar classification of undecidable problems in the resource consumption necessary for normalization, including normalization in a polynomial number of steps.
(B) A determination of upper bounds for the size of confluence diagrams in first-order term rewriting and lambda calculus, including (i) a proof of the fact that any computable (total) integer function can be majorized by the size of such diagrams for a first-order term rewriting systems, (ii) that the size of such diagrams for orthogonal first-order term rewriting systems is exponential, and that this upper bound is tight.
(C) A complete characterization of the difference between weak and strong convergence in infinitary termrewriting with finite rule sets.
(D) Definitions for, and development of, the theory of higher-order infinitary rewriting, specifically infinitary combinatory reduction systems. Among the theorems proved are results that properly generalize most known results for confluence and normalization in infinitary rewriting, including infinitary lambda calculus.