Logic, semirings, and fixed points

Naaf, Matthias Ferdinand; Grädel, Erich; Esparza, Javier

doi:HT030911795

Logic, semirings, and fixed points

Naaf, Matthias Ferdinand^RWTH*

2024 & 2025

Verantwortlichkeitsangabevorgelegt von Matthias Ferdinand Naaf, M.Sc.

ImpressumAachen : RWTH Aachen University 2024

Umfang1 Online-Ressource : Illustrationen

Dissertation, RWTH Aachen University, 2024

Veröffentlicht auf dem Publikationsserver der RWTH Aachen University 2025

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Grädel, Erich (Thesis advisor)^RWTH* ; Esparza, Javier (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2024-08-30

Online
DOI: 10.18154/RWTH-2024-10804
URL: https://publications.rwth-aachen.de/record/996756/files/996756.pdf

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
absorptive semirings (frei) ; fixed-point logic (frei) ; provenance analysis (frei) ; semiring semantics (frei)

Thematische Einordnung (Klassifikation)
DDC: 510

Kurzfassung
Provenienzanalyse in Halbringen ist ein erfolgreicher Ansatz aus der Datenbanktheorie der letzten zwei Jahrzehnte, der mehrere frühere Ansätze zur Provenienzanalyse vereinheitlicht. Dazu werden die Einträge einer Datenbank zunächst mit Halbringwerten beschriftet und anschließend wird eine Halbringsemantik für Datenbankabfragen definiert, die diese Werte mithilfe der Halbringoperationen verrechnet und so einen Halbringwert für jede Antwort der Abfrage liefert. Mittels verschiedener Halbringe kann ein breites Spektrum an Anwendungen abgedeckt werden: der Boolesche Halbring ergibt die konventionelle Semantik, natürliche Zahlen bilden Multimengen ab und reellwertige Halbringe Kosten oder Wahrscheinlichkeiten. Mit Polynomhalbringen lässt sich nachverfolgen, welche Einträge die Auswertung einer Abfrage beeinflussen. Dieser Ansatz war ursprünglich auf Abfragen ohne Negation beschränkt, was sich ein Jahrzehnt später durch die Einführung einer Halbringsemantik für die Prädikatenlogik geändert hat. Diese Semantik stellt eine interessante Verallgemeinerung der klassischen Booleschen Semantik auf mehrere Wahrheitswerte dar, bei der Logik und Algebra auf neuartige Weise kombiniert werden. Tatsächlich spielen algebraische Eigenschaften, Homomorphismen und universelle Halbringe eine wichtige Rolle für die Analyse dieser neuen Semantik. Das wird noch bedeutender für die Halbringsemantik von Fixpunktlogik (LFP), bei der zusätzliche Bedingungen an die Vollständigkeit und Stetigkeit des Halbrings nötig sind, um Existenz und Verhalten von kleinsten wie größten Fixpunkten sicherzustellen. Damit die Semantik aussagekräftige Informationen liefert (im Sinne der Provenienzanalyse), wird zudem angenommen, dass der Halbring absorptiv ist. Damit ist der universelle vollständig stetige und absorptive Halbring S(X) von besonderem Interesse, sowohl für die Provenienzanalyse als auch für ein besseres Verständnis der Semantik. In dieser Arbeit werden Beiträge zur Halbringsemantik für Fixpunktlogik in mehreren Bereichen vorgestellt. Eine algorithmische Fragestellung ist die Berechnung der Fixpunkte, die bei der Auswertung von LFP auftauchen. Es wurden bereits mehrere Methoden entwickelt, um kleinste Fixpunkte in Halbringen zu berechnen, wobei sich die Verallgemeinerung des Newton-Verfahrens auf Halbringe als die allgemeinste solche Methode herausgestellt hat. Bisher war jedoch nicht bekannt, wie größte Fixpunkte berechnet werden können. Für dieses Problem wird hier eine geschlossene Formel zur Berechnung größter Fixpunkte in absorptiven, vollständig stetigen Halbringen vorgestellt. Das ist zunächst ein allgemeines Ergebnis über Halbringe, hat aber auch Konsequenzen für die Ausdrucksstärke von LFP im Vergleich zu infinitärer Logik in der Halbringsemantik. Weitere Beiträge zu algebraischen Grundlagen sind die Erweiterung von S(X) um unendlich viele Unbestimmte und Koeffizienten, sowie die Einführung von unendlichen Operationen in Halbringen, die für Halbringsemantik in unendlichen Strukturen und für infinitäre Logik benötigt werden. Im Bereich der Provenienzanalyse wird anhand einer Fallstudie für Büchi-Spiele gezeigt, wie sich die Halbringsemantik von LFP für die Provenienzanalyse von unendlichen Spielen nutzen lässt. Die resultierenden Halbringwerte liefern detaillierte Informationen über Gewinnstrategien und können beispielsweise zum Finden minimaler Reparaturen am Spielgraphen verwendet werden. Der letzte Bereich ist die Modelltheorie. Hier wird untersucht, wie sich die bekannten 0-1-Gesetze über das asymptotische Verhalten von Logik auf Zufallsstrukturen für die Halbringsemantik der Prädikaten- und infinitären Logik (und damit auch LFP) in verschiedenen Halbringen formulieren lassen.

Semiring provenance is a successful approach in database theory, developed over the last two decades, that provides a unifying framework for various forms of provenance computations. This is achieved by annotating the database with semiring values and then defining a semiring semantics for query languages that combines these values using the semiring operations, ultimately producing a semiring value for each answer of the query. By using different semirings, this approach can cover a wide range of applications: the Boolean semiring yields standard semantics, the natural semiring can be used for counting and bag semantics, semirings on real numbers can model costs or probabilities, and semirings of polynomials can be used to track which facts affect the evaluation of a query. This approach was originally confined to query languages without negation, but a decade later this limitation was lifted and a semiring semantics for first-order logic was proposed. This provides an interesting generalisation of the classical Boolean semantics to multiple truth values, combining logic and algebra in a unique way. Indeed, algebraic properties, homomorphisms, and universal semirings play an important role in the study of logics under this new semantics. This becomes even more important for the semiring semantics of fixed-point logic (LFP), where additional completeness and continuity assumptions (called full continuity) on the semiring are needed to guarantee that both least and greatest fixed points exist and are well behaved. To ensure that the semantics provides meaningful information (from a provenance perspective), it is further assumed that the semirings are absorptive. Of particular interest is thus the universal fully-continuous and absorptive semiring S(X), both for provenance applications and as an important tool for understanding the semantics. In this thesis, we advance the study of semiring semantics for fixed-point logic in several directions. An algorithmic aspect concerns the computation of fixed points arising in the evaluation of LFP-formulae. Several techniques have been developed to compute least fixed points in semirings, with the generalisation of Newton's method to semirings emerging as the most general technique, but it was not known how to compute greatest fixed points. We address this problem by providing a closed-form solution for greatest fixed points of polynomial systems in absorptive, fully-continuous semirings. This is a general result about semirings, but also has implications for the expressive power of LFP compared to infinitary logic under semiring semantics. Further contributions on the algebraic side are generalisations of the universal semiring S(X) by coefficients and by infinitely many indeterminates, as well as extensions of semirings by infinitary operations that lay the foundation for semiring semantics on infinite structures and for infinitary logic. In the direction of semiring provenance, we show in a case study on Büchi games how semiring semantics for LFP can be used for provenance analysis of infinite games. The resulting provenance values provide detailed information about winning strategies and can be used, for instance, to find minimal repairs of the game arena. Lastly, we take the perspective of model theory and study how the classical 0-1 laws about the asymptotic behaviour of logic on random structures can be generalised to semiring semantics of first-order and infinitary logic (and hence LFP) for several different semirings.

OpenAccess:
PDF
(additional files)