Logiken und Strukturen höherer Ordnung

In der Informatik finden sich viele Phänomene, zu deren Verständnis die Interaktion zwischen for- malen Sprachen und Strukturen besonders genau beachtet werden muss von Programmspezifika- tionen bis zu Datenbank-Abfragen. In dieser Hinsicht sind die folgenden Fragen von grundlegender Bedeutung: a) Ist die verwendete Sprache hinreichend ausdrucksstark, um damit die erforderlichen Abfragen zu spezifizieren? b) Können wir Antworten zu unseren Abfragen innerhalb einer vernünftigen Zeitspanne erwarten? Angenommen, wir wollen wissen, ob es einen Flug zwischen zwei bestimmten Städten mit höchs- tens einem Zwischen-Stopp gibt und unsere Sprache ist Prädikatenlogik erster Ordnung, dann lautet die Antwort sowohl auf (a) als auch auf (b) ja. Wollen wir aber wissen, ob es einen Flug mit einer beliebigen Anzahl von Zwischen-Stopps gibt, dann ist die Antwort auf (a) negativ, denn Prädikaten- logik erster Ordnung ist für diese Abfrage nicht hinreichend ausdrucksstark. Glücklicherweise gibt es viele Erweiterungen von Prädikatenlogik erster Ordnung, mit denen sich auch die zweite Abfrage formulieren lässt, wobei auch diese Abfrage noch innerhalb einer vernünftigen Zeitspanne ausge- wertet werden kann. Bei vielen wichtigen Abfragen geht das aber nicht mehr. Das hat zu intensiver Forschung in den Bereichen finiter Modelltheorie und Beschreibungskom- plexität geführt. Letzteres Gebiet kann als das Studium der Interaktion zwischen Logiken (formale Sprachen) und finiten (endlichen) Strukturen (Datenbanken) sowie deren Komplexität definiert wer- den. Dieses Forschungsgebiet hat in den letzten dreißig Jahren einige der grundlegendsten und tief- gehendsten Resultate der Informatik hervorgebracht. Es sind allerdings immer noch viele grundle- gende Fragen offen. Eine dieser Fragen ist, ob es Wege gibt, die Vorteile von Sprachen mit hoher Ausdrucksstärke wie etwa Logiken höherer Ordnung zu nutzen, ohne die damit verbundenen, hohen Kosten hinsicht- lich Rechenzeit für die Auswertung entsprechender Ausdrücke in Kauf nehmen zu müssen. Diese Frage ist nicht nur von theoretischem, sondern auch von hohem praktischem Interesse. Das gilt auch für die typische Art von Abfragen in der Industrie, für die zwar üblicherweise keine Logik höherer Ordnung unbedingt nötig ist, wo aber mit einer solchen Logik die Formulierung dieser Abfragen wesentlich natürlicher und auf höherer Abstraktionsebene erfolgen kann, was das Schreiben solcher Abfragen wesentlich vereinfacht. In dem eingereichten Forschungsvorhaben wollen wir dieses Problem untersuchen, wobei wir drei konkrete Untersuchungsrichtungen vorschlagen, mit denen die Verwendung hoch ausdrucksstarker Sprachen in der Industrie ermöglicht werden soll. In der ersten Stoßrichtung soll ein technischer Ansatz verwendet werden, um konkrete, steuerbare Anwendungsfälle zu identifizieren und zu klassifizieren, bei denen inhaltsreiche Ausdrücke aus- drucksstarker Sprachen höherer Ordnung verwendet werden können, um Abfragen zu vereinfachen. In der zweiten Stoßrichtung wollen wir adaptierbare Sprachen höherer Ordnung entwickeln, um semantische Web-Daten und Abfragen darauf zu modellieren. Verschachtelte Datenkollektionen werden in der Logik am natürlichsten mit Strukturen höherer Ordnung modelliert. Dadurch scheint es auch natürlich, Sprachen höherer Ordnung zur Manipulation solcher Kollektionen zu verwenden. Die dritte Forschungsrichtung zielt schließlich darauf ab, besser zu verstehen, welche Merkmale von Logiken höherer Ordnung einen tatsächlichen Einfluss auf die Ausdrucksstärke und Komplexi- tät haben. Hier wollen wir uns auf fundamentale theoretische Fragen zu Logiken über finiten Struk- turen konzentrieren.

Das Zusammenspiel formaler Sprachen und logisch-algebraischer Strukturen taucht in verschiedensten Bereichen der Informatik immer wieder auf, z.B. bei Datenbankanfragen, rigorosen Programmspezifikationen, Theorembeweisern und im Bereich künstlicher Intelligenz. Dies hat intensive Forschungsarbeiten inspiriert mit dem Ziel, die wechselseitigen Beziehungen zwischen Logik, insbesondere endlicher Modelltheorie, und Komplexitätstheorie zu verstehen und nutzbar zu machen. In den letzten 40 Jahren hat diese Forschung zu einigen der bemerkenswertesten und tiefgründigsten Ergebnis der Grundlagenforschung in der Informatik geführt. Dennoch gibt es noch viele offene Probleme. Innerhalb dieses Forschungsfelds hat das HOLS Projekt Logiken höherer Ordnung untersucht, deren Ausdrucksmächtigkeit für viele Bereiche äußerst attraktiv und relevant ist. Ein Problem ist es, diese Ausdrucksmächtigkeit für praktische Probleme nutzbar zu machen und akzeptable Kompromisse zwischen Lösungseleganz und Machbarkeit zu finden. Einige der Hauptergebnisse des Projekts betreffen dieses Kernproblem. Es ist gelungen nachzuweisen, dass es natürliche Fragmente in Logiken höherer Ordnung gibt, die interessanterweise in eine Logik niedrigerer Ordnung zusammenfallen, weil die allgemein höhere Ausdrucksmächtigkeit vor allem aus dem zusätzlichen Platz, den Relationen höherer Ordnung bereitstellen und nicht aus der tiefen Schachtelung resultiert. Die entsprechenden mathematischen Beweise sind konstruktiv und liefern damit Verfahren, die in der Praxis elegante Formulierungen komplexer Probleme ermöglichen, deren Formulierung ohne Logik höherer Ordnung extrem schwierig ist. Ein weiteres Hauptergebnis des Projekts ist die Charakterisierung sublinearer polylogarithmischer Zeitkomplexität durch semantisch eingeschränkte Fragmente der Logik zweiter Stufe und der Fixpunktlogik. Die Charakterisierung erfasst eine völlig neue Hierarchie sowohl deterministischer wie nicht-deterministischer Komplexitätsklassen. Die Relevanz dieser Klassen wurde durch zahlreiche Anwendungsbeispiele aus der Datenbanktheorie, insbesondere im Zusammenhang mit riesigen Datenmengen, untermauert. Darüberhinaus hat das Projekt zahlreiche Bezüge zu Web-Daten, abstrakten Zustandsmaschinen und anderen Gebieten hergestellt.