Titelaufnahme

The anti-unification problem is concerned with finding a generalization for two input examples. The interesting generalizations are the least general ones. Informally, the problem can be described as: Given two concrete objects, find an expression that describes all their common features and uniformly represents their differences by variables. Such generalization problems arise in many areas of computer science and mathematics. An algorithm that computes least general generalizations for two input examples is called an anti-unification algorithm. In this work, we study the anti-unification problem for various theories. We develop algorithms that solve such problems, analyze their properties, study their computational complexity, demonstrate their usage on real world examples, and present a library of anti-unification algorithms which is implemented in Java.

Anti-unification algorithms are presented in a rule-based manner featuring a store that keeps track of all the differences at the input examples. Under certain circumstances, an algorithm that maintains such a store can be used to solve the matching problem as well as the problem of finding a join. Some of the algorithms developed in this work need a minimization step that requires to solve the matching problem. We show that those algorithms are self-minimizing in the sense that the matching problem can be solved by the anti-unification algorithm itself.

We develop anti-unification algorithms for unranked terms, nominal terms, and simply-typed lambda terms. For unranked terms, we consider first-order variables and higher-order variables. The anti-unification problem in such higher-order unranked theories is finitary but highly nondeterministic. Therefore, we impose a few natural restrictions on the computed generalizations so that we can establish a one-to-one correspondence between a generalization and a skeleton. (The skeleton consists of all those common parts of the input terms that are to be retained in the generalization.) A generalization can be computed in quadratic time for a given skeleton. This means that, for instance, if the skeleton is a constrained longest common subtree of the input terms, then both skeleton and generalization computation can be done in quadratic time.

In general, the problem of nominal anti-unification is of type zero, (i.e., a minimal complete set of generalizations does not always exist) but if the set of atoms permitted in generalizations is finite, then it becomes unitary. This is the anti-unification problem we consider for nominal terms. For simply-typed lambda terms, we restrict generalizations to be higher-order patterns so that a generalization computed for two arbitrary lambda terms is a unique pattern. (In higher-order patterns all the arguments of free variables are distinct bound variables.) We show an algorithm that computes it in quadratic time.

The implemented Java library provides anti-unification algorithms for all the theories discussed above. Such anti-unification problems arise, for instance, in proof generalization, in analogical reasoning, in detection of similarities in XML documents or in pieces of software code, etc. Therefore, our library can be a valuable ingredient for tools that need to solve such generalization problems.

Das Anti-Unifikations-Problem beschäftigt sich mit der Suche nach einer Generalisierungen (Verallgemeinerung) für zwei Eingabebeispiele. Interessant sind dabei jene Verallgemeinerungen welche am wenigsten generell sind. Informell kann das Problem wie folgt beschrieben werden: Finde einen Ausdruck für zwei konkrete Objekte welcher alle Gemeinsamkeiten beschreibt und deren Unterschiede einheitlich als Variablen darstellt. Solche Verallgemeinerungsprobleme kommen in vielen Gebieten der Computerwissenschaft und der Mathematik vor. Ein Algorithmus welcher die am wenigsten generellen Verallgemeinerungen von zwei Eingabebeispielen berechnet wird Anti-Unifikations-Algorithmus genannt. In dieser Arbeit studieren wir das Anti-Unifikations-Problem in verschiedenen Theorien. Wir entwickeln Algorithmen welche solche Probleme lösen, analysieren deren Eigenschaften, studieren deren Komplexität, demonstrieren deren Anwendung anhand von realitätsnahen Beispielen und präsentieren eine Programmbibliothek von Anti-Unifikations-Algorithmen welche in Java implementiert wurde.

Zur Präsentation der Anti-Unifikations-Algorithmen wird eine regelbasierten Methode mit einem Speicher welcher die Unterschiede in den Eingabebeispielen protokolliert verwendet. Unter gewissen Voraussetzungen kann ein Algorithmus der einen solchen Speicher besitzt sowohl das Matching-Problem als auch das Problem vom Auffinden einer gemeinsamen Instanz (Join) lösen. Manche der in dieser Arbeit entwickelten Algorithmen benötigen einen Minimierungsprozess in dem das Matching-Problem gelöst werden muß. Wir zeigen, dass diese Algorithmen selbst-minimierend sind, das heißt, dass das Matching-Problem vom Anti-Unifikations-Algorithmus selbst gelöst werden kann.

Wir entwickeln Anti-Unifikations-Algorithmen für untypisierte Terme, nominale Terme und für einfach typisierte Lambda-Terme. Für untypisierte Terme betrachten wir Variablen erster Ordnung und Variablen höherer Ordnung. Das Anti-Unifikations-Problem in solchen untypisierten Theorien höherer Ordnung ist endlich aber nicht deterministisch. Deswegen stellen wir einige wenige naturgemäße Bedingungen an die errechneten Generalisierungen, sodass wir eine eindeutige Zuordnung zwischen einer Generalisierungen und einem Gerüst erreichen. (Das Gerüst beinhaltet alle Gemeinsamkeiten der Eingabeterme welche in der Generalisierung erhalten werden.) Eine Generalisierung kann in quadratischer Zeit für ein gegebenes Gerüst berechnet werden. Das heißt, wenn zum Beispiel das Gerüst ein eingeschränkter größter Teilbaum der Eingabeterme ist, dann kann sowohl die Generalisierung als auch das Gerüst in quadratischer Zeit berechnet werden.

Generell ist das nominale Anti-Unifikations-Problem vom Typ Null (d.h., eine minimale komplette Menge von Generalisierungen existiert nicht immer). Wenn jedoch die Menge der erlaubten Atome in einer Generalisierung endlich ist, dann wird das Problem eindeutig lösbar. Dies ist das Anti-Unifikations-Problem welches wir für nominale Terme betrachten. Für einfach typisierte Lambda-Terme beschränken wir die Generalisierungen auf Pattern höherer Ordnung, sodass die errechnete Generalisierung für zwei beliebige Lambda-Terme ein eindeutiges Pattern ist. (In einem Pattern höherer Ordnung sind alle Argumente von freien Variablen unterschiedliche gebundene Variablen.) Wir zeigen einen Algorithmus welcher diese Pattern-Generalisierung in quadratischer Zeit berechnet.

Die implementierte Java-Bibliothek stellt Anti-Unifikations-Algorithmmen für alle obig diskutierten Theorien bereit. Solche Anti-Unifikations-Probleme kommen zum Beispiel in Beweisgeneralisierung, in analogischem Schlußfolgern, im Auffinden von ähnlichkeiten in XML Dokumenten oder Stücken von Softwarecode etc. vor. Daher kann unsere Programmbibliothek ein wertvoller Bestandteil für Programme sein welche solche Generalisierungsprobleme lösen müssen.