💻 computer science

Well-Scoped Locally Nameless Representation of Syntax

Dieser Beitrag stellt eine generische, gut abgegrenzte, lokal benannte Syntaxdarstellung für Agda vor, die durch Plotkin-artige Bindungssignaturen parametrisiert ist, belegt ihre Angemessenheit gegenüber einer naiven, benannten Syntax modulo Alpha-Konversion und demonstriert ihren Nutzen anhand von Beispielen.

Ursprüngliche Autoren: Andrew M. Pitts

Veröffentlicht 2026-05-12

📖 5 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Andrew M. Pitts

Originalarbeit lizenziert unter CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dies ist eine KI-generierte Erklärung des untenstehenden Papers. Sie wurde nicht von den Autoren verfasst oder gebilligt. Für technische Genauigkeit konsultieren Sie das Originalpaper. Vollständigen Haftungsausschluss lesen

Stellen Sie sich vor, Sie sind ein Bibliothekar, der versucht, eine riesige, chaotische Bibliothek zu organisieren, in der Bücher auf andere Bücher innerhalb ihrer eigenen Seiten verweisen können. Manche Bücher haben Titel auf ihren Umschlägen (wie „Der große Gatsby"), während andere nur nummerierte Regale in einem bestimmten Abschnitt bezeichnen (wie „Regal 3, Reihe 2").

Dieser von Andrew Pitts verfasste Artikel beschreibt eine neue, intelligentere Methode, diese Bibliothek zu organisieren, damit Computer (speziell „interaktive Theorembeweiser" wie Agda) die Regeln der Bibliothek überprüfen können, ohne verwirrt zu werden oder Fehler zu machen.

Hier ist die Aufschlüsselung der Ideen des Artikels unter Verwendung einfacher Analogien:

1. Das Problem: Das Dilemma „Namenslos" versus „Benannt"

Wenn Informatiker versuchen, einem Computer Sprachen beizubringen (wie Programmiersprachen oder Logik), müssen sie sich mit Variablen auseinandersetzen.

Die „benannte" Methode: Sie geben jeder Variablen einen Namen, wie x, y oder z. Dies ist für Menschen leicht zu lesen, aber Computer geraten in Verwirrung, wenn Sie Namen austauschen (ein Problem, das als „Alpha-Konvertierung" bekannt ist). Ist x dasselbe wie y, wenn Sie sie umbenennen?
Die „namenslose" Methode (De-Bruijn-Indizes): Sie verzichten vollständig auf Namen. Stattdessen sagen Sie einfach „die 1. Variable", „die 2. Variable" usw., wobei Sie von innen nach außen zählen. Dies ist großartig für Computer, aber schrecklich für Menschen, da es wie ein durcheinandergeratenes Durcheinander von Zahlen aussieht.

2. Die alte Lösung: „Lokal benannt"

Vor einigen Jahren entwickelten Forscher eine hybride Idee namens Lokal benannt.

Freie Variablen (Dinge, die nicht in einer Schleife oder Funktion gebunden sind) behalten ihre Namen (wie x).
Gebundene Variablen (Dinge innerhalb einer Schleife) verwenden Zahlen (wie 0, 1).

Der Haken: Dieses System hat eine „Falle". Es erlaubt Ihnen, „kaputte" Terme zu erstellen, bei denen die Zahlen nicht zum Gültigkeitsbereich passen. Stellen Sie sich ein Buch vor, das sagt: „Gehen Sie zu Regal 5", Sie sich aber gerade in einem Raum befinden, der nur 3 Regale hat. Der Computer muss ständig prüfen: „Ist dieser Term 'lokal geschlossen' (gültig)?". Dies erfordert eine Menge zusätzlicher Beweisarbeit, wie ein Bibliothekar, der ständig überprüft, ob ein Buch im richtigen Gang steht, bevor er jemandem erlaubt, es auszuleihen.

3. Die neue Lösung: „Gut skopierter lokal benannt"

Dieser Artikel schlägt einen besseren Weg vor: Gut skopierter lokal benannt.

Anstatt nur Zahlen zu verwenden, nutzt der Computer Typen, um die Regeln durchzusetzen.

