Rachunek lambda: opis twierdzenia, cechy, przykłady

Lambda-calculus jest formalnym systemem w logice matematycznej do wyrażania obliczeń opartych na abstrakcji i stosowaniu funkcji przy użyciu zmiennych wiążących i zastępczych. Jest to uniwersalny model, który można zastosować do projektowania dowolnej maszyny Turinga. Po raz pierwszy wprowadzone przez Churcha, słynnego matematyka, w latach 30.

System polega na konstruowaniu wyrażeń 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 wiązania zmiennej w funkcji.

Rachunek lambda może być nie przypisany lub wpisany. W pierwszej wersji funkcje mogą być stosowane tylko wtedy, gdy są w stanie przyjąć dane tego typu. Typowany lambda-calculus jest słabszy, może wyrazić mniejszą wartość. Ale z drugiej strony, pozwalają one udowodnić więcej rzeczy.

Jednym z powodów, dla których istnieje tak wiele różnych typów, jest to, że naukowcy chcą zrobić więcej, nie rezygnując z możliwości udowodnienia silnych twierdzeń rachunku lambda.

Ma ona zastosowanie w wielu różnych dziedzinach matematyki, filozofii, lingwistyki i informatyki. Przede wszystkim lambda-calculus jest rachunkiem, który odegrał ważną rolę w rozwoju teorii języków programowania. To właśnie style kreacji funkcjonalnej realizują systemy. Są one również gorącym tematem badawczym w teorii tych kategorii.

For Dummies

Lambda-calculus został wprowadzony przez matematyka Alonzo Churcha w latach 30. XX wieku w ramach badań nad podstawami nauki. Oryginalny system został pokazany jako logicznie niezgodny w 1935 roku, kiedy Stephen Kline i J. Б. Rosser opracował paradoks Kline-Rossera.

Później, w 1936 roku, Church wyodrębnił i opublikował tylko część związaną z obliczeniami, co obecnie nazywa się nieopisanym lambda-calculusem. W 1940 roku wprowadził również słabszą, ale logicznie spójną teorię, znaną jako system typów prostych. W swojej pracy wyjaśnia całą teorię w prostym języku, więc można powiedzieć, że Church opublikował lambda calculus for dummies.

Do lat 60. XX wieku, kiedy to wyjaśnił się jej związek z językami programowania, λ była tylko formalizmem. Dzięki zastosowaniom Richarda Montague`a i innych lingwistów do semantyki języka naturalnego, rachunek zyskał honorowe miejsce zarówno w lingwistyce, jak i informatyce.

Pochodzenie symbolu

Lambda nie oznacza słowa ani skrótu, powstała dzięki wzmiance w Zasadach matematyki Russella, po której nastąpiły dwie zmiany typograficzne. Przykładowa notacja: dla funkcji f z f (y) = 2y + 1 jest 2ŷ + 1. Również tutaj symbol karetki ("hat") jest używany nad y do oznaczenia zmiennej wejściowej.

Kościół pierwotnie zamierzał użyć podobnych symboli, ale zecerzy nie mogli umieścić symbolu "kapelusza" nad literami. Więc zamiast tego wpisali to oryginalnie jako "/.2y+1". W kolejnym odcinku edycji, zecerzy zastąpili "/" wizualnie podobnym symbolem.

Wprowadzenie do rachunku lambda

System składa się z języka pojęć, które są wybierane przez określoną składnię formalną, oraz zbioru reguł transformacji, które pozwalają na manipulowanie nimi. O ostatnim punkcie można myśleć jako o teorii równania lub jako o definicji operacyjnej.

Wszystkie funkcje w lambda-calculus są anonimowe, tzn. nie mają nazw. Akceptują one tylko jedną zmienną wejściową, a currying jest używany do implementacji wykresów z kilkoma niezmiennikami.

Terminy lambda

Składnia rachunku definiuje pewne wyrażenia jako ważne, a inne jako nieważne. Tak jak różne ciągi znaków są poprawnymi programami C, a niektóre nie są. Poprawne wyrażenie lambda-calculus nazywa się "lambda-terminus".

Poniższe trzy reguły dostarczają indukcyjnej definicji, którą można zastosować do skonstruowania wszystkich syntaktycznie dopuszczalnych pojęć:

Sama zmienna x jest poprawnym wyrażeniem lambda:

• jeśli T jest LT, a x jest niestałe, to (lambda xt) nazywamy abstrakcją.
• jeżeli T oraz s są pojęciami, to (TS) jest nazywane zastosowaniem.

Nic innego nie jest wyrażeniem lambda. Zatem pojęcie jest ważne wtedy i tylko wtedy, gdy można je uzyskać poprzez ponowne zastosowanie tych trzech zasad. Jednakże niektóre nawiasy mogą być pominięte według innych kryteriów.

Definicja

Wyrażenia lambda składają się z:

• zmienne v 1, v 2,..., v n,...
• symbole abstrakcji "λ" i kropka.`
• nawiasy ().

Zbiór Λ, może być zdefiniowany indukcyjnie:

