Towards Weak Stratification for Logics of Definitions

Technische Zusammenfassung: Hin zu schwacher Stratifizierung für Logiken der Definitionen

Problemstellung
Die Logik der Definitionen ist eine Familie von Logiken, die verwendet werden, um Urteile zu kodieren und über sie zu schlussfolgern, welche durch Inferenzregeln spezifiziert sind, wobei atomare Prädikate mit logischen Formeln assoziiert sind, die von dem Prädikat selbst abhängen können. Um die inhärente scheinbare Zirkularität solcher Definitionen zu lösen, erzwingen Standardansätze eine Stratifizierungsbedingung, die sicherstellt, dass ein Prädikat nicht negativ (links von einer Implikation) im Körper seiner eigenen Definition erscheint. Diese Bedingung behandelt Definitionen effektiv als monotone Fixpunktoperatoren.

Viele nützliche Spezifikationen, insbesondere jene, die logische Relationen für den Beweis von Eigenschaften von Programmiersprachen erfordern, benötigen jedoch Definitionen, in denen das Prädikat negativ erscheint. In der Logik $\mathcal{G}$, die der Abella-Proof-Assistant zugrunde liegt, sind solche Definitionen nicht zulässig. Tiu [19] führte zuvor eine Logik namens $\mathcal{LD}$ ein, welche die Stratifizierungsbedingung zu einer schwachen Stratifizierung lockert (erlaubt negative Vorkommen, sofern das Level des Kopfes strikt größer als das Level des negativen Vorkommens ist), wobei $\mathcal{LD}$ jedoch auf ein Kernfragment beschränkt war. Es fehlte die Unterstützung für den Nabla-Quantor ($\nabla$), der essenziell für das Schließen über Namen und Frische mittels nominaler Konstanten ist, sowie für allgemeine induktive Definitionen jenseits der natürlichen Zahleninduktion. Die Herausforderung, die sich diese Arbeit stellt, besteht darin, die Logik der Definitionen so zu erweitern, dass sie schwache Stratifizierung unter Beibreibung von $\nabla$ und allgemeinen induktiven Definitionen unterstützt und dabei die Konsistenz wahrt.

Methodik
Das Paper definiert eine neue Logik, $\mathcal{LD}\mu\nabla$, welche Tius $\mathcal{LD}$ um Nabla-Quantifizierung und allgemeine induktive Definitionen erweitert. Die Methodik vollzieht sich in drei Hauptphasen:

1. Syntax und Semantik von $\mathcal{LD}\mu\nabla$:
   Die Logik wird als Erweiterung eines prädikatenlogischen Sequenzenkalküls mit einer Menge von Definitionen $\mathcal{D}$ und einer Menge von induktiven Definitionen $\mathcal{I}$ formuliert.

• Schwache Stratifizierung: Eine Definitionsmenge $\mathcal{D}$ ist schwach stratifiziert, wenn für jede Klausel $H \triangleq_X B$ und jede Grundsubstitution $\rho$ gilt: $\text{lvl}(H\rho) \ge \text{lvl}(B\rho)$. Entscheidend ist, dass dies negative Vorkommen des definierten Prädikats erlaubt, sofern das Level des Kopfes strikt größer als das Level des negativen Vorkommens ist.
• Strikte Stratifizierung für Induktion: Das Paper legt eine strengere Bedingung für induktive Definitionen $\mathcal{I}$ fest: Diese müssen strikt stratifiziert sein (das Level eines grundlegenden atomaren Prädikats muss unabhängig von seinen Argumenten sein). Diese Einschränkung ist notwendig, um Inkonsistenzen zu verhindern, die beim Kombinieren von Induktion mit schwacher Stratifizierung auftreten könnten.
• Nabla-Quantor: Die Logik beinhaltet den $\nabla$-Quantor, um mit nominalen Konstanten und Frische umzugehen, wobei zwischen generischen und spezifischen Instanzen von Namen unterschieden wird.

2. Grundlogik und Interpretation:
   Um die Konsistenz zu beweisen, konstruieren die Autoren eine grundlegende Version der Logik, $\mathcal{LD}\mu\nabla_\infty$, in der alle Formeln grundlegend sind (keine Eigenvariablen).

• Grundlegendes Lemma (Grounding Lemma): Ein entscheidender technischer Schritt ist der Beweis, dass jede Ableitung in $\mathcal{LD}\mu\nabla$ via einer Grundsubstitution als eine Ableitung in $\mathcal{LD}\mu\nabla_\infty$ interpretiert werden kann. Dies reduziert das Konsistenzproblem der vollen Logik auf die Konsistenz der Grundlogik.
• Infinitäre Regeln: In $\mathcal{LD}\mu\nabla_\infty$ werden die Standard-$\forall R$- und $\exists L$-Regeln durch infinitäre Regeln ersetzt, die über alle Grundterme quantifizieren, und die $\mu L$-Regel für Induktion wird analog dazu erweitert, um alle Grundinstanzen abzudecken.

