Explizite Substitution

Ein Kalkül expliziter Substitutionen ist eine Erweiterung des Lambda-Kalküls, bei dem die Substitution auf die gleiche Weise wie die Abstraktion oder die Anwendung in den Kalkül integriert wird, während im Lambda-Kalkül die Substitution Teil der Metatheorie ist , dass ist, es ist außerhalb der Theorie des Lambda-Kalküls definiert.

Prinzip

Die Idee, die zur Erklärung der Substitutionen führt, ergibt sich aus dem Wunsch, die Substitution als eigenständige Operation zu behandeln, indem sie in die Syntax integriert und eine bestimmte Anzahl von Regeln hinzugefügt wird, die die Substitution verteilen und anwenden und Teil davon sind. der Berechnung ebenso wie die β-Reduktion Teil des Lambda-Kalküls ist. Das Interesse an der Integration der Substitution in die Berechnung besteht darin, über die Substitution sowohl in Bezug auf Implantation, Komplexität, Effizienz oder Bewertungsstrategie als auch in Bezug auf die β-Reduktion sprechen zu können . Dies kann das Teilen , die verzögerte oder verzögerte Bewertung oder die sofortige Bewertung erklären . Eine Substitution, die in einem Begriff vorkommt, kann sofort bewertet werden oder ihre Bewertung kann verschoben werden, wenn dies erforderlich ist. Darüber hinaus kann die Bewertung einer Substitution an mehreren Stellen verwendet werden und erfordert nur eine Berechnung ( gemeinsame Nutzung ).

Reichhaltige Syntax

Damit das formale System gleichzeitig von Abstraktion und Anwendung sowie von Substitution sprechen kann, muss die Syntax des Lambda-Kalküls mit einem expliziten Substitutionsoperator angereichert werden. Es gibt zwei Möglichkeiten, dies zu tun, je nachdem, ob Sie mit expliziten Variablen oder mit de Bruijn-Indizes arbeiten .

Erforderliche Eigenschaften

Hier sind einige Eigenschaften, die durch ein System expliziter Substitutionen erfüllt werden sollen. Zunächst sind Eigenschaften erforderlich.

Es gibt auch optionale Eigenschaften, die man sich wünschen kann.

Varianten

Es gibt verschiedene Berechnungen expliziter Substitutionen. Dies kann auf zwei Arten erklärt werden:

Im Allgemeinen behalten Systeme, die in Bezug auf Meta-Begriffe konfluent sind, keine starke Normalisierung bei und umgekehrt. Diejenigen, die diese beiden Eigenschaften erfüllen, sind nicht einfach.

Die λx-Berechnung

Das λx-System verwendet explizite Variablennamen und verfügt über vier Regeln für das Substitutionssystem sowie eine Regel zur Eliminierung von β-Redex und damit zur Simulation der β-Reduktion.

(b)  : (λx.M) N → M⟨x: = N⟩ (xvI)  : x⟨x: = P⟩ → P. (xvK)  : x⟨y: = P⟩ → x (x ≠ y) (xap)  : (MN) ⟨x: = P⟩ → (M⟨x: = P⟩) (N⟨x: = P⟩) (xab)  : (λx.M) ⟨y: = P⟩ → λx. (M⟨y: = P⟩) (x ≠ y)

Das λx-System behält die starke Normalisierung bei . Wir können die folgende Regel hinzufügen, die die Regel (xvK) verallgemeinert und daher ersetzt .

(xgc)  : M⟨x: = P⟩ → M (x∉var (M))

Regelübersicht

Die Berechnung λυ

Die Berechnung λυ verwendet de Bruijn-Indizes. Es gibt also keine Variablen mehr, sondern nur Metavariablen. Λυ enthält keine gebundenen Variablen mehr und ist ein Umschreibungssystem erster Ordnung . Die syntaktischen Ergänzungen sind wie folgt.