• Jeśli x jest zmienną, to x ∈ Λ;
• x jest niestałe i M ∈ Λ, to (λx.M) ∈ Λ;
• M, N ∈ Λ, to (MN) ∈ Λ.

Oznaczając

W celu zachowania przejrzystości notacji wyrażeń lambda stosuje się zwykle następujące konwencje:

• Pominięto nawiasy zewnętrzne: MN zamiast (MN).
• Zakłada się, że zastosowania pozostają asocjacyjne: zamiast ((MN) P) można napisać MNP.
• Ciało abstrakcji rozciąga się dalej w prawo: λx.MN oznacza, że λx. (MN) zamiast (λx.M) N.
• Redukuje sekwencję abstrakcji: λx.λy .λz.N może λxyz.N.

Zmienne wolne i związane

Operator λ przyłącza swoją niestałą wszędzie tam, gdzie znajduje się ona w ciele abstrakcji. Zmienne należące do dziedziny nazywane są związanymi. W wyrażeniu λ x. M, część λ x jest często nazywana granicą. Jakby dla podpowiedzi, że zmienne stają się grupą po dodaniu x do M. Wszystkie inne niestabilne nazywane są wolnymi.

Na przykład w wyrażeniu λ y. x x y, y jest związaną niestałą, a x jest wolne. I warto też zwracać uwagę, Że zmienna jest pogrupowana według "najbliższej" abstrakcji. W poniższym przykładzie rozwiązanie lambda-calculus jest reprezentowane przez pojedyncze wystąpienie x, które jest związane przez drugi element:

λ x. y (λ x. z x)

Zbiór zmiennych wolnych M oznaczamy jako FV (M) i definiujemy przez rekurencję na 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łę, która nie zawiera zmiennych wolnych nazywamy zamkniętą. Zamknięte wyrażenia lambda są również znane jako kombinatory i są równoważnymi terminami w logice kombinatorycznej.

Redukcja

Znaczenie wyrażeń lambda jest określone przez to, jak można je zredukować.

Istnieją trzy rodzaje przycięć:

• Transformacja α: zmiana w zmiennych związanych (alfa).
• β-redukcja: zastosowanie funkcji do ich argumentów (beta).
• η-transformacja: obejmuje pojęcie ekstensjonalizmu.

Mówimy tu także o równoważnościach uzyskanych: dwa wyrażenia są β-równoważne, jeśli można je β-transformować na ten sam składnik, a α / η-równoważność definiuje się podobnie.

Termin redex, skrótowy dla danego zwrotu, odnosi się do podtematów, które można zredukować za pomocą jednej z zasad. Lambda calculus for dummies, przykłady:

(λ x.M) N to beta-redex w wyrażeniu zastępującym N przez x w M. Składnik, do którego redukuje się reda, nazywa się jego reduktem. Redukcja (λ x.M) N to M [x: = N].

Jeśli x nie jest wolny w M, λ x. M x jest również λ-REDEX z regulatorem M.

Transformacja α

Zmiana nazw alfabetu pozwala na zmianę nazw powiązanych zmiennych. Na przykład λ x. x może dać λ y. у. Terminy, które różnią się tylko poprzez konwersję alfa, nazywane są α-równoważnymi. Często, gdy używamy lambda-calculus, odpowiednik α jest uważany za wzajemny.

Exact zasady dla przekształcenia alfa nie są dokładnie trywialne. Po pierwsze, w tej abstrakcji zmienia się nazwy tylko tych zmiennych, które dotyczą tego samego systemu. Na przykład, konwersja alfa λ x.λ x. x może prowadzić do λ y.λ x. x, ale może to nie skutkować λy.λx.y Ten ostatni ma inne znaczenie niż oryginał. Jest to analogiczne do pojęcia programowania zmiennego cieniowania.

Po drugie, transformacja alfa jest niemożliwa, jeśli prowadzi do zawłaszczenia przez nietrwałą inną abstrakcję. Na przykład, jeśli zastąpimy x przez y w λ x.λ y. x, można uzyskać λ y.λ y. y, co wcale nie jest równoznaczne.

W językach programowania z zakresem statycznym transformacja alfa może być użyta do uproszczenia rozdzielczości nazw. Robiąc to, upewnij się, że pojęcie zmiennej nie ukrywa notacji w domenie zawierającej.

W notacji wskaźnikowej De Bruijna dowolne dwa równoważne alfa terminy są identyczne pod względem składniowym.

Zastępując

Zmiana pisana E [V: = R] to proces zastępowania wszystkich wolnych wystąpień zmiennej V w wyrażeniu E zwrotem R. Substytucja w zakresie λ jest określona przez lambdę rachunku rekurencyjnego na strukturze pojęć w następujący sposób (uwaga: x i y są tylko zmiennymi, a M i N są dowolnymi wyrażeniami λ).

x [x: = N] ≡ N

y [x: = N] ≡ y if 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żeli x ≠ y, pod warunkiem że y ∉ FV (N).

Aby zastąpić abstrakcję lambda, czasami konieczne jest α-transformowanie wyrażenia. Na przykład nie jest prawdą, że (λ x. Y) [y: = x] prowadziło do (λ x. X), ponieważ podstawiony x powinien być wolny, ale skończył jako związany. Prawidłowe podstawienie w tym przypadku to (λ z. X) w ramach α-równoważności. Warto zauważyć, że substytucja jest jednoznacznie zdefiniowana z wiernością lambda.

