Semiring semantics: algebraic foundations, model theory, and strategy analysis

Mrkonjić, Lovro; Grädel, Erich; Tannen, Val

doi:HT031045318

Semiring semantics: algebraic foundations, model theory, and strategy analysis = Halbringsemantik: Algebraische Grundlagen, Modelltheorie und Strategieanalyse

Mrkonjić, Lovro^RWTH*

2025

Verantwortlichkeitsangabevorgelegt von Lovro Mrkonjić, Master of Science

ImpressumAachen : RWTH Aachen University 2025

Umfang1 Online-Ressource : Illustrationen

Dissertation, RWTH Aachen University, 2025

Veröffentlicht auf dem Publikationsserver der RWTH Aachen University

Genehmigende Fakultät
Fak01

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

Tag der mündlichen Prüfung/Habilitation
2025-04-14

Online
DOI: 10.18154/RWTH-2025-03940
URL: https://publications.rwth-aachen.de/record/1010223/files/1010223.pdf

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
games with imperfect information (frei) ; infinitary operations (frei) ; model theory (frei) ; semiring semantics (frei) ; separating homomorphisms (frei)

Thematische Einordnung (Klassifikation)
DDC: 510

Kurzfassung
In der Halbringsemantik werden boolesche Wahrheitswerte aus der klassischen Semantik durch Werte aus einem kommutativen Halbring $\mathcal{S}$ ersetzt. Logische Formeln $\psi$ werden nicht zu wahr oder falsch ausgewertet, sondern zu einem Wert $[\![ \psi ]\!]$ aus dem Halbring $\mathcal{S}$. Ein Wert von Null wird üblicherweise als „falsch“ interpretiert, und jeder andere Wert repräsentiert „wahr“, trägt aber abhängig vom Halbring $\mathcal{S}$ noch zusätzliche Informationen mit sich. Zum Beispiel können Polynomhalbringe $\mathbb{N}[X]$ für die Provenienzanalyse verwendet werden, das Polynom $[\![ \psi ]\!]$ liefert dann eine detaillierte Übersicht der Fakten, die zur Wahrheit von $\psi$ in einem bestimmten Modell beitragen. In der Prädikatenlogik wird die Addition des Halbrings verwendet, um Disjunktionen und Existenzquantoren auszuwerten, während die Multiplikation für Konjunktionen und Allquantoren verwendet wird. Klassische Modelle werden durch Halbringinterpretationen ersetzt, welche jedem Literal im Modell einen Halbringwert zuordnen. Dadurch kann die Modelltheorie auf Halbringinterpretationen ausgeweitet werden. Da modelltheoretische Eigenschaften der Halbringsemantik stark vom Halbring $\mathcal{S}$ abhängen, liefern wir zuerst eine Einführung in die Halbringalgebra. Dabei konzentrieren wir uns insbesondere auf Halbringe mit infinitären Operationen und Polynomhalbringe. Als wichtiges algebraisches Werkzeug in der Halbring-Modelltheorie führen wir trennende Homomorphismen ein. Diese können verwendet werden, um Sachverhalte in der Halbringsemantik durch Reduktion auf die klassische boolesche Semantik zurückzuführen. Im Gegensatz zur klassischen Modelltheorie zeigen wir, dass elementare Äquivalenz auf endlichen Halbringinterpretationen in vielen Halbringen nicht mit Isomorphie übereinstimmt, zum Beispiel in allen vollständig idempotenten Halbringen mit drei oder mehr Elementen. Trotzdem können endliche Halbringinterpretationen auf einigen Halbringen, wie zum Beispiel $\mathbb{N}$, in der Prädikatenlogik axiomatisiert werden. Zusätzlich formulieren wir den Kompaktheitssatz in der Halbringsemantik und beweisen, dass er auf endlichen Halbringen unter bestimmten Bedingungen immer noch gilt. Wir untersuchen Halbringsemantiken auch im Kontext der Spieltheorie. Die Grundidee ist, dass Positionen $v$ in einem Spiel $\mathcal{G}$ zu einem Halbringwert $\mathcal{G} [\![ v ]\!] \in \mathcal{S}$ ausgewertet werden, ausgehend von einer „Eingabebewertung“ $\ell$ der Positionen und Aktionen in $\mathcal{G}$. Es ist bekannt, dass in diesem Zusammenhang der Strategiesummensatz gilt: Die Endbewertung $\mathcal{G} [\![ v ]\!]$ entspricht der Summe der Bewertungen aller Strategien, die von $v$ ausgehen. Wir erweitern die Halbringsemantik auf Spiele mit imperfekter Information und zeigen, dass eine angepasste Variante des Strategiesummensatzes auch für solche Spiele gilt.

Semiring semantics generalizes classical semantics by replacing the classical domain of Boolean truth values with a commutative semiring $\mathcal{S}$. A logical formula $\psi$ is not evaluated to true or false, but instead to an element $[\![ \psi ]\!]$ from the semiring $\mathcal{S}$. A valuation of zero is usually interpreted as “false”, whereas a nonzero element represents “true” and carries additional information depending on the semiring $\mathcal{S}$ in question. For example, polynomial semirings $\mathbb{N}[X]$ may be used to perform provenance analysis, where the polynomial $[\![ \psi ]\!]$ provides a detailed overview of the facts that contribute to the truth of $\psi$ in a certain model. In first-order logic, semiring addition is used to evaluate disjunctions and existential quantifiers, while multiplication is used for conjunctions and universal quantifiers. Classical models are replaced with semiring interpretations which assign a semiring element to each literal of a model. This prompts the introduction of model theory to the semiring setting. Since model-theoretic properties of semiring semantics vary significantly depending on the semiring $\mathcal{S}$, we first provide an overview of semiring algebra, focusing in particular on semirings with infinitary operations and polynomial semirings. We further introduce separating homomorphisms as an important algebraic tool in semiring model theory, which can be applied to gain insights on semiring semantics by reduction to classical Boolean semantics. In contrast to classical model theory, we show that elementary equivalence on finite semiring interpretations does not coincide with isomorphism on large classes of semirings, such as the class of fully idempotent semirings with at least three elements, but first-order axiomatization of finite semiring interpretations is still possible on some specific semirings such as $\mathbb{N}$. Additionally, we generalize the classical compactness theorem to the semiring setting and prove that it holds on finite semirings with suitable algebraic properties. We also study semiring semantics in the field of game theory. The underlying idea is that positions $v$ in a game $\mathcal{G}$ are evaluated to some semiring element $\mathcal{G} [\![ v ]\!] \in \mathcal{S}$, based on “initial” semiring valuations $\ell$ of the positions and actions in $\mathcal{G}$. It is known that the sum of strategies theorem holds in this setting: The final valuation $\mathcal{G} [\![ v ]\!]$ corresponds to the sum of the valuations of all strategies starting from $v$. We extend semiring semantics to games with imperfect information and show that an adapted version of the sum of strategies theorem still holds in these games.

OpenAccess:
PDF
(additional files)