⇑ (s): 0 ↦ 0 1 ↦ s (0) [ ↑ ] 2 ↦ s (1) [ ↑ ] ⁞ n + 1 (s (n) [ ↑ ] ⁞ (B)  : (λM) N → M [N /] (App)  : (MN) [s] → M [s] N [s] (Lambda)  : (λ M) [s] → λ (M [ ⇑ (s)]) (FVar)  : 0 [M /] → M. (RVar)  : n + 1 [M /] → n (FVarLift)  : 0 [ ⇑ (s)] → 0 (RVarLift)  : n + 1 [ ⇑ (s)] → n [s] [ ↑ ] (VarShift)  : n [ ↑ ] → n + 1

Die Berechnung λυ bewahrt die starke Normalisierung .

Regelübersicht

Die ersten drei Regeln entsprechen den äquivalenten Regeln von Lambda-x. Beispielsweise eliminiert Regel (B) einen Beta-Redex und führt eine explizite Substitution ein.

Die λσ-Berechnung

Die λσ-Berechnung ist die ursprüngliche Berechnung von Abadi, Cardelli, Curien und Lévy. Zusätzlich zu den Operatoren der Berechnung λυ hat diese Berechnung

Es gibt weder einen Operator ⇑ noch eine Substitution M / .

Die λσ-Berechnung

(Beta)

(λ M) N → M [N · id]

(App)

(MN) [s] → M [s] N [s]

(Abs)

(λ M) [s] → λ (M [0 · (s ∘ ↑)])

(Geschlossen)

M [s] [t] → M [s ∘ t]

(VarId)

0 [Id] → 0

(VarCons)

0 [Frau] → M.

(IdL)

id ∘ s → s

(ShiftId)

↑ ∘ id → ↑

(ShiftCons)

↑ ∘ (M. S) → s

(AssEnv)

(s ∘ t) → u → s ∘ (t ∘ u)

(MapEnv)

(M. S) → t → M [t]. (s ∘ t)

Während die Substitutionen von λυ angeben, was dem Index 0 und seinen Avataren zuzuweisen ist, wenn er in λ versinkt, und wie die anderen Indizes als 0 verschoben werden sollen, gruppieren die Substitutionen von λσ in einer einzigen Substitution die Zuordnungen zu allen Indizes und dafür Sie enthalten einen Kompositionsoperator.

Geschichte

Die Idee der expliziten Substitution wird im Vorwort zu Curry und Feys 'Buch über kombinatorische Logik skizziert, erhält jedoch in der Arbeit von Bruijn im Zusammenhang mit dem Automath- System den Status eines realen Systems zum Umschreiben von Begriffen . Im Gegensatz dazu werden das Konzept und die Terminologie normalerweise Martín Abadi , Luca Cardelli , Curien und Lévy zugeschrieben . In einem Artikel, der der erste einer langen Reihe sein wird, stellen die Autoren den λσ-Kalkül vor und zeigen, dass der Lambda-Kalkül im Hinblick auf die Substitution mit großer Aufmerksamkeit untersucht werden muss. Ohne ausgeklügelte Mechanismen zur gemeinsamen Nutzung von Strukturen können Substitutionen in der Größe explodieren.

Anmerkungen und Referenzen

  1. Delia Kesner: Eine Theorie expliziter Substitutionen mit sicherer und vollständiger Zusammensetzung. Logische Methoden in der Informatik 5 (3) (2009)
  2. M. Abadi, L. Cardelli, PL. Curien und JJ. Levy, Explicit Substitutions, Journal of Functional Programming 1, 4 (Oktober 1991), 375–416.
  3. (in) Haskell Curry und Robert Feys , Combinatory Logic Volume I , Amsterdam, Nordholland Verlag,1958
  4. NG de Bruijn: Ein namensfreier Lambda-Kalkül mit Funktionen zur internen Definition von Ausdrücken und Segmenten. Technologische Universität Eindhoven, Niederlande, Fakultät für Mathematik, (1978), (TH-Bericht), Nummer 78-WSK-03.

Literaturverzeichnis

Siehe auch