β-redukcja

Redukcja beta odzwierciedla ideę zastosowania funkcji. Redukcja beta jest zdefiniowana w kategoriach substytucji: ((X V. E) E `) jest E [V: = E`].

Na przykład, zakładając pewne kodowanie 2, 7, ×, istnieje następująca β-redukcja: ((λ n. N × 2) 7) → 7 × 2.

Beta-redukcja może być postrzegana jako to samo, co pojęcie lokalnej redukowalności w dedukcji naturalnej poprzez izomorfizm Curry-Howarda.

Konwersja η to

Konwersja ta wyraża ideę ekstensjonalizmu, 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 zamiana wymienia między λ x. (F x) i f zawsze, gdy x nie występuje swobodnie w f.

O tym działaniu można myśleć jak o koncepcji lokalnej kompletności w dedukcji naturalnej poprzez izomorfizm Curry`ego-Howarda.

Formy normalne i łączenie

Dla nieopisanego rachunku lambda, redukcja β jako reguła przepisywania nie jest ani silnie normalizująca ani słabo normalizująca.

Można jednak wykazać, że redukcja β łączy się w pracy do transformacji α (t. е. dwie formy normalne można uznać za równe, jeśli możliwa jest α-konwersja jednej na drugą).

Dlatego zarówno silnie normalizujące terminy, jak i słabo normalizujące pojęcia mają jedną normalną postać. Dla pierwszych terminów każda strategia redukcji jest gwarantowana, że prowadzi do typowej konfiguracji. Natomiast dla warunków słabo normalizujących niektóre strategie redukcji mogą nie znaleźć się.

Dodatkowe metody programowania

Istnieje duża liczba idiomów tworzenia dla lambda-calculus. Wiele z nich zostało pierwotnie opracowanych w kontekście wykorzystania systemów jako podstawa semantyka język programowania, Efektywne stosowanie ich jako konstrukcji niskiego poziomu. Ponieważ niektóre style zawierają lambda-calculus (lub coś bardzo podobnego) jako fragment, techniki te również znajdują zastosowanie w praktycznej twórczości, ale mogą być wtedy postrzegane jako niejasne lub obce.

Stałe nazwane

W lambda-calculus, biblioteka ma postać zestawu wcześniej zdefiniowanych funkcji, w których wyrażenia są po prostu konkretnymi stałymi. Czysty rachunek nie ma pojęcia nazwanych niezmienników, ponieważ wszystkie atomowe wyrażenia lambda są zmiennymi. Ale można je również symulować, wybierając niestałą jako nazwę stałej, używając abstrakcji lambda do wiązania tego wariantu w części głównej i stosując tę abstrakcję do zamierzonej definicji. Zatem, jeśli użyjemy f do oznaczenia M w N, możemy powiedzieć,

(λ f. H) M.

Autorzy często wprowadzają pojęcie składniowe takie jak let, aby umożliwić pisanie rzeczy w bardziej intuicyjnym porządku.

f = M w N

Poprzez łączenie takich definicji, można napisać "program" rachunku lambda jako zero lub więcej definicji funkcji, po których następuje pojedynczy człon lambda, używający tych definicji, które stanowią większość programu.

Zauważalnym ograniczeniem tego let jest to, że nazwa f nie jest zdefiniowana w M, ponieważ M jest poza zakresem wiązania abstrakcji lambda f. Oznacza to, że atrybut funkcji rekurencyjnej nie może być używany jako M z let. Bardziej zaawansowana konstrukcja składniowa letrec, która pozwala na pisanie definicji funkcji rekurencyjnych w tym stylu, zamiast tego dodatkowo używa kombinatorów stałoprzecinkowych.

Analogi drukowane

Ten typ jest typowanym formalizmem, który używa symbolu do oznaczenia anonimowej funkcji abstrakcji. W tym kontekście typy są zwykle obiektami o charakterze syntaktycznym, które są przypisane do lambda-termów. Dokładny charakter zależy od danego rachunku. Z pewnego punktu widzenia, typowane PI mogą być postrzegane jako udoskonalenia nietypowych PI. Ale z drugiej strony, mogą być również uważane za bardziej fundamentalną teorię, a nieukierunkowany rachunek lambda jako specjalny przypadek z tylko jednym typem.

Typowane LI są założycielskimi językami programowania i podstawą języków funkcjonalnych, takich jak ML i Haskell. I, bardziej pośrednio, imperatywne style tworzenia. Typowane lambda-termy odgrywają ważną rolę w rozwoju systemów typów dla języków programowania. Tutaj typowanie zazwyczaj ujmuje pożądane właściwości programu, np. nie spowoduje naruszenia dostępu do pamięci.

Typizowany rachunek lambda jest ściśle związany z logiką matematyczną i teorią dowodu poprzez izomorfizm Curry-Howard, i może być postrzegany jako wewnętrzny język klas kategorii, na przykład, który jest po prostu stylem kartezjańskim zamkniętym.