Rachunek lambda (lub λ-rachunek ) jest formalny system wynaleziony przez Alonzo Church w 1930 roku , która określa pojęcia funkcji i aplikacji . Manipulujemy wyrażeniami zwanymi wyrażeniami λ, w których grecka litera λ jest używana do wiązania zmiennej. Na przykład, jeśli M jest wyrażeniem λ, λx.M jest również wyrażeniem λ i reprezentuje funkcję, która x kojarzy M.
Rachunek λ był pierwszym formalizmem, który zdefiniował i scharakteryzował funkcje rekurencyjne : ma zatem ogromne znaczenie w teorii obliczalności , na równi z maszynami Turinga i modelem Herbranda-Gödla . Od tego czasu jest stosowany jako teoretyczny język programowania i jako metajęzyk do formalnej demonstracji wspomaganej komputerowo . Rachunek lambda można wpisać lub nie .
Lambda-rachunek jest związana z logiki kombinatorycznej z Haskell Curry i uogólnione w obliczeniach wyraźnych substytucji .
Podstawową ideą rachunku lambda jest to, że wszystko jest funkcją . Funkcja jest w szczególności wyrażona wyrażeniem, które może zawierać funkcje, które nie zostały jeszcze zdefiniowane: te ostatnie są następnie zastępowane zmiennymi. Istnieje podstawowa operacja zwana aplikacją :
Odnotowano zastosowanie wyrażenia (opisującego funkcję) do wyrażenia (opisującego funkcję) .
Możemy również tworzyć funkcje, mówiąc, że jeśli E jest wyrażeniem, tworzymy funkcję, która dopasowuje x do wyrażenia E; Piszemy λx.E tę nową funkcję.
Nazwa zmiennej nie jest ważniejsza niż w wyrażeniu takim jak ∀x P (x), które jest równoważne z ∀y P (y) . Innymi słowy, jeśli E [y / x] jest wyrażeniem E, w którym wszystkie wystąpienia x zostały przemianowane na y , rozważymy, że wyrażenia λx.E i λy.E [y / x] są równoważne.
Korzystając z narzędzi, które właśnie nabyliśmy, uzyskujemy za pomocą aplikacji i abstrakcji dość skomplikowane funkcje, które możemy chcieć uprościć lub ocenić. Aplikacja uproszczenie z formą (λx.E) p powraca do przekształcenia alternatywnym ekspresji E gdzie każdy wolny od X otrzymuje P . Ta forma uproszczenia nazywana jest skróceniem (lub β- skróceniem, jeśli chcemy pamiętać, że stosujemy regułę β rachunku lambda).
Na tej podstawie możemy zbudować kilka ciekawych funkcji, takich jak funkcja tożsamości , która jest funkcją dopasowującą , innymi słowy funkcją . Możemy również skonstruować stałą funkcję równą , a mianowicie .
Stamtąd możemy zbudować funkcję, która tworzy funkcje stałe, pod warunkiem, że damy jej stałą jako parametr, innymi słowy funkcję , to znaczy funkcję, która sprawia, że funkcja jest stale równa .
Możemy też na przykład skonstruować funkcję, która permutuje użycie parametrów innej funkcji, a dokładniej, jeśli jest to wyrażenie, chcielibyśmy, aby działało jak . Funkcja jest funkcją . Jeśli zastosujemy funkcję do , otrzymamy, że możemy uprościć w .
Jak dotąd byliśmy dość nieformalni. Ideą rachunku lambda jest dostarczenie precyzyjnego języka do opisu funkcji i uproszczenie ich.
Rachunek lambda definiuje jednostki składniowe, które nazywane są terminami lambda (lub czasami także wyrażeniami lambda ) i które dzielą się na trzy kategorie :
Mapie widać w następujący sposób: jeśli u jest funkcją, a jeśli v jest jej argument, a następnie UV jest wynikiem mapy do v funkcji u .
Abstrakcji λ x . v można interpretować jako sformalizowanie funkcji, która do x wiąże v , gdzie v zwykle zawiera wystąpienia x .
Zatem funkcja f, która przyjmuje wyraz lambda x jako parametr i dodaje do niego 2 (tj. W obecnym zapisie matematycznym funkcja f : x ↦ x +2 ) będzie oznaczona w rachunku lambda wyrażeniem λ x . x +2 . Zastosowanie tej funkcji do liczby 3 jest zapisane ( λ x . X +2) 3 i jest „oceniane” (lub znormalizowane) w wyrażeniu 3 + 2 .
Alonzo Church znał relacje między jego rachunku i to od Russella i Whiteheada Principia Mathematica . Teraz używają one notacji do oznaczenia abstrakcji, ale Church użył zamiast niej notacji, która później stała się . Peano zdefiniował również abstrakcję w swojej formie matematycznej , używa w szczególności notacji, aby zwrócić uwagę na funkcję, taką jak .
Aby oddzielić aplikacje, zastosowano nawiasy, ale dla jasności niektóre nawiasy zostały pominięte. Na przykład piszemy x 1 x 2 ... x n dla (( x 1 x 2 ) ... x n ).
W rzeczywistości istnieją dwie konwencje:
Shönfinkel i Curry wprowadzono currying : jest to proces, za reprezentowanie funkcji z kilkoma argumentami. Na przykład funkcja, która z parą ( x , y ) wiąże u, jest uważana za funkcję, która z x wiąże funkcję, która z y wiąże u . Dlatego jest oznaczony: λx. (Λy.u) . Jest też napisane λx.λy.u lub λxλy.u lub po prostu λxy.u . Na przykład funkcja, która z parą ( x , y ) wiąże x + y, będzie oznaczona λx.λy.x + y lub po prostu λxy.x + y .
W ogólnych wyrażeniach matematycznych, aw szczególności w rachunku lambda, istnieją dwie kategorie zmiennych: zmienne swobodne i zmienne powiązane (lub głupie ). W rachunku lambda zmienna jest połączona przez λ. Powiązana zmienna ma zasięg, a ten zasięg jest lokalny. Ponadto można zmienić nazwę zmiennej związanej bez zmiany ogólnego znaczenia całego wyrażenia, w którym się pojawia. O zmiennej, która nie jest związana, mówi się, że jest wolna.
Powiązane zmienne w matematyceNa przykład w wyrażeniu zmienna jest wolna, ale zmienna jest połączona (przez ). To wyrażenie jest „to samo”, ponieważ było nazwą lokalną, tak jak jest . Z drugiej strony nie odpowiada temu samemu wyrażeniu, ponieważ jest wolny.
Tak jak całka łączy zmienną całkującą, tak samo jest ze zmienną, która po niej następuje.
Przykłady :
Określamy zestaw VL (t) o zmiennych wolnych o okresie T przez indukcję:
Termin, który nie zawiera żadnej wolnej zmiennej, jest nazywany zamkniętym (lub zamkniętym). O tym wyrażeniu lambda mówi się również, że jest kombinatorem (z powiązanej koncepcji logiki kombinatorycznej ).
Termin, który nie jest zamknięty, nazywany jest terminem otwartym.
Najważniejszym narzędziem rachunku lambda jest podstawianie, które pozwala na zastąpienie zmiennej terminem. Mechanizm ten jest podstawą redukcji, która jest podstawowym mechanizmem oceny wyrażeń, a więc „obliczania” wyrażeń lambda.
Podstawienie w okresie N t zmiennej x przez okres u oznaczono t [x: = U] . Należy podjąć pewne środki ostrożności, aby poprawnie zdefiniować podstawienie, aby uniknąć zjawiska przechwytywania zmiennych, które mogłoby, jeśli nie będziemy uważać, związać zmienną, która była wolna przed zastąpieniem.
Na przykład, jeśli u zawiera wolną zmienną y i jeśli x pojawia się w t jako wystąpienie podrzędu w postaci λy.v , może pojawić się zjawisko przechwytywania. Operacja t [x: = u] nazywana jest substytucją w t z x przez u i jest definiowana przez indukcję na t :
Uwaga : w ostatnim przypadku zwróćmy uwagę, że y nie jest wolną zmienną u . Rzeczywiście, zostałby wówczas „przechwycony” przez zewnętrzną lambdę. W takim przypadku zmieniamy nazwę y i wszystkie jej wystąpienia w v za pomocą zmiennej z, która nie występuje w t ani w u .
Konwersja α identyfikuje λy.v i λz.v [y: = z] . Mówi się, że dwa wyrażenia lambda, które różnią się tylko zmianą nazwy (bez przechwytywania) ich połączonych zmiennych, są α-konwertowalne . Konwersja α jest relacją równoważności między wyrażeniami lambda.
Przykłady:
Uwaga: konwersja α musi być dokładnie zdefiniowana przed podstawieniem. Zatem w terminie λx.λy.xyλz.z nie możemy nagle zmienić nazwy x na y (otrzymalibyśmy λy.λy.yyλz.z ), z drugiej strony możemy zmienić nazwę x na z .
Zdefiniowane w ten sposób substytucja jest mechanizmem zewnętrznym w stosunku do rachunku lambda, mówi się również, że jest częścią metateorii. Zauważ, że niektóre prace mają na celu wprowadzenie substytucji jako mechanizmu wewnętrznego rachunku lambda, prowadzącego do tak zwanych jawnych obliczeń przez podstawienie .
Jednym ze sposobów patrzenia na terminy rachunku lambda jest myślenie o nich jako o drzewach z węzłami binarnymi (odwzorowania), węzłami jednoargumentowymi (abstrakcje λ) i liśćmi (zmiennymi). Te redukcje są przeznaczone do zmiany warunków lub drzew jeśli widzimy je w ten sposób; na przykład zmniejszenie (λx.xx) (λy.y) daje (λy.y) (λy.y) .
Redex nazywamy wyrazem postaci (λx.u) v , gdzie u i v są wyrazy, a x zmienną. Definiujemy skurcz beta (lub skurcz β) (λx.u) v jako u [x: = v] . Mówimy, że człon C [u] redukuje się do C [u '], jeśli u jest reeksem, który β zawęża się do u' , wtedy piszemy C [u] → C [u '] , relację → nazywamy skróceniem .
Przykład skurczu :
(λx.xy) a daje (xy) [x: = a] = ay .
Oznaczamy → * z przechodnią odruchowe zamknięcie relacji skurczu → i nazywamy to ograniczenie . Innymi słowy, redukcja jest skończoną, prawdopodobnie pustą sekwencją skurczów.
Zdefiniować = β jako symetryczne i czasownik refleksyjnym zamknięciem skurczu i nazywa beta konwersji , p- konwersji , lub częściej beta równoważności lub β- równoważności .
Równoważność β pozwala na przykład porównać wyrazy, które nie dają się zredukować do siebie, ale które po serii β-skurczów prowadzą do tego samego wyniku. Na przykład (λy.y) x = β (λy.x) z, ponieważ dwa wyrażenia kurczą się, dając x .
Formalnie mamy M = β M ' wtedy i tylko wtedy, gdy ∃ N 1 , ..., N p takie, że M = N 1 , M' = N p i dla wszystkich i mniejsze niż p i większe niż 0 , N i → N i + 1 lub N i + 1 → N i .
Oznacza to, że w konwersji można zastosować redukcje lub odwrotne relacje redukcji (zwane ekspansjami ).
Definiujemy również inną operację, zwaną eta-redukcją , zdefiniowaną następująco: λx.ux → η u , gdy x nie wydaje się być wolne w u. Rzeczywiście, ux jest interpretowane jako obraz x przez funkcję u . Zatem λx.ux jest następnie interpretowane jako funkcja, która do x wiąże obraz x przez u , a więc jako samą funkcję u .
Obliczenie związane z członem lambda to sekwencja redukcji, które generuje. Termin jest opisem obliczenia, a jego wynikiem jest normalna postać terminu (jeśli występuje).
Mówi się, że człon lambda t jest w normalnej postaci, jeśli nie można do niego zastosować skurczu beta, tj. Jeśli t nie zawiera redex, lub jeśli nie ma wyrażenia lambda u takiego, że t → u . Struktura składniowa terminów w normalnej formie została opisana poniżej.
Przykład:λx.y (λz.z (yz))
Mówimy, że człon lambda t jest znormalizowany, jeśli istnieje wyraz u, do którego nie można zastosować skurczu beta i taki, że t = β u . Takie U jest nazywany postaci normalnej o t .
Mówimy, że człon lambda t jest silnie znormalizowany, jeśli wszystkie redukcje z t są skończone .
Przykłady:Niech Æ ≡ λx.xx być ustawiony .
Jeśli termin jest silnie znormalizowany, to można go znormalizować.
Twierdzenie Churcha-Rossera: niech t i u będą dwoma wyrazami takimi, że t = β u . Istnieje termin v taki, że t → * v i u → * v .
Rombu (lub zlania się) Twierdzenie niech t , U 1 i U 2 będzie lambda warunki tak, że t → * u 1 a t → * U 2 . Wtedy istnieje lambda określenie v taki sposób, że u 1 → * V i U 2 → * V .
Dzięki twierdzeniu Churcha-Rossera można z łatwością wykazać wyjątkowość postaci normalnej, a także spójność rachunku lambda (tj. Istnieją co najmniej dwa odrębne wyrażenia nieprzekształcalne beta).
Możemy opisać strukturę terminów w normalnej formie, które tworzą zbiór . W tym celu opisujemy tak zwane terminy neutralne, które tworzą zbiór . Terminy neutralne to terminy, w których zmienna (na przykład ) jest stosowana do terminów w normalnej formie. Na przykład jest neutralna, jeśli ... są w normalnej formie. Wyrazy w formie normalnej są terminami neutralnymi poprzedzonymi zerem, jednym lub większą liczbą λ, innymi słowy, kolejnymi abstrakcjami terminów w formie normalnej. Tak jest w normalnej formie. Możemy opisać terminy w normalnej formie za pomocą gramatyki.
Przykłady : jest neutralny, więc również w normalnej formie. jest w normalnej postaci. jest neutralna. jest w normalnej postaci. Z drugiej strony nie jest w formie normalnej, ponieważ nie jest neutralna i nie jest abstrakcją terminu w formie normalnej, ale także dlatego, że sam jest β-redex, a więc β -redukowalnym.
Jeśli chodzi o składnię i redukcję rachunku lambda, możemy dostosować różne obliczenia, ograniczając mniej więcej klasę terminów. Możemy zatem wyróżnić dwie główne klasy obliczeń lambda: nietypowy rachunek lambda i typowane obliczenia lambda. Typy są adnotacjami terminów, których celem jest zachowanie tylko terminów, które można znormalizować, być może poprzez przyjęcie strategii redukcji. Mamy zatem nadzieję, że rachunek lambda będzie zgodny z właściwościami Churcha-Rossera i normalizacji.
Korespondencja Curry-Howard dotyczy wpisywanych rachunek lambda do systemu naturalnej dedukcji. Stwierdza, że typ odpowiada zdaniu, a termin odpowiada dowodowi i vice versa.
Kody symulują typowe obiekty komputerowe, w tym liczby naturalne, funkcje rekurencyjne i maszyny Turinga. I odwrotnie, rachunek lambda może być symulowany przez maszynę Turinga. Dzięki tezie Churcha wnioskujemy, że rachunek lambda jest uniwersalnym modelem rachunku różniczkowego.
BooleansW części Składnia widzieliśmy, że definiowanie prymitywów jest praktyczne. To właśnie zamierzamy tutaj zrobić.
true = λab.a
false = λab.b
To jest tylko definicja kodowania i moglibyśmy zdefiniować inne.
Zauważamy, że: prawda xy → * x i : false xy → * y
Następnie możemy zdefiniować wyraz-lambda reprezentujący alternatywę: jeśli-to-jeszcze . Jest to funkcja z trzema argumentami, wartością logiczną b oraz dwoma wyrazami lambda u i v , która zwraca pierwszy, jeśli wartość logiczna jest prawdą, a drugi w przeciwnym razie.
ifthenelse = λbuv. (buv) .
Nasza funkcja jest weryfikowana: ifthenelse true xy = (λbuv. (buv)) prawda xy ; ifthenelse true xy → (λuv. (true uv)) xy ; ifthenelse prawda xy → * (prawda xy) ; ifthenelse true xy → * ((λab.a) xy) ; ifthenelse true xy → * x .
Zobaczymy w ten sam sposób ifthenelse false xy → * y .
Stamtąd mamy również wyrażenie lambda dla klasycznych operacji logicznych: no = λb.ifthenelse b false true ; i = λab.ifthenelse ab false (albo λab.ifthenelse aba ); gdzie = λab.ifthenelse a true b (lub λab.ifthenelse aab ).
Liczby całkowitePoniższe kodowanie liczb całkowitych jest nazywane liczbami całkowitymi Kościoła od nazwiska ich projektanta. Pytamy: 0 = λfx.x , 1 = λfx.fx , 2 = λfx.f (fx) , 3 = λfx.f (f (fx)) i na ogół: n = λfx.f (f (... (fx) ...)) = λfx.f n x z f iterowanymi n razy.
Zatem liczba całkowita n jest postrzegana jako funkcjonał, który łączy f n (x) z parą ff, x≻ .
Niektóre funkcjeIstnieją dwa sposoby zakodowania funkcji następcy , albo przez dodanie f na początku, albo na końcu. Na początku mamy n = λfx.f n x i chcemy λfx.f n + 1 x . Konieczne jest, aby móc dodać f albo na początku f („pod” lambdami), albo na końcu.
Pozostałe funkcje są zbudowane na tej samej zasadzie. Na przykład dodawanie przez „konkatenację” dwóch wyrażeń lambda: λnpfx.nf (pfx) .
Aby zakodować mnożenie , używamy f do „propagowania” funkcji w całym wyrazie : λnpf.n (pf)
Poprzednik i odejmowanie nie są proste albo. Porozmawiamy o tym później.
Możemy zdefiniować test przy 0 w następujący sposób: if0thenelse = λnab.n (λx.b) a lub używając wartości Booleans λn.n (λx.false) true .
IteratoryNajpierw zdefiniujmy funkcję iteracji na liczbach całkowitych: iterates = λnuv.nuv
v jest podstawą, a u funkcją. Jeśli n wynosi zero, obliczamy v , w przeciwnym razie obliczamy u n (v) .
Na przykład dodatek, który pochodzi z następujących równań
można zdefiniować w następujący sposób. Podstawowy przypadek v to liczba p , a funkcja u jest funkcją następczą . Zatem składnik lambda odpowiadający obliczeniu sumy to: add = λnp. iter n następca s . Zauważ, że dodaj np → * n następcę s .
ParyMożemy zakodować pary przez c = λz.zab, gdzie a jest pierwszym elementem, a b drugim. Oznaczymy tę parę (a, b) . Aby uzyskać dostęp do dwóch części, używamy π 1 = λc.c (λab.a) i π 2 = λc.c (λab.b) . Rozpoznamy prawdziwe i fałszywe wartości logiczne w tych wyrażeniach i pozostawimy czytelnikowi zredukowanie π 1 (λz.zab) do a .
ListyMożemy zauważyć, że liczba całkowita to lista, której nie przyglądamy się elementom, biorąc pod uwagę tylko długość. Dodając informacje odpowiadające elementom, możemy budować listy w sposób analogiczny do liczb całkowitych: [a 1 ; ...; a n ] = λgy. ga 1 (... (ga n y) ...). Więc : [] = λgy.y; [a 1 ] = λgy.ga 1 rok; [a 1 ; a 2 ] = λgy.ga 1 (ga 2 y).
Iteratory na listachW ten sam sposób, w jaki wprowadziliśmy iterację na liczbach całkowitych, wprowadzamy iterację na listach. lista_funkcji jest zdefiniowana przez λlxm.lxm jak dla liczb całkowitych. Koncepcja jest prawie taka sama, ale są drobne niuanse. Zobaczymy na przykładzie.
przykład: długość listy jest zdefiniowana przez
x :: l to lista nagłówków x i ogonów l (notacja ML ). Funkcja długości zastosowana do listy l jest kodowana przez: λl.liste_it l (λym.add (λfx.fx) m) (λfx.x) Lub tylko λl.l (λym.add 1 m) 0.
Drzewa binarneZasada konstrukcji liczb całkowitych, par i list jest uogólniona na drzewa binarne:
Drzewo to albo liść, albo węzeł. W tym modelu żadne informacje nie są przechowywane na poziomie węzła, dane (lub klucze) są przechowywane tylko na poziomie liścia. Następnie możemy zdefiniować funkcję, która oblicza liczbę liści drzewa: nb_feuilles = λa.arbre_it a (λbc.add bc) (λn.1) lub prościej: nb_feuilles = λa.a add (λn.1)
PoprzednikAby zdefiniować poprzednika na liczbach całkowitych Kościoła, konieczne jest użycie par. Chodzi o to, aby zrekonstruować poprzednika poprzez iterację: pred = λn.π 1 (iteruje n (λc. (Π 2 c, następca (π 2 c))) (0,0)). Ponieważ poprzednik liczb całkowitych naturalnych nie jest zdefiniowany jako 0, w celu zdefiniowania funkcji całkowitej przyjęliśmy tutaj konwencję, że jest ona równa 0.
Sprawdzamy na przykład, że pred 3 → * π 1 (iter 3 (λc. (Π 2 c, następca (π 2 c))) (0,0)) → * π 1 (2,3) → * 2.
Wychodzimy z tego, że odejmowanie można zdefiniować wzorem: sub = λnp. Iteruje p pred n z konwencją, że jeśli p jest większe od n, to sub np jest równe 0.
RekursjaŁącząc poprzednik i iterator, otrzymujemy rekursor . Różni się to od iteratora tym, że funkcja, która jest przekazywana jako argument, ma dostęp do poprzednika.
rec = λnfx.π 1 (n (λc. (f (π 2 c) (π 1 c), następca (π 2 c))) (x, 0))
Sumatory punktów stałych
Sumator punktów stałych umożliwia skonstruowanie dla każdego F rozwiązania równania X = FX . Jest to przydatne do programowania funkcji, które nie są wyrażane po prostu przez iterację, takich jak gcd, i jest szczególnie potrzebne do programowania funkcji częściowych.
Najprostszym stały punkt łączący ze względu na curry, to: Y = λf. (Λx.f (xx)) (λx.f (xx)). Turing zaproponował inny łącznik punktów stałych: Θ = (λx. Λy. (Y (xxy))) (λx. Λy. (Y (xxy))).
Sprawdzamy to cokolwiek g. Dzięki łącznikowi stałoprzecinkowemu możemy na przykład zdefiniować funkcję, która przyjmuje funkcję jako argument i sprawdza, czy ta funkcja argumentu zwraca prawdę dla przynajmniej jednej liczby całkowitej: teste_annulation = λg.Y (λfn.ou (gn) (f (następca n))) 0.
Na przykład, jeśli zdefiniujemy przemienną sekwencję wartości logicznych prawda i fałsz : alternates = λn.itère n not false, to sprawdzamy, czy: teste_annulation alternates → * or (alternates 0) (Y (λfn.or (alternates n) ( f następca n)) (następca 0)) → * lub (alternatywy 1) (Y (λfn. lub (alternatywy n) (f następca n)) (następca 1)) → * prawda.
Możemy również zdefiniować gcd: pgcd = Y (λfnp.if0thenelse (sub pn) (if0thenelse (sub np) p (fp (sub np))) (fn (sub pn))).
Połączenie z rekurencyjnymi funkcjami częściowymiRekursor i punkt stały są kluczowymi składnikami pokazującymi, że każda rekurencyjna funkcja częściowa jest definiowalna w rachunku λ, gdy liczby całkowite są interpretowane przez liczby całkowite Kościoła. Odwrotnie, wyrażenia λ mogą być kodowane przez liczby całkowite, a redukcja składników λ jest definiowana jako (częściowa) funkcja rekurencyjna. Rachunek λ jest zatem modelem obliczalności .
Terminy opatrujemy adnotacjami wyrażeniami zwanymi typami . Robimy to, umożliwiając wpisanie terminu. Jeśli ta metoda się powiedzie, mówimy, że termin jest dobrze wpisany . Oprócz tego, że daje to wskazówkę, co funkcja „robi”, np. Przekształca obiekty pewnego typu w obiekty innego typu, pomaga zapewnić silną normalizację , czyli - to znaczy dla wszystkich terminów redukcje skutkują normalną formą (która jest unikalna dla każdego terminu początkowego). Innymi słowy, wszystkie obliczenia przeprowadzone w tym kontekście kończą się. Te typy proste są skonstruowane jako typów funkcji Funkcje Funkcje Funkcje Funkcje funkcji do funkcji, etc. Cokolwiek by się wydawało, siła ekspresyjna tego rachunku jest bardzo ograniczona (stąd nie można w nim zdefiniować wykładni ani nawet funkcji ).
Bardziej formalnie, proste typy są zbudowane w następujący sposób:
Intuicyjnie, drugi przypadek reprezentuje typ funkcji, które pobierają element typu i zwracają element typu .
Kontekst to zestaw par postaci, w którym jest zmienną i typem. Wyrok typowania jest trójka (my wtedy powiedzieć, że jest dobrze wpisany ), zdefiniowane rekurencyjnie przez:
Jeśli dodaliśmy stałe do obliczenia lambda, musimy nadać im typ (przez ).
Prosty typ rachunku lambda jest zbyt restrykcyjny, aby wyrazić wszystkie obliczalne funkcje , których potrzebujemy w matematyce, a zatem w programie komputerowym. Jednym ze sposobów na przezwyciężenie wyrazistości prostego rachunku lambda jest zezwolenie na zmienne typu i kwantyzacja nad nimi, tak jak ma to miejsce w systemie F lub rachunku konstruktów .
Rachunek lambda stanowi teoretyczną podstawę programowania funkcjonalnego i tym samym wpłynął na wiele języków programowania. Pierwszym z nich jest Lisp, który jest językiem bez typu. Później zostaną opracowane ML i Haskell , które są językami maszynowymi.
Indeksy de Bruijna są zapisem rachunku lambda, który umożliwia przedstawienie za pomocą terminu każdej klasy równoważności dla konwersji α. W tym celu de Bruijn zaproponował zastąpienie każdego wystąpienia zmiennej liczbą naturalną. Każda liczba naturalna oznacza liczbę λ, którą należy przekroczyć, aby powiązać wystąpienie z jego łącznikiem.
Stąd termin λ x. xx jest reprezentowane przez termin λ 0 0, podczas gdy termin λx. λy. λz .xz (yz) jest reprezentowane przez λ λ λ 2 0 (1 0) , ponieważ w pierwszym przypadku ścieżka od x do jego łącznika nie przecina żadnego λ, podczas gdy w drugim przypadku ścieżka od x na jego łączniku przecina dwa λ (a mianowicie λy i λz ), ścieżka y na jego łączniku przecina λ (mianowicie λz ), a ścieżka z na jego łączniku nie przecina żadnego λ.
Jako inny przykład, termin (λ x λ y λ z λ u. (X (λ x λ y. X))) (λ x. (Λ x. X) x) i termin, który jest jego odpowiednikiem α czyli (λ x λ y λ z λ u. (x (λ v λ w. v))) (λ u. (λ t. t) u) są reprezentowane przez (λ λ λ λ (3 (λ λ 1 ))) (λ (λ 0) 0) (patrz rysunek).