Stellen Sie sich die Bibliothek als verschiedene „Räume" vor.
Wenn Sie sich in Raum 0 befinden, können Sie nur Regale mit den Nummern 0 bis 0 sehen (was bedeutet: keine Regale, nur freie Namen).
Wenn Sie sich in Raum 1 befinden, können Sie die Regale 0 und 1 sehen.
Wenn Sie sich in Raum 5 befinden, können Sie die Regale 0 bis 5 sehen.

Die Magie: In diesem System können Sie buchstäblich kein kaputtes Buch erstellen. Wenn Sie versuchen, „Gehen Sie zu Regal 10" zu schreiben, während Sie in Raum 2 stehen, sagt das Typsystem des Computers: „Nein, das ist unmöglich. Sie können diesen Satz nicht einmal schreiben."

Der Artikel argumentiert, dass dieser Ansatz:

Die „Falle" entfernt: Sie müssen keine zusätzlichen Beweise schreiben, um zu prüfen, ob ein Term gültig ist. Die Tatsache, dass der Term existiert, beweist, dass er gültig ist.
Transparent ist: Es sieht immer noch größtenteils wie die „benannte" Methode aus, an die Menschen gewöhnt sind, sodass es nicht so verwirrend ist wie die reine „namenslose" Methode.
Allgemeingültig ist: Die Autoren haben eine „Bibliothek" (eine Reihe von Werkzeugen) erstellt, die für jede Sprache funktioniert, die Sie definieren möchten, solange Sie die Regeln der Bindung (wie if-Anweisungen oder lambda-Funktionen funktionieren) mit einer Standardvorlage beschreiben.

4. Wie es funktioniert (das „Öffnen" und „Schließen")

Der Artikel beschreibt zwei Hauptoperationen, die wie das Verschieben von Büchern zwischen Räumen sind:

Abstraktion (Schließen): Einen freien Namen (wie x) nehmen und in einen gebundenen Index (wie 0) verwandeln. Dies ist wie das Nehmen eines Buches vom Regal und das Einlegen in einen spezifischen nummerierten Schlitz in einem neuen Raum.
Konkretion (Öffnen): Einen gebundenen Index nehmen und durch ein spezifisches Buch (Term) ersetzen. Dies ist wie das Herausnehmen eines Buches aus einem Schlitz und das Einsetzen eines echten Buches an seine Stelle.

Die Autoren beweisen, dass ihre „gut skopierte" Mathematik perfekt funktioniert. Sie zeigen, dass ihr neues System mathematisch äquivalent zum alten „benannten" System ist, was bedeutet, dass sie exakt dieselben Konzepte repräsentieren, nur sicherer organisiert.

5. Reale Beispiele

Der Artikel spricht nicht nur über Theorie; sie testeten ihre „Bibliothek" an drei verschiedenen Arten von Sprachen:

Der Pi-Kalkül: Eine Sprache, die verwendet wird, um zu beschreiben, wie Computerprogramme miteinander sprechen (wie Telefonanrufe). Hier sind Namen „Kanäle" für die Kommunikation.
Martin-Löf-Typentheorie: Ein komplexes System für mathematische Beweise. Sie zeigten, wie man Regeln für natürliche Zahlen und Typen schreibt, ohne sich in der „Frische" der Namen zu verirren.
Gödels System T: Ein System zum Beweis, dass Berechnungen schließlich enden (Entscheidbarkeit). Sie verwendeten ihre Methode, um zu beweisen, dass ein spezifischer Algorithmus korrekt funktioniert.

Das Fazit

Der Artikel sagt: „Hören Sie auf, manuell zu prüfen, ob Ihre Variablen am richtigen Ort sind. Lassen Sie das Typsystem des Computers die schwere Arbeit für Sie erledigen."

Durch die Verwendung von abhängigen Typen (ein Merkmal der Programmiersprache Agda) schufen sie ein System, in dem ungültige Syntax unmöglich zu schreiben ist. Dies spart Forschern das Schreiben von Tausenden Zeilen langweiliger Beweiscode nur, um zu sagen: „Ja, diese Variable ist im Gültigkeitsbereich." Es macht formale Verifikation (den Beweis, dass Software fehlerfrei ist) einfacher, sicherer und näher daran, wie Menschen natürlich über Sprache nachdenken.

Technisches Zusammenfassung: Wohl-gescopete lokal benannte Darstellung der Syntax

