Maszyna Krivine'a

Widok obrazu maszyny Krivine

W informatyce teoretycznej maszyna Krivine'a jest maszyną abstrakcyjną (czasami nazywaną maszyną wirtualną ). Jako maszyna abstrakcyjna ma wspólne cechy z maszynami Turinga i maszyną SECD . Maszyna Krivine wyjaśnia, jak obliczyć funkcję rekurencyjną. Dokładniej, ma na celu rygorystyczne zdefiniowanie redukcji postaci normalnej głowy wyrażenia lambda przy użyciu wywołania według nazwy zmniejszenie. Dzięki swojemu formalizmowi szczegółowo opowiada, jak działa swego rodzaju redukcja i wyznacza teoretyczne podstawy semantyki operacyjnej funkcyjnych języków programowania . Z drugiej strony maszyna Krivine'a implementuje wywołanie według nazwy, ponieważ ocenia treść β- redexu , zanim zastosuje treść do swojego parametru. Innymi słowy, w wyrażeniu ( λ x . t ) u oblicza najpierw λ x . t przed zastosowaniem go do u . W programowaniu funkcjonalnym oznaczałoby to, że aby ocenić funkcję zastosowaną do parametru, najpierw ocenia funkcję przed zastosowaniem jej do parametru.

Maszyna Krivine'a została zaprojektowana przez francuskiego logika Jeana-Louisa Krivine'a na początku lat 80-tych.

Zadzwoń po imieniu i kieruj redukcją postaci normalnej

Maszyna Krivine opiera się na dwóch koncepcjach związanych z rachunkiem lambda , a mianowicie redukcji głowy i wywołaniu po imieniu.

Redukcja normalnej postaci głowy

Redex (mówi się też β-redex) jest wyrazem rachunku lambda postaci ( λ x . t ) u . Jeśli termin ma kształt ( λ x . t ) u ₁ ... u _n, mówi się, że jest to redeks głowy . Postać normalna głowy to termin rachunku lambda, który nie jest redeksem głowy. Redukcja głowy to (niepusta) sekwencja skróceń wyrazu, która zawiera zwroty głowy. Redukcja głowy kadencji t (które nie powinno być w postaci normalnej głowy) jest redukcją głowy, która zaczyna się od wyrazu t i kończy się w postaci normalnej głowy. Z abstrakcyjnego punktu widzenia redukcja głowy to sposób, w jaki program oblicza, gdy ocenia podprogram rekurencyjny. Ważne jest, aby zrozumieć, w jaki sposób można wdrożyć taką redukcję. Jednym z celów maszyny Krivine'a jest zaproponowanie procesu redukcji wyrazu do postaci normalnej głowy i formalne opisanie tego procesu. Podobnie jak Turing użył abstrakcyjnej maszyny do formalnego opisania pojęcia algorytmu, Krivine użył abstrakcyjnej maszyny do formalnego opisania pojęcia redukcji postaci normalnej głowy.

Przykład

Wyraz (( λ 0) ( λ 0)) ( λ 0) (który odpowiada, jeśli używamy zmiennych jawnych, terminowi ( λx . x ) ( λy . y ) ( λ z . z )) nie jest w głowie normalnej forma ponieważ ( λ 0) ( λ 0) kurczy się w ( λ 0) otrzymując redeks głowy ( λ 0) ( λ 0), która kurczy się w ( λ 0) i która jest zatem normalną postacią głowy (( λ 0) ( λ 0)) ( λ 0). Inaczej mówiąc, normalny skurcz głowy to:

(( λ 0) ( λ 0)) ( λ 0) ➝ ( λ 0) ( λ 0) ➝ λ 0,

co odpowiada:

( λx . x ) ( λ y . y ) ( λ z . z ) ➝ ( λ y . y ) ( λ z . z ) ➝ λ z . z .

Zobaczymy dalej, jak maszyna Krivine'a redukuje wyraz (( λ 0) ( λ 0)) ( λ 0).

Zadzwoń po imieniu

Aby zaimplementować redukcję głowy terminu uv , który jest aplikacją, ale która nie jest redeksem, należy zredukować ciało u , aby wykazywało abstrakcję, a zatem utworzyć redeks z v . Kiedy pojawia się redex, zmniejsza się go. Aby zredukować zawsze najpierw treść aplikacji, nazywa się call by name . Maszyna Krivine implementuje wywołanie według nazwy .

Opis

Podana tutaj prezentacja maszyny Krivine'a oparta jest na zapisach wyrażeń lambda wykorzystujących indeksy de Bruijna i zakłada, że wyrazy, z których oblicza ona główne formy normalne, są domknięte . Modyfikuje obecny stan dopóki nie może już tego robić, w którym to przypadku uzyskuje normalną postać głowy. Ta główna postać normalna reprezentuje wynik obliczeń lub daje błąd, co oznacza, że termin, od którego się zaczęła, jest nieprawidłowy. Może jednak wejść w nieskończoną sekwencję przejść, co oznacza, że wyraz, który próbuje zredukować, nie ma postaci normalnej głowy i odpowiada niekończącemu się obliczeniu.

Udowodniono, że maszyna Krivine'a poprawnie realizuje redukcję postaci normalnej głowy wywołanej po imieniu w rachunku lambda. Co więcej, maszyna Krivine'a jest deterministyczna , ponieważ każdy wzorzec stanu odpowiada co najwyżej jednemu przejściu maszyny.

Stan

Państwo składa się z trzech elementów

