Substitution Without Copy and Paste

Grundlegende Informationen

• Paper-ID: 2510.12304
• Titel: Substitution Without Copy and Paste
• Autoren: Thorsten Altenkirch (University of Nottingham), Nathaniel Burke (Imperial College London), Philip Wadler (University of Edinburgh and Input Output)
• Klassifizierung: cs.LO (Logik in der Informatik)
• Veröffentlichungskonferenz: LFMTP 2025 (International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice)
• Paper-Link: https://arxiv.org/abs/2510.12304

Zusammenfassung

Bei der Definition von Substitutionsoperationen für Sprachen mit Bindern (wie dem einfach typisierten λ-Kalkül) ist es üblich, Substitutions- und Umbenennungsoperationen separat zu definieren, was zu erheblicher Code-Duplizierung führt. Um die kategorischen Eigenschaften des Kalküls zu verifizieren, müssen identische Argumente mehrfach wiederholt werden. Dieses Paper präsentiert einen leichtgewichtigen Ansatz zur Vermeidung dieser Wiederholungen und konstruiert eine einfach typisierte CwF (Contextual Weak Functor), die isomorph zu einer Familie initialer einfach typisierter CwFs ist. Das Paper wird als literarisches Agda-Programmierskript präsentiert.

Forschungshintergrund und Motivation

Kernproblem

Bei der mechanisierten Beweisführung zur Definition von Substitutionsoperationen für Sprachen mit Bindern erfordert die traditionelle Methode:

1. Separate Definition von Variablenumbennung (∆ ⊩v Γ) und Termsubstitution (∆ ⊩ Γ)
2. Wiederholte Implementierung von vier verschiedenen Substitutionsoperationen: Variable-zu-Variable, Variable-zu-Term, Term-zu-Variable, Term-zu-Term
3. Wiederholte Beweise aller Kombinationen von Funktorgesetzen, was zu 8 verschiedenen Beweisfällen führt

Forschungsmotivation

1. Softwareentwicklungsprinzipien: Vermeidung von Copy-Paste-Code, was in der formalen Beweisführung besonders wichtig ist
2. Theoretische Bedeutung: Bereitstellung einer Grundlage für Substitutionsdefinitionen in abhängig typisierten Theorien
3. Praktische Anwendung: Interpretation abhängig typisierter Theorien in höheren Kategorien

Einschränkungen bestehender Methoden

• Code-Duplizierung: Ähnliche Operationen müssen separat für Variablen und Terme definiert werden
• Beweis-Duplizierung: Kategorische Gesetze erfordern Beweise für alle Kombinationen, was zu erheblichen Wiederholungen führt
• Wartungsschwierigkeiten: Änderungen an einer Stelle erfordern Synchronisierung mehrerer ähnlicher Definitionen

Kernbeiträge

1. Einheitliches Framework: Präsentation eines einheitlichen Substitutionsoperators basierend auf Sort-Parametrisierung, der die Behandlung von Variablen und Termen in einer einzigen Definition zusammenführt
2. Terminierungsgarantie: Geschickte Nutzung von Agdas struktureller Rekursion und lexikographischer Terminierungsprüfung zur Gewährleistung der Wohldefiniertheit
3. Kategorische Verifikation: Beweis, dass die rekursive Definition der Substitution alle Gesetze der einfach typisierten CwF erfüllt
4. Initialitätsergebnis: Etablierung eines Isomorphismus zwischen der rekursiven Substitutionssyntax und der initialen CwF
5. Normalisierungssatz: Die Normalform der Substitution von λ-Termen entspricht λ-Termen ohne explizite Substitution

Methodische Details

Aufgabenstellung

Konstruktion eines einheitlichen Substitutionssystems, das:

• Eingabe: Beliebige Kombinationen von Termen/Variablen und Substitutionen/Umbenennungen
• Ausgabe: Entsprechende Substitutionsergebnisse
• Einschränkungen: Beibehaltung von Typsicherheit und Terminierung

Kerntechnik: Sort-System

Sort-Typdefinition

data Sort : Set where
  V : Sort
  T>V : (s : Sort) → IsV s → Sort

data IsV : Sort → Set where
  isV : IsV V

pattern T = T>V V isV

Diese Definition macht V strukturell kleiner als T und erfüllt damit die Anforderungen von Agdas Terminierungsprüfung.

