Wyraźne podstawienie

W informatyce mówi się , że rachunki lambda mają jawne podstawienia , jeśli zwraca się szczególną uwagę na sformalizowanie procesu podstawienia . Kontrastuje to ze standardowym rachunkiem lambda , w którym podstawienia są wykonywane przez redukcje beta w sposób niejawny, który nie jest wyrażany w rachunku; warunki „świeżości” w takich niejawnych obliczeniach są notorycznym źródłem błędów. Koncepcja ta pojawiła się w wielu opublikowanych artykułach z zupełnie różnych dziedzin, takich jak maszyny abstrakcyjne , logika predykatów i obliczenia symboliczne .

Przegląd

Prostym przykładem rachunku lambda z wyraźnym podstawieniem jest „λx”, który dodaje jedną nową formę wyrażenia do rachunku lambda , a mianowicie postać M⟨x:=N⟩, która brzmi „M, gdzie x zostanie zastąpione przez N” . (Znaczenie nowego terminu jest takie samo, jak popularny idiom let x:=N w M z wielu języków programowania.) λx można zapisać zgodnie z następującymi regułami przepisywania :

(λx.M) N → M⟨x:=N⟩
x⟨x:=N⟩ → N
x⟨y:=N⟩ → x (x≠y)
(M ₁ M ₂ ) ⟨x:=N⟩ → (M ₁ ⟨x:=N⟩) (M ₂ ⟨x:=N⟩)
(λx.M) ⟨y:=N⟩ → λx.(M⟨y:=N⟩) (x≠y i x nie są wolne w N)

Chociaż podstawienie jest wyraźne, to sformułowanie nadal zachowuje złożoność „konwencji zmiennych” rachunku lambda, wymagającej arbitralnej zmiany nazw zmiennych podczas redukcji, aby zapewnić, że warunek „( x ≠ y i x nie jest wolny w N) ” w ostatniej regule jest zawsze spełnione przed zastosowaniem reguły. Dlatego wiele rachunków jawnego podstawienia całkowicie unika nazw zmiennych, używając tak zwanej „beznazwniczej” indeksu De Bruijna .

Historia

Wyraźne podstawienia zostały naszkicowane we wstępie do książki Curry'ego o logice kombinatorycznej i wyrosły z „sztuczki implementacyjnej” stosowanej na przykład przez AUTOMATH i stały się szanowaną teorią składniową w rachunku lambda i teorii przepisywania . Chociaż w rzeczywistości pochodzi od de Bruijna , pomysł specyficznego rachunku różniczkowego, w którym podstawienia są częścią języka obiektowego, a nie nieformalnej metateorii, jest tradycyjnie przypisywany Abadiemu , Cardelli , Curienowi i Lévy'emu. Ich przełomowy artykuł na temat rachunku λσ wyjaśnia, że implementacje rachunku lambda muszą być bardzo ostrożne, gdy mamy do czynienia z podstawieniami. Bez wyrafinowanych mechanizmów udostępniania struktury podstawienia mogą spowodować eksplozję rozmiarów, dlatego w praktyce podstawienia są opóźniane i jawnie rejestrowane. To sprawia, że zgodność między teorią a implementacją jest wysoce nietrywialna, a poprawność implementacji może być trudna do ustalenia. Jednym z rozwiązań jest uczynienie podstawień częścią rachunku różniczkowego, to znaczy posiadanie rachunku jawnych podstawień.

Jednak gdy podstawienie zostanie wyraźnie określone, podstawowe właściwości podstawienia zmieniają się z właściwości semantycznych na właściwości składniowe. Jednym z najważniejszych przykładów jest „lemat podstawienia”, który przy zapisie λx staje się

(M⟨x:=N⟩)⟨y:=P⟩ = (M⟨y:=P⟩)⟨x:=(N⟨y:=P⟩)⟩ (gdzie x≠y i x nie są wolne w P )

Zaskakujący kontrprzykład, dzięki Mellièsowi, pokazuje, że sposób, w jaki ta reguła jest zakodowana w oryginalnym rachunku jawnych podstawień, nie jest silnie normalizujący . Następnie opisano wiele rachunków, starając się zaoferować najlepszy kompromis między właściwościami składniowymi jawnych rachunków podstawieniowych.

Zobacz też