termin , _
stos , _
środowisko . _

Termin jest terminem λ z indeksami de Bruijna. Stos i środowisko należą do tej samej rekurencyjnej struktury danych. Mówiąc dokładniej, środowisko i stos to listy par <term, environment> , które są nazywane domknięciami . Poniżej wstawienie jako nagłówek listy ℓ (stos lub środowisko) elementu a jest zapisywane jako: ℓ 0 , podczas gdy pusta lista jest zapisana □. Stos to miejsce, w którym maszyna przechowuje zamknięcia, które muszą być dalej oceniane, podczas gdy środowisko to powiązanie między indeksami a zamknięciami w danym momencie podczas oceny. Pierwszym elementem środowiska jest domknięcie związane z indeksem , drugim elementem jest domknięcie związane z indeksem 1 itd. Jeśli maszyna ma ocenić indeks, pobiera tam parę <termin, środowisko> zamknięcie, które daje termin do oceny, oraz środowisko, w którym ten termin musi zostać oceniony. Te intuicyjne objaśnienia pozwalają zrozumieć zasady działania maszyny. Jeśli zapiszemy t dla terminu, p dla stosu i e dla środowiska, stany związane z tymi trzema bytami zostaną zapisane jako t , p, e. Reguły wyjaśniają, w jaki sposób maszyna przekształca stan w inny stan po zidentyfikowaniu wzorców między stanami.

Stan początkowy ma na celu oszacowanie terminu t , jest to stan t ,□,□, w którym termin wynosi t , a stos i środowisko są puste. Stan końcowy (przy braku błędu) ma postać λ t , □, e, innymi słowy, otrzymane wyrazy są abstrakcją wraz z otoczeniem i pustym stosem.

Przejścia

Maszyna Krivine ma cztery przejścia: App , Abs , Zero , Succ .

Przejścia maszyny Krivine'a
Nazwa	Zanim	Po
Aplikacja	tu , p, e	t , < u ,e>:p, mi
Abs	λ t , < u ,e'>:p, mi	t , p, < u ,e'>:e
Zero	0 , p, < t , e'>:e	t , p, e'
Succ	n+1 , p, < t ,e'>:e	n, p, e

0 Aplikacja przejściowa usuwa parametr aplikacji i umieszcza go na stosie w celu dalszej oceny. Przejście Abs usuwa λ terminu i podnosi zamknięcie ze szczytu stosu i umieszcza je na wierzchu środowiska. To zamknięcie odpowiada indeksowi de Bruijna w nowym środowisku. Przejście Zero obejmuje pierwsze zamknięcie środowiska. Termin tego zamknięcia staje się bieżącym terminem, a środowisko tego zamknięcia staje się bieżącym środowiskiem. Przejście Succ usuwa pierwsze zamknięcie listy środowisk i zmniejsza wartość indeksu.

Dwa przykłady

Oceńmy wyraz ( λ 0 0) ( λ 0), który odpowiada wyrazowi ( λ x . x x ) ( λ x . x ). Zacznijmy od stanu ( λ 0 0) ( λ 0), □, □.

Ocena składnika *(λ 0 0) (λ 0)*
( λ 0 0) ( λ 0), □, □
λ 0 0, [< λ 0, □>], □
0 0, □, [< λ 0, □>]
0, [<0, < λ 0, □>>], [< λ 0, □>]
λ 0, [<0, < λ 0, □>>], □
0, □, [<0 , < λ 0, □>>]
0, □, [< λ 0, □>]
λ 0, □, □

Wniosek jest taki, że główna postać normalna wyrażenia ( λ 0 0) ( λ 0) to λ 0. To przekłada się na zmienne w: głównej postaci normalnej wyrażenia ( λ x . x x ) ( λ x . x ) jest λ x . x .

Oceńmy wyraz (( λ 0) ( λ 0)) ( λ 0) jak pokazano poniżej:

Ocena ((λ 0) (λ 0)) (λ 0)
(( λ 0) ( λ 0)) ( λ 0), □, □
( λ 0) ( λ 0), [<( λ 0), □>], □
( λ 0), [<( λ 0), □>, <( λ 0), □>], □
0, [<( λ 0), □>], [<( λ 0) , □>]
λ 0, [<( λ 0), □>], □
0, □, [<( λ 0), □>]
( λ 0), □, □

Potwierdza to powyższy fakt, że postać normalna wyrazu (( λ 0) ( λ 0)) ( λ 0) to ( λ 0).

Zobacz też

Notatki

Treść tej edycji została przetłumaczona z istniejącego artykułu francuskiej Wikipedii pod adresem fr:Machine de Krivine ; zobacz jego historię do przypisania.

Bibliografia

Jean-Louis Krivine: Maszyna do rachunku lambda, nazywana po imieniu . Obliczenia wyższego rzędu i symboliczne 20 (3): 199-207 (2007) archiwum .
Curien, Pierre-Louis (1993). Kombinatory kategoryczne, algorytmy sekwencyjne i funkcjonalne (wyd. 2). Birkhauser.
Frédéric Lang: Wyjaśnienie leniwej maszyny Krivine przy użyciu jawnych podstawień i adresów . Obliczenia wyższego rzędu i symboliczne 20 (3): 257-270 (2007) archiwum .
Olivier Danvy (red.): Redakcja wydania specjalnego Higher-Order and Symbolic Computation on the Krivine machine, tom. 20(3) (2007)

Linki zewnętrzne

Media związane z maszyną Krivine w Wikimedia Commons