Einheitliche Definitions von Termen und Substitutionen

data _ ⊢ [_]_ : Con → Sort → Ty → Set where
  zero : Γ ▷ A ⊢ [ V ] A
  suc : Γ ⊢ [ V ] A → (B : Ty) → Γ ▷ B ⊢ [ V ] A
  `_ : Γ ⊢ [ V ] A → Γ ⊢ [ T ] A
  _ ·_ : Γ ⊢ [ T ] A ⇒ B → Γ ⊢ [ T ] A → Γ ⊢ [ T ] B
  λ_ : Γ ▷ A ⊢ [ T ] B → Γ ⊢ [ T ] A ⇒ B

Dabei entspricht Γ ⊢ [ V ] A Variablen und Γ ⊢ [ T ] A Termen.

Gitterstruktur auf Sort

data _ ⊑ _ : Sort → Sort → Set where
  rfl : s ⊑ s
  v⊑t : V ⊑ T

_⊔_ : Sort → Sort → Sort
V ⊔ r = r
T ⊔ r = T

Einheitliche Substitutionsoperation

Kern-Substitutionsfunktion

_[_] : Γ ⊢ [ q ] A → ∆ ⊩ [ r ] Γ → ∆ ⊢ [ q ⊔ r ] A

Schlüsseleinsicht: Der Sort des Ergebnisses ist die kleinste obere Grenze der Input-Sorts, was sicherstellt, dass das Ergebnis nur dann eine Variable ist, wenn beide Eingaben Variablen/Umbenennungen sind.

Terminierungsbehandlung

Lösung des Terminierungsproblems durch Sort-polymorphe Identitätsfunktion:

id-poly : Γ ⊩ [ q ] Γ
id : Γ ⊩ [ V ] Γ
id = id-poly {q = V}

Technische Innovationen

1. Strukturierte Rekursion: Nutzung der Sortstruktur und lexikographischer Maße zur Gewährleistung der Terminierung
2. Parametrischer Polymorphismus: Einheitliche Behandlung verschiedener Fälle von Variablen und Termen durch Sort-Parameter
3. Gittertheorie-Anwendung: Elegante Behandlung von Typerhöhung durch die ⊔-Operation
4. Umschreiberegeln: Nutzung von Agdas REWRITE-Funktionalität zur Vereinfachung der Gleichheitsbeweisführung

Theoretische Verifikation

Kategorische Gesetze

Identitätsgesetz

[id] : x [ id ] ≡ x

Beweis durch strukturelle Induktion; der Schlüssel ist ein Naturheitssatz für den Variablenfall.

Assoziativgesetz

[◦] : x [ xs ◦ ys ] ≡ x [ xs ] [ ys ]

Erfordert gegenseitige Rekursion mit dem linken Identitätsgesetz, was die innere Verbindung der kategorischen Struktur widerspiegelt.

CwF-Strukturverifikation

Das Paper beweist, dass die rekursive Substitutionssyntax alle Axiome der einfach typisierten CwF erfüllt:

• Kategorische Struktur: Kontexte und Substitutionen bilden eine Kategorie
• Prägarben-Struktur: Jeder Typ entspricht einer Prägarbe
• Terminales Objekt: Der leere Kontext
• Kontexterweiterung: Struktur ähnlich dem kategorischen Produkt

Initialitätssatz

Etablierung von Abbildungen in beiden Richtungen:

1. Normalisierung norm : Γ ⊢I A → Γ ⊢ [ T ] A
2. Einbettung ⌜_⌝ : Γ ⊢ [ q ] A → Γ ⊢I A

und Beweis, dass sie zueinander invers sind:

• Stabilität norm ⌜ t ⌝ ≡ t
• Vollständigkeit ⌜ norm t ⌝ ≡ t

Implementierungsdetails

Nutzung von Agda-Funktionen

1. Induktiv-induktive Typen: Gegenseitige Definition von Sort und IsV
2. Lexikographische Terminierung: Unterstützung komplexer Rekursionsmuster
3. Umschreiberegeln: Automatisierung der Gleichheitsbeweisführung
4. Muster-Synonyme: Vereinfachung der Verwendung komplexer Typen

Terminierungsanalyse

Beweis der Terminierung durch Aufrufgraphanalyse; das Maß für jede Funktion:

• _[_]: (r, t)
• id: (r, Γ)
• _+_: (r, σ)
• suc[_]: (q)

In allen Zyklen nimmt entweder der Sort streng ab, oder der Sort bleibt gleich während andere Parameter abnehmen.

Vergleich mit verwandten Arbeiten

Unterschiede zu bestehenden Methoden

1. Kit-Methode18,5: Abstraktion gemeinsamer Muster von Umbennung und Substitution durch Kits, erfordert aber immer noch wiederholte Beweise
2. Monadische Perspektive6,9: Kodierung von Substitution als Funktion von Variablen zu Termen, schwer auf abhängige Typen erweiterbar
3. Automatisierungswerkzeuge21,22: Die Autosubst-Bibliothek generiert automatisch Substitutionslemmata, aber die Grundlage enthält immer noch Wiederholungen

Vorteilsanalyse

1. Einfachheit: In Sprachen mit Unterstützung für lexikographische Rekursion einfacher
2. Einheitlichkeit: Eine einzige Definition deckt alle Fälle ab
3. Erweiterbarkeit: Grundlage für die Behandlung abhängig typisierter Theorien

Schlussfolgerungen und Diskussion

Hauptschlussfolgerungen

1. Methodischer Beitrag: Beweis, dass Sort-Parametrisierung Substitutionsoperationen elegant vereinheitlichen kann
2. Theoretischer Beitrag: Etablierung der Initialität der rekursiven Substitutionssyntax
3. Praktischer Beitrag: Bereitstellung konkreter technischer Lösungen zur Vermeidung von Wiederholungen

Einschränkungen

1. Abhängigkeit von Agda-Funktionen: Erfordert Unterstützung für lexikographische Terminierungsprüfung
2. Komplexitätsverlagerung: Obwohl Wiederholungen vermieden werden, erhöht sich die Komplexität des Sort-Systems
3. Erweiterungsherausforderungen: Erweiterung auf abhängige Typen erfordert weitere Forschung

Zukünftige Richtungen

1. Erweiterung auf abhängige Typen: Anwendung der Methode auf vollständige abhängig typisierte Theorien
2. Höhere Kohärenz: Anwendungen in höheren Kategorien
3. Andere Beweisassistenten: Portierung auf Lean, Coq und andere Systeme

Tiefgreifende Bewertung

Stärken

1. Technische Innovativität: Das Sort-System-Design löst elegant das Terminierungs- und Einheitlichkeitsproblem
2. Theoretische Vollständigkeit: Vollständige theoretische Entwicklung von grundlegenden Definitionen bis zur Initialität
3. Praktischer Wert: Bietet praktische Lösungen für häufige Probleme in der formalen Verifikation
4. Klare Darstellung: Als literarisches Programmierskript ist die Kombination von Code und Erklärung gut gelungen

Schwächen

1. Plattformabhängigkeit: Starke Abhängigkeit von spezifischen Agda-Funktionen, begrenzte Portabilität
2. Komplexitäts-Tradeoff: Obwohl Wiederholungen vermieden werden, werden neue konzeptuelle Komplexitäten eingeführt
3. Unbekannte Erweiterbarkeit: Erweiterung auf komplexere Typensysteme erfordert weitere Verifikation

Einfluss

1. Theoretischer Beitrag: Bietet neue Perspektiven für die Mechanisierung von Typtheorie
2. Praktische Anleitung: Bietet nützliche Werkzeuge für Praktiker der formalen Verifikation
3. Forschungsinspiration: Legt Grundlagen für weitere Forschung in abhängig typisierten Theorien

Anwendungsszenarien

1. Formale Verifikation: Sprachdefinitionen, die mit Bindern umgehen müssen
2. Typtheorie-Forschung: Forschung zu CwF und initialen Algebren
3. Programmiersprachen-Theorie: Mechanisierung des λ-Kalküls und seiner Erweiterungen

Literaturverzeichnis

Das Paper zitiert wichtige Arbeiten in diesem Bereich, darunter:

• De Bruijns Originalarbeit12
• McBrides Kit-Methode18
• Allais et al. typensichere Ansätze5
• Autosubst-Serie21,22
• Verwandte Forschung zu relativen Monaden6

Diese Zitate zeigen das tiefe Verständnis des Autors für die Entwicklung des Feldes und die gründliche Recherche bestehender Arbeiten.