Topological Convergence in Infinitary Abstract Rewriting

Abstract

Rewriting is a field on the border of logic, mathematics and theoretical computer science. It studies the stepwise transformation of objects and as such applies to a lot of processes in computer science, systems in mathematics and also formalized stepwise processes in other fields of science. Abstract rewriting studies properties those processes might have, independent of the concrete structure of the objects and the steps. Examples are properties like termination (modeling that processes terminate) and confluence (modeling that finite divergent processes starting from a common source can be extended to reach a common target). Infinitary abstract rewriting studies processes of infinite length and as such is concerned with convergence (modeling that the processes in some sense get arbitrarily close to some intended target).

In this thesis I study the foundations of rewriting in general and infinitary abstract rewriting in particular. Infinitary abstract rewriting is still very much work-in-progress and various frameworks exist. I compare these frameworks and their formalizations and note some deficiencies. I also propose a framework of my own based on topological convergence, a notion of convergence derived from the mathematical branch of general topology. This framework is proven to encompass the two main existing frameworks and has desirable technical properties.