Rachunek Lambda to formalny system logiki matematycznej do wyrażania obliczeń opartych na abstrakcji i stosowania funkcji przy użyciu wiązania i podstawienia zmiennych. Jest to uniwersalny model, który można zastosować do konstrukcji dowolnej maszyny Turinga. Rachunek lambda został po raz pierwszy wprowadzony przez Churcha, słynnego matematyka, w latach 30. XX wieku.
System polega na budowaniu elementów lambda i wykonywaniu na nich operacji redukcji.
Wyjaśnienia i zastosowania
Grecka litera lambda (λ) jest używana w wyrażeniach lambda i terminach lambda do oznaczenia powiązania zmiennej w funkcji.
Rachunek Lambda może być bez typu lub wpisany. W pierwszym wariancie z funkcji można korzystać tylko wtedy, gdy są w stanie odbierać dane tego typu. Typowane rachunki lambda są słabsze, mogą wyrażać mniejszą wartość. Ale z drugiej strony pozwalają udowodnić więcej rzeczy.
Jednym z powodów, dla których istnieje tak wiele różnych typów, jest chęć naukowców, aby robić więcej, nie rezygnując z możliwości udowodnienia silnych twierdzeń rachunku lambda.
System ma zastosowanie w wielu różnych dziedzinach matematyki, filozofii, językoznawstwa i informatyki. Przede wszystkim rachunek lambda jest rachunkiem, który odegrał ważną rolę w rozwoju teorii języków programowania. To style tworzenia funkcjonalnego, które wdrażają systemy. Są również gorącym tematem badań w teorii tych kategorii.
Dla manekinów
Rachunek lambda został wprowadzony przez matematyka Alonzo Churcha w latach 30. XX wieku jako część jego badań nad podstawami nauki. Oryginalny system okazał się logicznie niespójny w 1935 roku, kiedy Stephen Kleen i J. B. Rosser opracowali paradoks Kleene-Rosser.
Później, w 1936 roku, Church wyróżnił i opublikował tylko tę część, która ma znaczenie dla obliczeń, co obecnie nazywa się nieopisanym rachunkiem lambda. W 1940 wprowadził również słabszą, ale logicznie spójną teorię znaną jako system typów pierwszych. W swojej pracy wyjaśnia całą teorię w prostych słowach, można więc powiedzieć, że Church opublikował rachunek lambda dla manekinów.
Do lat 60., kiedy jego związek z językami programowania stał się jasny, λ był tylko formalizmem. Dzięki zastosowaniom Richarda Montagu i innych lingwistów w semantyce języka naturalnego rachunek różniczkowy zajmuje poczesne miejsce zarówno w lingwistyce, jak i informatyce.
Pochodzenie symbolu
Lambda nie oznacza słowa ani akronimu, pochodzi z odniesienia w Principal Mathematics Russella, po którym następują dwie zmiany typograficzne. Przykład zapisu: dla funkcji f z f (y)=2y + 1 to 2ŷ + 1. A tutaj używamy karetki („kapelusz”) nad y, aby oznaczyć zmienną wejściową.
Kościół pierwotnie zamierzał używać podobnych symboli, ale zecer nie był w stanie umieścić symbolu „kapelusza” nad literami. Więc zamiast tego wydrukowali go pierwotnie jako "/\y.2y+1". W kolejnym odcinku montażu maszynistki zastąpiły "/\" podobnym wizualnie znakiem.
Wprowadzenie do rachunku lambda
System składa się z języka terminów, które są wybierane przez określoną składnię formalną oraz zestawu reguł transformacji, które pozwalają na manipulowanie nimi. Ostatni punkt można uznać za teorię równań lub jako definicję operacyjną.
Wszystkie funkcje w rachunku lambda są anonimowe, co oznacza, że nie mają nazw. Przyjmują tylko jedną zmienną wejściową, a currying służy do implementacji wykresów z wieloma zmiennymi.
Warunki Lambda
Składnia rachunku różniczkowego definiuje niektóre wyrażenia jako prawidłowe, a inne jako nieprawidłowe. Tak jak różne ciągi znaków są poprawnymi programami w C, a niektóre nie. Rzeczywiste wyrażenie rachunku lambda nazywa się „terminem lambda”.
Poniższe trzy zasady zapewniają indukcyjną definicję, którą możnastosuje się do konstrukcji wszystkich pojęć poprawnych składniowo:
Sama zmienna x jest prawidłowym wyrażeniem lambda:
- jeśli T jest LT, a x jest niestałe, wtedy (lambda xt) nazywa się abstrakcją.
- jeśli T i s są pojęciami, wtedy (TS) nazywa się aplikacją.
Nic innego nie jest terminem lambda. Zatem pojęcie jest ważne wtedy i tylko wtedy, gdy można je uzyskać poprzez wielokrotne stosowanie tych trzech reguł. Jednak niektóre nawiasy mogą zostać pominięte zgodnie z innymi kryteriami.
Definicja
Wyrażenia Lambda składają się z:
- zmienne v 1, v 2, …, v n, …
- symbole abstrakcji 'λ' i kropka '.'
- nawiasy ().
Zestaw Λ można zdefiniować indukcyjnie:
- Jeśli x jest zmienną, to x ∈ Λ;
- x nie jest stała i M ∈ Λ, wtedy (λx. M) ∈ Λ;
- M, N ∈ Λ, następnie (MN) ∈ Λ.
Oznaczenie
Aby zachować porządek w zapisie wyrażeń lambda, powszechnie stosuje się następujące konwencje:
- Pominięto nawiasy zewnętrzne: MN zamiast (MN).
- Zakłada się, że aplikacje pozostają asocjacyjne: można zapisać MNP zamiast ((MN) P).
- Ciało abstrakcji rozciąga się dalej w prawo: λx. MN oznacza λx. (MN), nie (λx. M) N.
- Sekwencja abstrakcji jest zmniejszona: λx.λy.λz. N może być λxyz. N.
Wolne i powiązane zmienne
Operator λ łączy swoją niestałą gdziekolwiek się znajduje w ciele abstrakcji. Zmienne, które wchodzą w zakres, są nazywane powiązanymi. W wyrażeniu λ x. M, część λx jest często określana jako spoiwo. Jakby sugerować, że zmienne stają się grupą z dodaniem X x do M. Wszystkie inne niestabilne są nazywane wolnymi.
Na przykład w wyrażeniu λ y. x x y, y - związany nietrwały, a x - wolny. Warto też zauważyć, że zmienna jest pogrupowana według swojej „najbliższej” abstrakcji. W poniższym przykładzie rozwiązanie rachunku lambda jest reprezentowane przez pojedyncze wystąpienie x, które jest powiązane z drugim wyrazem:
λ x. y (λ x. z x)
Zbiór wolnych zmiennych M jest oznaczony jako FV (M) i jest definiowany przez rekursję w strukturze terminów w następujący sposób:
- FV (x)={x}, gdzie x jest zmienną.
- FV (λx. M)=FV (M) {x}.
- FV (MN)=FV (M) ∪ FV (N).
Formuła, która nie zawiera wolnych zmiennych, nazywana jest zamkniętą. Zamknięte wyrażenia lambda są również znane jako kombinatory i są równoważne terminom w logice kombinatorycznej.
Skrót
Znaczenie wyrażeń lambda zależy od tego, jak można je skrócić.
Istnieją trzy rodzaje cięć:
- α-transform: zmiana powiązanych zmiennych (alfa).
- β-redukcja: stosowanie funkcji do ich argumentów (beta).
- η-transform: obejmuje pojęcie ekstensjonalności.
Tu też jestmówimy o powstałych równoważnościach: dwa wyrażenia są β-równoważne, jeśli można je przekształcić w ten sam składnik β, a równoważność α / η definiuje się podobnie.
Termin redex, skrót od redukowalnego obrotu, odnosi się do podtematów, które można ograniczyć za pomocą jednej z reguł. Rachunek lambda dla manekinów, przykłady:
(λ x. M) N jest redeksem beta w wyrażeniu zastępującym N przez x w M. Składnik, do którego redeks się redukuje, nazywa się jego redukcją. Redukcja (λ x. M) N to M [x:=N].
Jeśli x nie jest wolne w M, λ x. M x również em-REDEX z regulatorem M.
α-transformacja
Zmiany nazw alfa umożliwiają zmianę nazw powiązanych zmiennych. Na przykład x. x może dać λ y. tak. Mówi się, że terminy różniące się tylko transformacją alfa są równoważnikami α. Często podczas korzystania z rachunku lambda równoważniki α są uważane za wzajemne.
Dokładne zasady konwersji alfa nie są całkowicie trywialne. Po pierwsze, dzięki tej abstrakcji zmieniane są nazwy tylko tych zmiennych, które są powiązane z tym samym systemem. Na przykład transformata alfa λ x.λ x. x może prowadzić do λ y.λ x. x, ale to nie może prowadzić do λy.λx.y Ten ostatni ma inne znaczenie niż oryginał. Jest to analogiczne do koncepcji programowania cieniowania zmiennych.
Po drugie, transformacja alfa nie jest możliwa, jeśli spowodowałaby przechwycenie przez nietrwałą inną abstrakcję. Na przykład, jeśli zamienisz x na y w λ x.λ y. x, wtedy możesz dostaćλy.λy. u, co wcale nie jest takie samo.
W językach programowania o zakresie statycznym konwersja alfa może być używana do uproszczenia rozpoznawania nazw. Jednocześnie uważając, aby pojęcie zmiennej nie maskowało oznaczenia w obszarze zawierającym.
W notacji indeksu De Bruyne, dowolne dwa terminy w alfabecie równoważnym są identyczne składniowo.
Wymiana
Zmiany zapisane przez E [V:=R] są procesem podstawienia wszystkich wolnych wystąpień zmiennej V w wyrażeniu E przez obrót R. Podstawienie ze względu na λ jest zdefiniowane przez lambda rekurencji rachunek struktury pojęć w następujący sposób (uwaga: x i y - tylko zmienne, a M i N - dowolne wyrażenie λ).
x [x:=N] ≡ N
y [x:=N] ≡ y, jeśli x ≠ y
(M 1 M 2) [x:=N] ≡ (M 1 [x:=N]) (M 2 [x:=N])
(λ x. M) [x:=N] ≡ λ x. M
(λ y. M) [x:=N] y λ y. (M [x:=N]) jeśli x y, pod warunkiem, że y ∉ FV (N).
W celu podstawienia do abstrakcji lambda, czasami konieczne jest przekształcenie wyrażenia α. Na przykład nie jest prawdą, że (λ x. Y) [y:=x] daje w wyniku (λ x. X), ponieważ podstawione x powinno być wolne, ale ostatecznie zostało powiązane. Prawidłowe zastąpienie w tym przypadku to (λ z. X) aż do równoważności α. Zauważ, że podstawienie jest jednoznacznie zdefiniowane aż do lambda.
β-redukcja
Redukcja Beta odzwierciedla ideę zastosowania funkcji. Beta-redukcyjna jest zdefiniowana w terminachpodstawienie: ((X V. E) E ') to E [V:=E'].
Na przykład, zakładając, że kodowanie 2, 7, ×, jest następująca β-redukcja: ((λ n. N × 2) 7) → 7 × 2.
Redukcja beta może być postrzegana jako taka sama jak koncepcja lokalnej redukowalności w ramach naturalnej dedukcji za pomocą izomorfizmu Curry-Howarda.
η-transformacja
Ta konwersja wyraża ideę rozszerzalności, która w tym kontekście polega na tym, że dwie funkcje są równe, gdy dają ten sam wynik dla wszystkich argumentów. Ta konwersja zamienia się między λ x. (F x) i f zawsze, gdy x nie wydaje się wolne w f.
To działanie można uznać za tożsame z koncepcją lokalnej zupełności w naturalnej dedukcji poprzez izomorfizm Curry-Howarda.
Formy normalne i fuzja
W przypadku rachunku lambda bez określonego typu, reguła β-redukcji generalnie nie jest ani silna, ani słaba normalizująca.
Niemniej jednak można wykazać, że β-redukcja łączy się podczas wykonywania przed transformacją α (tj. dwie normalne formy można uznać za równe, jeśli możliwa jest transformacja α z jednej w drugą).
Dlatego zarówno warunki silnie normalizujące, jak i słabo dostosowujące się mają jedną normalną postać. W przypadku pierwszych warunków każda strategia redukcji gwarantuje typową konfigurację. Podczas gdy w przypadku słabo normalizujących się warunków, niektóre strategie redukcji mogą tego nie znaleźć.
Dodatkowe metody programowania
Istnieje wiele idiomów tworzenia dla rachunku lambda. Wiele z nich zostało pierwotnie opracowanych w kontekście wykorzystania systemów jako podstawy semantyki języka programowania, skutecznie stosując je jako konstrukcje niskopoziomowe. Ponieważ w niektórych stylach jako fragment kodu stosuje się rachunek lambda (lub coś bardzo podobnego), techniki te znajdują również zastosowanie w praktycznym tworzeniu, ale mogą być wówczas postrzegane jako niejasne lub obce.
Nazwane stałe
W rachunku lambda biblioteka przyjmuje postać zestawu wcześniej zdefiniowanych funkcji, w których terminy są po prostu konkretnymi stałymi. Czysty rachunek różniczkowy nie ma pojęcia o nazwanych niezmiennych, ponieważ wszystkie atomowe terminy lambda są zmiennymi. Ale można je również naśladować, przyjmując mutable jako nazwę stałej, używając abstrakcji lambda do powiązania tego elementu niestabilnego w ciele i stosując tę abstrakcję do zamierzonej definicji. Więc jeśli użyjesz f do przedstawienia M w N, możesz powiedzieć
(λ f. N) M.
Autorzy często wprowadzają koncepcję składni, taką jak let, aby umożliwić pisanie w bardziej intuicyjny sposób.
f=M do N
Dzięki łączeniu takich definicji można napisać "program" rachunku lambda jako zero lub więcej definicji funkcji, po których następuje pojedynczy element lambda, używając tych definicji, które stanowią większość programu.
Ważnym ograniczeniem tego niech jest to, że nazwa f nie jest zdefiniowana w M,ponieważ M jest poza wiążącym zakresem abstrakcji lambda f. Oznacza to, że atrybut funkcji rekurencyjnej nie może być użyty jako M z let. Bardziej zaawansowana składnia letrec, która umożliwia pisanie definicji funkcji rekurencyjnych w tym stylu, dodatkowo wykorzystuje zamiast tego kombinatory stałoprzecinkowe.
Drukowane analogi
Ten typ to typizowany formalizm, który używa symbolu do reprezentowania anonimowej abstrakcji funkcji. W tym kontekście typy są zwykle obiektami o charakterze składniowym, które są przypisywane terminom lambda. Dokładna natura zależy od rachunku różniczkowego. Z pewnego punktu widzenia wpisane LI mogą być traktowane jako udoskonalenia niewpisane LI. Ale z drugiej strony można je również uznać za bardziej fundamentalną teorię, a beztypowy rachunek lambda jest przypadkiem szczególnym z tylko jednym typem.
Wpisane LI są podstawą języków programowania i podstawą języków funkcjonalnych, takich jak ML i Haskell. I, bardziej pośrednio, imperatywne style tworzenia. Typowane rachunki lambda odgrywają ważną rolę w rozwoju systemów typów dla języków programowania. Tutaj typowalność zazwyczaj przechwytuje pożądane właściwości programu, na przykład nie spowoduje naruszenia dostępu do pamięci.
Rachunki lambda typowane są ściśle związane z logiką matematyczną i teorią dowodu poprzez izomorfizm Curry-Howarda i mogą być traktowane jako na przykład wewnętrzny język klas kategorii, któryto po prostu styl zamknięć kartezjańskich.