Problemstellung
Bei der Formalisierung von Sprachen mit Bindungskonstrukten (z. B. $\lambda$ -Kalkül, Typsysteme) in interaktiven Theorembeweisern, die auf abhängigen Typentheorien basieren (wie Agda, Lean oder Rocq), besteht eine zentrale Herausforderung im Management von Variablenbindung und $\alpha$ -Äquivalenz. Der Ansatz „lokal benannt" (locally nameless), der freie Variablen als explizite Namen und gebundene Variablen als de-Bruijn-Indizes darstellt, hat sich als geeignet erwiesen, die PoplMark-Kriterien für geringen Infrastrukturaufwand, Transparenz und einfache Einstiegsmöglichkeiten zu erfüllen. Allerdings leiden Standard-Darstellungen im lokal benannten Stil unter einem kritischen Mangel: Die induktive Definition von Termen erlaubt „hängende" Indizes (Indizes, die den aktuellen Scope überschreiten). Um Korrektheit zu gewährleisten, muss die Domäne auf eine Teilmenge „lokal geschlossener" Terme beschränkt werden. Dies erfordert wiederholte, manuelle Beweise, dass Operationen (wie Substitution) die lokale Geschlossenheit erhalten, was eine erhebliche Belastung darstellt und eine Fehlerquelle in formalen Entwicklungen bildet.

Methodik
Der Artikel schlägt eine „wohl-gescopete" Variante der lokal benannten Darstellung vor, die das abhängige Typsystem von Agda nutzt, um lokale Geschlossenheit intrinsisch durchzusetzen, anstatt sie als separates Prädikat zu definieren.

Indizierte induktive Typen: Anstelle eines einzigen Term-Typs definiert die Bibliothek eine Familie von Typen Trm[n], indiziert durch eine natürliche Zahl $n$ . Ein n-Term ist ein Term, bei dem alle de-Bruijn-Indizes aus dem endlichen Typ Fin n (natürliche Zahlen kleiner als $n$ ) stammen.
Lokal geschlossene Terme als 0-Terme: In diesem Rahmen entsprechen „lokal geschlossene" Terme (jene ohne hängende Indizes) exakt Trm[0]. Terme mit freien Variablen werden als Trm[n] dargestellt, wobei $n$ der Anzahl der freien Variablen im Scope entspricht.
Parametrisierung durch Bindungssignaturen: Die Bibliothek ist generisch und parametrisiert durch eine Plotkin-artige Bindungssignatur. Dies ermöglicht die Definition von Operatoren, deren Stelligkeit und der Anzahl der Namen, die in jeder Argumentposition gebunden werden.
Operationen via abhängige Typen:
- Scope-Abschwächung (Weakening): Eine Funktion Trm[m] -> Trm[n] (für $m \le n$ ), die Indizes injiziert und die erforderliche Verschiebung beim Übergang zu einem größeren Scope behandelt.
- Konkretion (Öffnung): Ersetzen eines Index $i$ in einem (1+n)-Term durch einen 0-Term, um einen n-Term zu erzeugen. Dies beinhaltet das Herunterverschieben von Indizes größer als $i$ um eins.
- Abstraktion (Schließen): Ersetzen eines freien Namens in einem n-Term durch einen Index, um einen (1+n)-Term zu erzeugen. Dies beinhaltet das Hochverschieben von Indizes.
- Substitution: Strukturell definiert. Da die Substitutionsfunktion Namen auf 0-Terme (Trm) abbildet, wird die Bedingung „lokal geschlossen" automatisch durch das Typsystem erzwungen. Substitution an einem n-Term ergibt einen weiteren n-Term.

Hauptbeiträge

Die WSLN-Bibliothek: Eine generische Agda-Bibliothek, die wohl-gescopete lokal benannte Terme implementiert. Sie bietet die Infrastruktur zur Definition von Syntax, Operationen (Abschwächung, Substitution, Abstraktion, Konkretion) und Schlussfolgerungsprinzipien für jede Sprache, die durch eine Plotkin-Bindungssignatur spezifiziert ist.
Formaler Angemessenheitsbeweis: Der Artikel liefert einen rigorosen Beweis, der eine Bijektion herstellt zwischen:
1. Dem Typ der wohl-gescopeten lokal benannten 0-Terme (Trm[0]).
2. Den $\alpha$ -Äquivalenzklassen von „namenbehafteten" Termen (Termen mit expliziten Namen für sowohl freie als auch gebundene Variablen).
  Diese Bijektion zeigt, dass die wohl-gescopete Darstellung die Semantik der capture-vermeidenden Substitution und der $\alpha$ -Äquivalenz korrekt erfasst.