3. Cut-Elimination:
   Der Kern des Konsistenzbeweises ist die Eliminierung der Cut-Regel (speziell der Multicut-Regel) in $\mathcal{LD}\mu\nabla_\infty$.

• Reduktionsrelation: Eine Reduktionsrelation wird auf Ableitungen definiert, die spezifiziert, wie Cuts nach oben gedrückt oder eliminiert werden können.
• Reduzierbarkeit: Folgend der von McDowell und Miller adaptierten Tait-Martin-Löf-Technik definieren die Autoren einen Begriff der Reduzierbarkeit (und Normalisierbarkeit) für Ableitungen. Sie beweisen, dass jede Ableitung in $\mathcal{LD}\mu\nabla_\infty$ reduzierbar ist.
• Behandlung induktiver Fälle: Ein kritischer Aspekt des Beweises ist der Umgang mit der Interaktion zwischen schwacher Stratifizierung und Induktion. Die Autoren zeigen, dass während schwache Stratifizierung für allgemeine Definitionen ausreicht, induktive Definitionen strikt stratifiziert bleiben müssen. Sie liefern ein Gegenbeispiel (Abschnitt 3.3), das demonstriert, dass das Zulassen schwach stratifizierter induktiver Definitionen zu logischer Inkonsistenz führt.

Hauptbeiträge

• Definition von $\mathcal{LD}\mu\nabla$: Das Paper definiert formal eine Logik, die schwache Stratifizierung, Nabla-Quantifizierung und allgemeine induktive Definitionen kombiniert.
• Konsistenzbeweis: Der primäre Beitrag ist der Beweis, dass $\mathcal{LD}\mu\nabla$ konsistent ist. Dies wird durch den Nachweis der Cut-Elimination für die Grundlogik $\mathcal{LD}\mu\nabla_\infty$ und die Etablierung einer Grundinterpretation erreicht.
• Stratifizierungsbeschränkungen: Die Arbeit klärt die Grenze zwischen zulässigen und unzulässigen Definitionen. Sie zeigt, dass schwache Stratifizierung für allgemeine Definitionen ausreicht (was logische Relationen ermöglicht), induktive Definitionen jedoch eine strikte Stratifizierung erfordern, um die Konsistenz zu bewahren.
• Gegenbeispiel: Das Paper liefert ein spezifisches Gegenbeispiel, das zeigt, dass die Lockerung der Stratifizierungsbedingung für induktive Definitionen zu logischer Inkonsistenz führt, was die für $\mathcal{I}$ auferlegte Einschränkung rechtfertigt.

Ergebnisse

• Konsistenz: Es wird bewiesen, dass die Logik $\mathcal{LD}\mu\nabla$ konsistent ist. Folglich besitzt die Logik $\mathcal{LD}\mu\nabla_\infty$ cut-freie Ableitungen für alle beweisbaren Sequenzen.
• Inversions-Eigenschaften: Das Paper etabliert metatheoretische Eigenschaften für $\mathcal{LD}\mu\nabla_\infty$, einschließlich der Invertierbarkeit verschiedener Einführungsregeln (z. B. $\wedge R$, $\vee L$, $\nabla R$) und einer spezifischen partiellen Invertierbarkeit für $\vee R$, $\exists R$ und Definitionsregeln ($\Delta R$), wenn der Kontext leer ist. Diese Eigenschaften sind entscheidend für Beweissuchverfahren.
• Limitierungen: Der Cut-Elimination-Satz wird nur für die Grundlogik $\mathcal{LD}\mu\nabla_\infty$ etabliert. Das Paper merkt an, dass die Erweiterung dieses Ergebnisses auf die volle Logik $\mathcal{LD}\mu\nabla$ (mit Eigenvariablen) eine offene Herausforderung bleibt.

Bedeutung
Die Bedeutung dieser Arbeit liegt in ihrem Potenzial, die Fähigkeiten des Abella-Proof-Assistants zu erweitern. Abella basiert auf der Logik $\mathcal{G}$, welche derzeit Definitionen auf eine strikte Stratifizierung beschränkt. Indem diese Arbeit die Aufnahme schwach stratifizierter Definitionen rechtfertigt, ebnet sie den Weg für Abella, logische Relationen nativ zu unterstützen – eine fundamentale Technik zum Beweis semantischer Eigenschaften von Programmiersprachen (wie Typsicherheit und Compilerkorrektheit).

Das Paper positioniert diese Arbeit als einen grundlegenden Schritt hin zu einer breiteren Erweiterung von $\mathcal{G}$. Während das aktuelle Resultat die Handhabung von schwacher Stratifizierung mit $\nabla$ und Induktion behandelt, merken die Autoren an, dass eine vollständige Rechtfertigung für Abella weitere Erweiterungen zur Einbeziehung von Ko-Induktion und nominaler Abstraktion erfordern würde. Die Arbeit hebt zudem die Notwendigkeit hervor, die strikte Stratifizierung für induktive Definitionen beizubehalten, eine Einschränkung, die die Inkonsistenzen verhindert, die andernfalls durch die Mischung von schwacher Stratifizierung mit Induktion entstehen würden.