Înlocuirea explicită

Un calcul al substituțiilor explicite este o extensie a calculului lambda în care substituția este integrată în calcul în același mod ca și abstractizarea sau aplicația, în timp ce în calculul lambda, substituția face parte din metateorie , că este, este definit în afara teoriei lambda-calculului.

Principiu

Ideea care duce la explicarea substituțiilor provine din dorința de a trata substituția ca o operație de sine stătătoare prin integrarea ei în sintaxă și prin adăugarea unui anumit număr de reguli care distribuie și aplică substituția și care fac parte din ea. a calculului la fel cum β-reducerea face parte din lambda-calcul. Interesul integrării substituției în calcul este acela de a putea vorbi despre substituție și în ceea ce privește implantarea, complexitatea, eficiența sau strategia de evaluare, precum și în relația sa cu reducerea β . Acest lucru poate explica schimbul , evaluarea întârziată sau leneșă sau evaluarea imediată. O înlocuire care apare într-un termen poate fi evaluată imediat sau evaluarea acesteia poate fi amânată, atunci când este nevoie. În plus, evaluarea unei înlocuiri poate fi utilizată în mai multe locuri și necesită doar un singur calcul ( partajare ).

Sintaxă bogată

Pentru ca sistemul formal să poată vorbi în același timp de abstractizare și aplicare, precum și de substituție, este necesar să se îmbogățească sintaxa lambda-calculului cu un operator de substituție explicit. Există două modalități de a face acest lucru, în funcție de faptul dacă lucrați cu variabile explicite sau cu indici de Bruijn .

Proprietăți necesare

Iată câteva proprietăți pe care vrem să le vedem satisfăcute de un sistem de substituții explicite. În primul rând sunt proprietăți necesare.

Există, de asemenea, proprietăți opționale pe care cineva le dorește.

Variante

Există mai multe calcule ale substituțiilor explicite. Acest lucru poate fi explicat în două moduri:

În general, sistemele care sunt confluente cu termeni meta nu păstrează o normalizare puternică și invers. Cei care satisfac aceste două proprietăți nu sunt simpli.

Calculul λx

Sistemul λx folosește nume de variabile explicite și are patru reguli pentru sistemul de substituție, plus o regulă pentru a elimina β-redex și astfel a simula β-reducere.

(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)

Sistemul λx păstrează normalizarea puternică . Putem adăuga următoarea regulă care generalizează și, prin urmare, înlocuiește regula (xvK) .

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

Prezentare generală a regulilor

Calculul λυ

Calculul λυ utilizează indicii de Bruijn. Prin urmare, nu mai există variabile, ci doar meta-variabile. Nu mai conține variabile legate, λυ este un sistem de rescriere de primă ordine . Adăugările sintactice sunt după cum urmează.

⇑ (s): 0 ↦ 0 1 ↦ s (0) [ ↑ ] 2 ↦ s (1) [ ↑ ] ⁞ n + 1 ↦ s (n) [ ↑ ] ⁞ (B)  : (λ M) N → M [N /] (Aplicație)  : (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

Calculul λυ păstrează normalizarea puternică .

Prezentare generală a regulilor

Primele trei reguli corespund regulilor echivalente ale lambda-x, de exemplu, regula (B) elimină un beta-redex și introduce o substituție explicită.

Calculul λσ

Calculul λσ este calculul inițial al lui Abadi, Cardelli, Curien și Lévy. În plus față de operatorii calculului λυ, acest calcul are

Nu există operator ⇑ și nici substituție M / .

Calculul λσ

(Beta)

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

(Aplicație)

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

(Abs)

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

(Închis)

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

(VarId)

0 [Id] → 0

(VarCons)

0 [Ms] → 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)

În timp ce substituțiile lui λυ spun ce să atribuiți indexului 0 și avatarurilor sale atunci când se scufundă în λ și cum să deplaseze indici altele decât 0, substituțiile grupului λσ într-o singură înlocuire atribuțiile la toți indicii și pentru asta acestea includ un operator de compoziție.

Istorie

Ideea substituției explicite este schițată în prefața cărții lui Curry și Feys despre logica combinatorială , dar capătă statutul unui sistem real de rescriere a termenilor în lucrarea desfășurată de Bruijn în legătură cu sistemul Automath . În contrast, conceptul și terminologia sunt de obicei atribuite lui Martín Abadi , Luca Cardelli , Curien și Lévy . Într-un articol care va fi primul dintr-o linie lungă, autorii introduc calculul λσ și arată că calculul lambda trebuie studiat cu multă atenție în ceea ce privește substituția. Fără mecanisme sofisticate de partajare a structurii, substituțiile pot exploda în mărime.

Note și referințe

  1. Delia Kesner: O teorie a substituțiilor explicite cu o compoziție sigură și completă. Metode logice în informatică 5 (3) (2009)
  2. M. Abadi, L. Cardelli, PL. Curien și JJ. Levy, Substituții explicite, Jurnalul de programare funcțională 1, 4 (octombrie 1991), 375-416.
  3. (în) Haskell Curry și Robert Feys , Combinatory Logic Volume I , Amsterdam, North-Holland Publishing Company,1958
  4. NG de Bruijn: Un calcul lambda fără nume cu facilități pentru definirea internă a expresiilor și segmentelor. Universitatea Tehnologică Eindhoven, Olanda, Departamentul de Matematică, (1978), (TH-Report), Numărul 78-WSK-03.

Bibliografie

Vezi și tu