Eliminierung von Beweisen für lokale Geschlossenheit: Durch die Kodierung von Scope-Einschränkungen in den Typindizes entfällt die Notwendigkeit für explizite „lokal geschlossene"-Prädikate und die damit verbundenen Beweisverpflichtungen (z. B. der Nachweis, dass Substitution lokale Geschlossenheit erhält). Diese Eigenschaften werden zu Konsequenzen der Typregeln.
Handhabung von Frische: Die Bibliothek integriert sich mit nominalen Techniken, indem sie eine „endlich unerschöpfliche" Menge von Atomen (natürliche Zahlen) verwendet, um frische Namen über kofinite Quantifizierung zu generieren und sicherzustellen, dass Frischebedingungen systematisch behandelt werden.

Ergebnisse
Der Artikel validiert den Ansatz durch drei verschiedene Beispiele, die in Agda implementiert wurden:

$\pi$ -Kalkül: Demonstriert die Anwendbarkeit der Bibliothek über den $\lambda$ -Kalkül hinaus, indem Prozessausdrücke und Kanalnamen behandelt werden. Es wird hervorgehoben, dass die Bibliothek zwar die Bindungsstruktur handhabt, die Typüberprüfung auf Wohlgeformtheit (z. B. Sicherstellen, dass Kanäle dort verwendet werden, wo erwartet) jedoch eine separate, benutzerdefinierte Urteil bleibt.
Martin-Löf-Typentheorie (MLTT): Zeigt, wie die Bibliothek die Definition von Typregeln erleichtert. Sie kontrastiert „exists-fresh"-Regeln (die explizite Frischeannahmen erfordern) mit „kofiniten Quantifizierungs"-Regeln (bei denen Frische implizit ist) und demonstriert, dass die wohl-gescopete Darstellung Letztere unterstützt, was zu saubereren und transparenteren Formalisierungen führt.
Gödels System T (Normalisierung durch Auswertung): Eine erhebliche Entwicklung, die die Entscheidbarkeit der $\beta\eta$ -Konversion beweist. Dieses Beispiel veranschaulicht, wie die wohl-gescopete Darstellung die Semantik der Abstraktion und den Umgang mit Frische in komplexen semantischen Konstruktionen (setoid-wertige Prägarben) vereinfacht und die Notwendigkeit endlich unterstützter semantischer Objekte vermeidet.

Bedeutung und Behauptungen
Der Artikel behauptet, dass die wohl-gescopete lokal benannte Darstellung eine „einfache" yet leistungsstarke Lösung für die „Falle" der hängenden Indizes bietet, die in traditionellen lokal benannten Ansätzen zu finden ist. Ihre primäre Bedeutung liegt darin, die Last der Sicherstellung der Scope-Korrektheit vom Benutzer (durch manuelle Beweise) auf den Typchecker des Theorembeweisers (durch abhängige Typen) zu verlagern.

Die Autoren betonen, dass dieser Ansatz die für die PoplMark-Kriterien erforderliche Transparenz wahrt: Formale Definitionen spiegeln informelle Konventionen eng wider, und das „Index-Yoga" (Manipulation von de-Bruijn-Indizes) ist innerhalb der Operationen der Bibliothek gekapselt. Obwohl die Implementierung eine sorgfältige Handhabung endlicher Ordinalzahlen (Fin n) und Indexverschiebungen erfordert, parametrisiert die Bibliothek diese Komplexität und ermöglicht es Benutzern, Sprachen zu definieren und Eigenschaften zu beweisen, ohne niedriglevelige Scope-Mechaniken verwalten zu müssen. Der Artikel vermerkt bescheiden, dass die aktuellen Bindungssignaturen unsortiert sind und einfache Bindungsscope modellieren, der Ansatz jedoch robust genug ist, um komplexe Typsysteme und semantische Beweise zu handhaben, wie die Entwicklung von System T belegt.