Techniken für unbeschränkte Terme im symbolischen Rechnen

Sprachen über unbeschräenkten Alphabeten haben in den vergangenen Jahren wegen ihrer vielfältigen Anwendungen verstärktes Interesse erfahren. Mit ihnen kann man in natürlicher Weise XML-Dokumente, Programm-Schemen, Ambiente, parallele rekursive Programmkonfigurationen mit unbeschränkter Anzahl gleichzeitig laufender Prozesse, mehrstellige Funktionen in verschiedenen Programmiersprachen und vieles mehr modellieren. Sie treten auch im Zusammenhang mit Rewriting, Wissensrepräsentation, Softwareanalyse und Programmtransformation auf, um nur einige zu nennen. Die unbeschränkten Terme, die uns interessieren, können sogenannte Context- und Hedge-Variablen enthalten, die Reihenfolge der Argumente mancher Funktionen kann irrelevant sein, oder es kann Sorten und Bedingungen an Variable geben, die durch reguläre Sprachen formuliert werden. Dieser Rahmen ist reichhaltig genug um interessante Anwendungen zu modellieren. Forschung über Techniken des Symbolischen Rechnens (lösen, beweisen, berechnen) für unbeschränkte Terme wird noch nicht sehr lange betrieben. In diesem Projekt betrachten wir den Aspekt des Lösens wegen seiner grundlegenden Bedeutung. Insbesondere werden wir zwei duale Techniken betrachten: Unifikation und Anti- Unifikation. Diese werden für Ausdrücke von erster und zweiter Ordnung untersucht werden, mit und ohne Sorten, syntaktisch und bezüglich einer Gleichungstheorie. Das generelle Ziel ist es, Algorithmen und Prozeduren zu entwickeln, sie zu analysieren, effiziente Speziallfälle herauszuarbeiten, sie zu implementieren und sie auf interessante "real-world"-Probleme anzuwenden.

Unifikation und Anti-Unifikation sind zwei duale Techniken des symbolischen Rechnens. Mit Hilfe von Unifikation werden Gleichungen zwischen zwei gegebenen Ausdrücken gelöst, indem die generellste gemeinsame Instanz berechnet wird. Mit Hilfe von Anti-Unifikation werden Gemeinsamkeiten zwischen zwei gegebenen Ausdrücken gefunden und deren Unterschiede abstrahiert, indem die spezifischste (bzw. am wenigsten generelle) Verallgemeinerung berechnet wird. Beide Techniken haben breite Anwendungsgebiete in verschiedenen Bereichen wie etwa der automatischen Schlussfolgerung, Softwareentwicklung, künstlichen Intelligenz, Bioinformatik, Linguistik usw.Im SToUT-Projekt haben wir diese Techniken für Sprachen über Alphabete mit variabler Arität, und einigen damit verwandten Formalismen, studiert. Sprachen mit variabler Arität haben in den letzten Jahren aufgrund ihrer Nutzbarkeit in verschiedenen modernen Anwendungen große Aufmerksamkeit erregt. Wir entwickelten, analysierten und implementierten Algorithmen zur Lösung von Gleichungen (und allgemeineren Konzepten) für Sprachen erster und zweiter Ordnung, wobei die Typinformationen entweder durch reguläre Ausdrücke oder mit Hilfe regulärer Sprachzugehörigkeitsconstraints dargestellt werden; Anti-Unifikations-Algorithmen für Sprachen mit variabler Arität erster und zweiter Ordnung, und in höherer (Lambda-Kalkül) und nominaler Sprache. Es wurde eine Open Source Algorithmus-Bibliothek erstellt, welche Online verfügbar ist. Außerdem haben wir interessante Anwendungen dieser Techniken in der Programmierung, Design-Theorie, und Bioinformatik aufgezeigt.Zusammenfassend hat das SToUT-Projekt wichtige Beiträge zur Entwicklung von Unifikations-, Constraintlösungs- und Anti-Unifikationsalgorithmen und -methoden in verschiedenen Sprachen und Formalismen geleistet. Es wurden auch neue Forschungsfragen aufgeworfen, welche wir bereits begonnen haben zu untersuchen.