Infinitary rewriting : theory and applications

Abstract

Infinitäre Ersetzungssysteme erweitern finitäre Ersetzungssysteme durch das Einführen eines Konvergenzbegriffs für unendliche Reduktionsfolgen. Die Idee, auch unendlichen Ableitungen zumindest konzeptionell eine Bedeutung zuzuordnen, ist zum Beispiel von der nicht-strikten funktionalen Programmierung oder auch von Prozesskalkülen her bekannt. Infinitäre Ersetzung ermöglicht es, diese unendlichen Ableitungen durch Ersetzungssysteme zu formalisieren. Die vorliegende Arbeit verfolgt das Ziel, einen umfassenden Überblick über das Gebiet der infinitären Termersetzungssysteme darzulegen, dessen Defizite aufzuzeigen und zu versuchen einige dieser Defizite zu beheben.<br />Das bedeutendste Problem, welches sich bei infinitären Systemen zeigt, ist die inhärente Schwierigkeit diese endlich darzustellen, um somit eine Implementierung zu ermöglichen. Zu diesem Zweck werden Termgraphersetzungssysteme betrachtet, welche es erlauben eingeschränkte Formen infinitärer Termersetzung endlich darzustellen. Darüber hinaus untersuchen wir verschiedene Modelle der infinitären Ersetzung: die etablierte metrische Methode sowie eine alternative Methode unter Zuhilfenahme von Halbordnungen. Beide Ansätze werden -- zusammen mit den daraus resultierenden infinitären Varianten von Konfluenz- und Terminierungseigenschaften -- auf abstrakter Ebene analysiert. Darauf aufbauend erörtern wir, dass das Halbordnungsmodell vorteilhaftere Eigenschaften besitzt und die Intuition von Konvergenz natürlicher wiedergeben kann. Diese Einschätzung wird ebenso von unseren Erkenntnissen belegt, die wir für infinitäre Termersetzungssysteme erhalten: Im Gegensatz zum metrischen Ansatz erlaubt es der Halbordnungsansatz einige Resultate zu verallgemeinern, die von finitären orthogonalen Systemen bekannt sind -- insbesondere Konfluenz.<br />Es wird außerdem gezeigt, dass sogenannte Böhm-Bäume, welche üblicherweise relativ aufwendig konstruiert werden müssen, als Normalformen im Halbordnungsmodell entstehen. Schließlich werden eine vollständige Ultrametrik und ein vollständiger Halbverband auf Termgraphen entwickelt, welche beide genutzt werden um infinitäre Termgraphersetzung einzuführen. Dies soll als Instrument dienen, um die Grenzen der Möglichkeiten der Termgraphersetzung für die Implementierung der infinitären Termersetzung zu untersuchen.<br />

Infinitary rewriting generalises usual finitary rewriting by providing infinite reduction sequences with a notion of convergence. The idea of -- at least conceptually -- assigning a meaning to infinite derivations is well-known, for example, from lazy functional programming or from process calculi. Infinitary rewriting makes it possible to apply rewriting in order to obtain a formal model for such infinite derivations. The goal of this thesis is to comprehensively survey the field of infinitary term rewriting, to point out its shortcomings, and to try to overcome some of these shortcomings. The most significant problem that arises in infinitary rewriting is the inherent difficulty to finitely represent and, hence, to implement it. To this end, we consider term graph rewriting, which is able to finitely represent restricted forms of infinitary term rewriting. Moreover, we study different models that are used to formalise infinite reduction sequences: The well-established metric approach as well as an alternative approach using partial orders. Both methods together with the consequent infinitary versions of confluence and termination properties are analysed on an abstract level. Based on this, we argue that the partial order model has more advantageous properties and represents the intuition of convergence in a more natural way. This assessment is also backed up by the results that we obtain for infinitary term rewriting: Unlike the metric approach, the partial order approach admits to generalise some results known from finitary orthogonal term rewriting -- most importantly, confluence. It is also shown that so-called Böhm trees, usually constructed rather intricately, naturally arise as normal forms in the partial order model. Finally, we devise a complete ultrametric and a complete semilattice on term graphs both of which are used to introduce infinitary term graph rewriting.<br />This is supposed to serve as a tool in order to investigate the limitations of term graph rewriting for implementing infinitary term rewriting.