Programowanie funkcjonalne - rachunek lambda

Rachunek lambda to struktura opracowana przez Alonzo Churcha w latach trzydziestych XX wieku w celu badania obliczeń z funkcjami.

Function creation - Kościół wprowadził notację λx.Edo oznaczenia funkcji, w której „x” jest argumentem formalnym, a „E” jest ciałem funkcjonalnym. Te funkcje mogą być bez nazw i pojedynczych argumentów.
Function application - Kościół użył notacji E₁.E₂ na oznaczenie zastosowania funkcji E₁ do rzeczywistego argumentu E₂. Wszystkie funkcje są na jednym argumencie.

Składnia rachunku Lambda

Rachunek Lamdby obejmuje trzy różne typy wyrażeń, tj.

E :: = x (zmienne)

| E ₁ E ₂(zastosowanie funkcji)

| λx.E (tworzenie funkcji)

Gdzie λx.E nazywa się abstrakcją Lambda, a E jest znane jako wyrażenia λ.

Czysty rachunek lambda nie ma wbudowanych funkcji. Przeanalizujmy następujące wyrażenie -

(+ (* 5 6) (* 8 3))

Tutaj nie możemy zacząć od znaku „+”, ponieważ działa on tylko na liczbach. Istnieją dwa redukowalne wyrażenia: (* 5 6) i (* 8 3).

Najpierw możemy zredukować jeden z nich. Na przykład -

(+ (* 5 6) (* 8 3)) 
(+ 30 (* 8 3)) 
(+ 30 24) 
= 54

Potrzebujemy reguły redukcji, aby obsłużyć λ

(λx . * 2 x) 4 
(* 2 4) 
= 8

Nazywa się to β-redukcją.

Parametr formalny może być używany wielokrotnie -

(λx . + x x) 4 
(+ 4 4) 
= 8

W przypadku wielu terminów możemy obsługiwać je w następujący sposób -

(λx . (λx . + (− x 1)) x 3) 9

Wewnętrzny x należy do wewnętrznego λ a zewnętrzne x należy do zewnętrznego.

(λx . + (− x 1)) 9 3 
+ (− 9 1) 3 
+ 8 3 
= 11

W wyrażeniu każde pojawienie się zmiennej jest „wolne” (do λ) lub „związane” (do λ).

β-redukcja (λx . E) y zastępuje każdy x który występuje za darmo w E z y. Na przykład -

Redukcja alfa jest bardzo prosta i można ją przeprowadzić bez zmiany znaczenia wyrażenia lambda.

λx . (λx . x) (+ 1 x) ↔ α λx . (λy . y) (+ 1 x)

Na przykład -

(λx . (λx . + (− x 1)) x 3) 9 
(λx . (λy . + (− y 1)) x 3) 9 
(λy . + (− y 1)) 9 3 
+ (− 9 1) 3 
+ 8 3 
11

Twierdzenie Churcha-Rossera stwierdza, co następuje -

Jeśli E1 ↔ E2, to istnieje E takie, że E1 → E i E2 → E. „Redukcja w jakikolwiek sposób może ostatecznie przynieść ten sam wynik”.
Jeśli E1 → E2 i E2 jest postacią normalną, to istnieje redukcja E1 do E2 w porządku normalnym. „Redukcja porządku normalnego zawsze da normalną formę, jeśli taka istnieje”.