Paradygmaty programowania/Wykład 8: U podstaw programowania funkcyjnego — rachunek lambda

Wstęp

W latach trzydziestych XX wieku Alonzo Church i Haskell Curry, pracując niezależnie, opracowali notację dla funkcji — rachunek lambda. Spojrzenie na funkcje w rachunku lambda jest nieco inne od klasycznego, teoriomnogościowego rozumienia funkcji jako zbioru par argument-wartość. W rachunku lambda funkcje rozumiane są jako przepisy, aby podkreślić ich obliczalność. Rachunek lambda ma dwa zasadnicze warianty: nietypowany, zwany po prostu rachunkiem lambda, oraz typowany. Najpierw przedstawimy nieco obszerniej ten pierwszy; później powiemy krótko o rachunku z typami.

Podstawowe definicje i własności

Napisy w rachunku lambda nazywamy termami. Zbiór $\Lambda$ termów rachunku lambda konstruuje się indukcyjnie jako zbiór słów nad alfabetem $Var\cup \{(,),\lambda \}$, gdzie $Var$ jest przeliczalnym zbiorem ziennych. Do zbioru $\Lambda$ należą tylko termy skonstruowane w poniższy sposób:

• Dowolna zmienna ze zbioru $Var$ jest termem rachunku lambda, czyli jeżeli $x\in Var$, to $x\in \Lambda$.

• Jeżeli weźmiemy dowolny term $M$ ze zbioru $\Lambda$, oraz dowolną zmienną $x$ ze zbioru $Var$, to term postaci $(\lambda x.M)$ jest termem rachunku lambda, czyli jeżeli $M\in \Lambda$ i $x\in Var,$ to $(\lambda x.M)\in \Lambda$. Powyższy sposób tworzenia termu nazywamy abstrakcją.

• Inna metoda to metoda aplikacji, czyli jeżeli termy $M\in \Lambda$ i $N\in \Lambda ,$ to $(MN)\in \Lambda$.

Nawiasy są często pomijane według zasady łączności lewostronnej: na przykład $MNPQ\equiv (((MN)P)Q).$ Wieloargumentowe funkcje są reprezentowane przez funkcje jednoargumentowe, których argumentami są funkcje. Zatem to, co zwykle jest zapisywane w postaci $F(N,M)$, w rachunku lambda zapisuje się $((FN)M)\equiv FNM.$ Powtórzenia symbolu $\lambda$ pomijane są według zasady łączności prawostronnej, tzn. $\lambda xyz.M\equiv (\lambda x.(\lambda y.(\lambda z.M))).$

W termie rachunku lambda zmienna może być wolna albo związana. Wolnym wystapieniem zmiennej $x$ nazywamy tylko takie wystąpienie tej zmiennej, które nie jest „w zasięgu” żadnego $\lambda x$.

Zbiór zmiennych wolnych termu $M$, oznaczany przez $FV(M)$, zdefiniowany jest, w zależności od budowy termu $M$, w następujący sposób:

• Jeżeli $M$ jest pojedynczą zmienną, tzn. $M\equiv x$, to zmienna ta jest wolna, a zatem $FV(M)=\{x\}$.

• Jeżeli $M$ jest postaci $\lambda x.M'$, to $\lambda x$ wiąże wszystkie wolne wystąpienia zmiennej $x$ w termie $M'$, a zatem $FV(M)=FV(M')-\{x\}$.

• Jeżeli $M$ jest postaci $PQ$, to zmiennymi wolnymi termu $M$ są wszystkie zmienne wolne występujące w termach $P$ i $Q$, czyli $FV(M)=FV(P)\cup FV(Q).$

Zmienna jest zmienną wolną termu $M$, jeżeli należy do zbioru $FV(M),$ a zmienną związaną w przeciwnym wypadku.

Term Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle M} jest domknięty wtedy i tylko wtedy, gdy Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle FV(M)=\emptyset.}

Przykład

• W termie Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle M = y(\lambda x.x)} zmienna Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle y} jest zmienną wolną, a Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle x} zmienną związaną. W termie $\lambda y.M$ nie ma zmiennych wolnych, jest to więc term domknięty.

• W termie $M=x(\lambda x.x)$ tylko pierwsze wystąpienie zmiennej $x$ jest wolne, chociaż $FV(M)=\{x\}$. Oczywiście term $M$ nie jest termem domkniętym.

Na termy w rachunku lambda patrzymy jako na przepisy, jak z zadanej wartości argumentu otrzymać wartość funkcji; zatem termy to procedury, których parametry specyfikowane są poprzez lambda abstrakcję:

Parser nie mógł rozpoznać (błąd składni): {\displaystyle \lambda \underbrace{x_1... x_n}_{\mbox{\tiny parametry}}. \underbrace{M}_{\mbox{\tiny ciało procedury}}}

Alfa-konwersja i beta-redukcja, czyli obliczanie

Termy rachunku lambda możemy przekształcać, korzystając z $\alpha$-konwersji i $\beta$-redukcji.

$\alpha$-konwersja to po prostu zamiana nazw zmiennych związanych. Zdarza się, że na przykład poprzez stosowanie „podprocedur” lub parametrów pochodzących z wykonania innych procedur dochodzi do konfliktu nazw zmiennych. Aby zapewnić poprawne wykonanie, stosujemy $\alpha$-konwersję, która pozwala zapewnić unikalność nazw.

$\lambda x.M\rightarrow _{\alpha }\lambda y.M[x/y],$

gdzie $y\not \in FV(M)$, a $M[x/y]$ oznacza wynik postawienia zmiennej $y$ za każde wolne wystąpienie zmiennej $x$ w termie $M$.

Będziemy używać oznaczenia $T_{1}=_{\alpha }T_{2}$, aby powiedzieć, że termy $T_{1}$ i $T_{2}$ są równe modulo $\alpha$-konwersja, tzn. że mogą być zredukowane do tego samego termu dzięki zastosowaniu skończonej liczby $\alpha$-konwersji.

Przykład Niech $x$, $y$, $z$ oznaczają różne zmienne. Wówczas

Parser nie mógł rozpoznać (nieznana funkcja „\aligned”): {\displaystyle \aligned \lambda x.x & =_\alpha \lambda y.y\\ \lambda x.xz & =_\alpha \lambda y.yz\\ \lambda x.xy & \neq_{\alpha} \lambda x.xz. \end{align}}

$\beta$-redukcja — obliczenia wykonywane przez procedurę symulowane są w rachunku lambda poprzez proces zwany $\beta$-redukcją. Aplikujemy procedurę $\lambda x.M$ do argumentu $N$:

$(\lambda x.M)N\rightarrow _{\beta }M[x/N]$

w taki sposób, że każda zmienna wolna termu $N$ pozostaje wolna po podstawieniu. Jest to oczywiście możliwe do osiągnięcia po ewentualnym wcześniejszym zastosowaniu $\alpha$-konwersji. Na przykład:

$(\lambda xy.xy)y\rightarrow \lambda y.yy$

jest nieprawidłowym użyciem $\beta$-konwersji, gdyż dochodzi do konfliktu oznaczeń i do utraty pierwotnego znaczenia termu-procedury. Jednakże można temu zaradzić, stosując $\alpha$-konwersję:

$(\lambda xy.xy)y=_{\alpha }(\lambda xz.xz)y=_{\beta }\lambda z.yz.$

Używamy oznaczenia $T_{1}=_{\beta }T_{2}$, aby powiedzieć, że termy $T_{1}$ i $T_{2}$ są równe modulo $\beta$-konwersja, tzn. że mogą być zredukowane do tego samego termu dzięki zastosowaniu skończonej liczby $\beta$-konwersji.

Aplikację $PQ$ nazywamy $\beta$-redeksem, jeżeli term $P$ jest w postaci $\lambda$-abstrakcji. Term $M$ jest w postaci normalnej, jeżeli nie zawiera $\beta$-redeksów, tzn. żaden podterm termu $M$ nie jest $\beta$-redeksem.

Własność Churcha-Rossera

Poniższe twierdzenie zwane jest własnością Churcha-Rossera lub własnością karo:

Jeżeli term $M$ poprzez pewne ciągi $\beta$-redukcji redukuje się do termów $N_{1}$ i $N_{2}$, to istnieje term $M'$ taki, że zarówno $N_{1}$, jak i $N_{2}$ można zredukować do $M'$ (poprzez ciągi $\beta$-redukcji):

Powyższa własność mówi, że postać normalna (o ile istnieje) jest unikalna z dokładnością do $\alpha$-konwersji.

Term $T$ jest normalizowalny, jeżeli można go zredukować do postaci normalnej, a jest silnie normalizowalny, jeżeli każda droga redukcji prowadzi do postaci normalnej. Beztypowy rachunek lambda nie ma żadnej z tych własności. Wprowadźmy oznaczenie: $\Delta =\lambda x.xx$. Najprostszym przykładem termu nie posiadającego postaci normalnej jest $\Delta \Delta$:

$\Delta \Delta =(\lambda x.xx)\Delta =_{\beta }\Delta \Delta .$

Przykładem termu, w którym nie każda droga redukcji prowadzi do postaci normalnej, jest:

Parser nie mógł rozpoznać (nieznana funkcja „\aligned”): {\displaystyle \aligned \overbrace{(\lambda x.y) (\underbrace{\Delta\Delta}_{(1)})}^{(2)} & =_\beta (\lambda x.y)(\Delta\Delta) & =_\beta & \mbox{~~~~...} & \mbox{~~~~~~| redukując (1)}\\ & =_\beta y & & & \mbox{~~~~~~| redukując (2)} \end{align} }

Istnieją strategie redukcji, które zawsze doprowadzają do postaci normalnej, oczywiście gdy postać normalna istnieje. Taką strategią jest na przykład metoda redukowania zawsze najbardziej lewego redeksu.

Lambda-definiowalność funkcji na liczbach naturalnych

Do tej pory nie przedstawiliśmy żadnych termów oznaczających liczby naturalne czy funkcje operujące na liczbach naturalnych, wydaje się więc rzeczą dziwną mówienie o lambda reprezentowalności tych funkcji. Okazuje się jednak, że w rachunku lambda nie potrzeba żadnych dodatkowych oznaczeń: pojęcie liczby i funkcji daje się wprowadzić na bazie do tej pory przyjętych definicji.

Popatrzmy na liczbę naturalną $n$ jak na procedurę, która $n$-krotnie stosuje następnik do zera. Oczywiste jest, że taka procedura w sposób jednoznaczny określa liczbę, i na odwrót. Mając dany przepis wiemy, jaką liczbę naturalną liczy, a mając liczbę naturalną doskonale wiemy, który przepis zastosować.

• Term $\lambda sx.\ x$ reprezentuje liczbę naturalną 0.

• Term Parser nie mógł rozpoznać (błąd składni): {\displaystyle \lambda sx.\ \underbrace{s( s( ... (s}_{\mbox{\tiny n razy}}x) ...))} reprezentuje liczbę naturalną $n$.

Term $\lambda sx.\ x$ to po prostu algorytm: „weź następnik $s$, weź zero $x$ i zwróć zero”; natomiast term Parser nie mógł rozpoznać (błąd składni): {\displaystyle \lambda sx.\ \underbrace{s( s( ... (s}_{\mbox{\tiny n razy}}x) ...))} to algorytm: „weź następnik $s$, weź zero $x$, zastosuj $n$-krotnie następnik do zera i zwróć wynik”. Zatem liczba naturalna w naszym rozumieniu to procedura, która ma dwa parametry: $s$ (następnik) oraz $x$ (zero).

Oczywiście powyższe termy podane są z dokładnością do $\alpha$-konwersji. Np. term $\lambda ty.t(ty)$ reprezentuje 2, gdyż $\lambda ty.t(ty)=_{\alpha }\lambda sx.s(sx)$.

Mówimy, że term $E$ rachunku lambda reprezentuje funkcję na liczbach naturalnych $e:\mathbb {N} ^{k}\to \mathbb {N}$ wtedy i tylko wtedy, gdy $E{\underline {n_{1}}}...{\underline {n_{k}}}=_{\alpha \beta }{\underline {e(n_{1},...,n_{k})}}$, gdzie ${\underline {n}}$ oznacza reprezentację liczby $n$ w rachunku lambda.

Operacje na liczbach

Znając reprezentację liczb naturalnych w rachunku lambda, możemy zdefiniować podstawowe operacje na liczbach.

Term

Parser nie mógł rozpoznać (nieznana funkcja „\aligned”): {\displaystyle \aligned A & = & \lambda mnsx. (ms)(nsx) \end{align}}

reprezentuje dodawanie. Jest to procedura, która oczekuje na podanie dwóch parametrów: $m$ i $n$, a w wyniku daje procedurę liczącą liczbę naturalną (będącą sumą liczb $m$ i $n$). Jak wygląda algorytm otrzymany w wyniku działania procedury $A$? Jest to algorytm, który $m$-krotnie stosuje następnik do $n$.

Przykład Zobaczmy, jak działa term $A$ na liczbach 1 i 2:

Parser nie mógł rozpoznać (nieznana funkcja „\aligned”): {\displaystyle \aligned A\underline{1}\ \underline{2} & = & & \{[\lambda m.\ (\lambda n.\ (\lambda sx.\ (ms)(nsx))]\underline{1}\} \underline{2} & & \mbox{~~~~~~| dopisując nawiasy i } \lambda\\ & =_\beta & &[\lambda n.\ (\lambda sx.\ (\underline{2}s)(nsx)]\underline{1} & & \mbox{~~~~~~| } m := 2\\ & =_\beta & & \lambda sx.\ (\underline{2} s)(\underline{1} sx) & & \mbox{~~~~~~| } n := 1\\ & = & & \lambda sx.\ (\underline{2} s)\{[(\lambda t.\ (\lambda y.\ ty))s]x\} & & \mbox{~~~~~~| dopisując nawiasy i } \lambda\\ & =_\beta & & \lambda sx.\ (\underline{2} s)[(\lambda y.\ sy)x] & & \mbox{~~~~~~| } t := s\\ & =_\beta & & \lambda sx.\ (\underline{2} s)(sx) & & \mbox{~~~~~~| } y := x\\ & = & & \lambda sx.\ \{\underbrace{[ \lambda t.\ (\lambda y. t(ty))]}_{\mbox{\tiny procedura licząca 2}} s\} \underbrace{(sx)}_{\mbox{\tiny „zero”}} & & \mbox{~~~~~~| dopisując nawiasy i } \lambda\\ & =_\beta & & \lambda sx.\ (\lambda y.\ s(sy))(sx) & & \mbox{~~~~~~| } t := s\\ & =_\beta & & \lambda sx.\ s(s(sx)) & & \mbox{~~~~~~| } y := sx\\ & = & & \underline{3} \end{align}}

Term

Parser nie mógł rozpoznać (nieznana funkcja „\aligned”): {\displaystyle \aligned M & = & \lambda mnsx. n(ms)x \end{align}}

reprezentuje mnożenie. Procedura mnożenia oczekuje na podanie dwóch argumentów $m$ i $n$, a w wyniku daje procedurę, która liczy liczbę naturalną w sposób następujący: $m$-krotnie dodaje liczbę $n$, zaczynając od zera. Liczba naturalna obliczona w taki sposób to $m\cdot n$.

Przykład

Parser nie mógł rozpoznać (nieznana funkcja „\aligned”): {\displaystyle \aligned M\underline{2}\ \underline{2} & = & & \{[\lambda m.\ (\lambda n.\ (\lambda sx.\ n(ms)x))]\underline{2}\} \underline{2} & & \mbox{~~~~~~| dopisując nawiasy i } \lambda\\ & =_\beta & & [\lambda n.\ (\lambda sx.\ n(\underline{2}s)x)]\underline{2} & & \mbox{~~~~~~| } m := 2\\ & =_\beta & & \lambda sx.\ \underline{2} (\underline{2} s)x & & \mbox{~~~~~~| } n := 2\\ & = & & \lambda sx.\ \underline{2} [\underbrace{(\lambda t.\ (\lambda y.\ t(ty)))}_{\mbox{\tiny procedura licząca 2}}s]x & & \mbox{~~~~~~| dopisując nawiasy i } \lambda\\ & =_\beta & & \lambda sx.\ \underline{2} [\lambda y.\ s(sy)] x & & \mbox{~~~~~~| } t := s\\ & = & & \lambda sx.\ \underbrace{[ \lambda t.\ (\lambda z. t(tz))]}_{\mbox{\tiny procedura licząca 2}} \underbrace{[\lambda y. s(sy)]}_{\mbox{\tiny dodawanie 2}} x & & \mbox{~~~~~~| dopisując nawiasy i } \lambda\\ & =_\beta & & \lambda sx.\ (\lambda z.\ [\lambda y. s(sy)] ([\lambda y. s(sy)]z))x & & \mbox{~~~~~~| } t := [\lambda y. s(sy)]\\ & =_\beta & & \lambda sx.\ [\lambda y. s(sy)] ([\lambda y. s(sy)]z) & & \mbox{~~~~~~| } z := x\\ & =_\beta & & \lambda sx.\ s(s[s(sx)]) & &\mbox{~~~~~~| } y := s(sx)\\ & = & & \underline{4} \end{align}}

Term

Parser nie mógł rozpoznać (nieznana funkcja „\aligned”): {\displaystyle \aligned C & = & \lambda mnksx. m(\lambda y.nsx)(ksx) \end{align}}

reprezentuje funkcję $if_{-}then_{-}else$. Term $C$ oczekuje na podanie trzech argumentów i tak jak w poprzednich przykładach zwraca procedurę obliczającą liczbę naturalną. W przypadku, gdy pierwszy parametr $m$ jest zerem, procedura wynikowa liczy liczbę $k$, w przeciwnym przypadku — liczbę $n$.

Przykład Zobaczmy dwa przykłady działania termu $C$ -- pierwszy, gdy $m=0$, oraz drugi, gdy $m\neq 0$.

Przykład pierwszy

Parser nie mógł rozpoznać (nieznana funkcja „\aligned”): {\displaystyle \aligned \mbox{} C \underline{0}\ \underline{n}\ \underline{k} & =_\beta & & \lambda sx.\ \underline{0} (\lambda y.\ \underline{n} sx) (\underline{k} sx)\\ & = & & \lambda sx.\ \underbrace{(\lambda tz. z)}_{\underline{0}} (\lambda y.\ \underline{n} sx)(\underline{k}sx) \\ & =_\beta & & \lambda sx.\ \underline{k} sx \\ & =_\beta & & \underline{k} \end{align}}

Przykład drugi

Parser nie mógł rozpoznać (nieznana funkcja „\aligned”): {\displaystyle \aligned C \underline{m}\ \underline{n}\ \underline{k} & =_\beta & & \lambda sx. \underline{m} (\lambda y. \underline{n} sx) (\underline{k} sx) \\ & = & & \lambda sx.\ [\lambda tz.\ \underbrace{t(... (t}_{\tiny m\neq 0 \mbox{ razy}}y) ...)] (\lambda y.\ \underline{n} sx)(\underline{k} sx) \\ & =_\beta & & \lambda sx. [\lambda y.\ \underline{n} sx] (... ([\lambda y.\ \underline{n} sx](\underline{k} sx)) ...)\\ & =_\beta & & \lambda sx. \underline{n} sx \end{align}}

Przekazanie funkcji jako parametru

Musimy częściowo zapomnieć o naszych intuicjach, gdy spojrzymy na term reprezentujący funkcję wykładniczą. Co prawda jest to term, który jak wszystkie poprzednie oczekuje na podanie (dwóch) parametrów,  w wyniku daje procedurę liczącą liczbę naturalną, ale trudno tu dopatrzeć się analogii do tych języków programowania, które przekazują parametry tylko przez wartość.

Term

Parser nie mógł rozpoznać (nieznana funkcja „\aligned”): {\displaystyle \aligned E & = & \lambda mn. (mn) \end{align}}

reprezentuje funkcję $e(m,n)=n^{m}$ i ma pewną „niezwykłą” własność: w wyniku zwraca algorytm, który „zero” jednego z parametrów traktuje jako następnik. Oto przykład:

Parser nie mógł rozpoznać (nieznana funkcja „\aligned”): {\displaystyle \aligned E\underline{2}\ \underline{2} & = & & [\lambda mn.\ (mn)] \underline{2}\ \underline{2}\\ & =_\beta & & \underline{2}\ \underline{2} & & \mbox{~~~~~~| } m := \underline{2},\ n := \underline{2}\\ & = & & \underbrace{[\lambda sx.\ s(sx)]}_{\underline{2}}\underline{2} &\\ & =_\beta & & \lambda x.\ \underline{2} (\underline{2} x) & & \mbox{~~~~~~| } s := \underline{2}\\ & =_\alpha & & \lambda s.\ \underline{2} (\underline{2} s) & & \mbox{~~~~~~| } x := s\\ & = & & \lambda s. [\lambda tx.\ t(tx)](\underline{2} s)\\ & =_\beta & & \lambda sx.\ (\underline{2} s)((\underline{2} s)x) & & \mbox{~~~~~~| } t := \underline{2} s\\ & = & & \lambda sx.\ (\underbrace{[\lambda ty. t(ty)]}_{\underline{2}}s) ((\underbrace{[\lambda pz. p(pz)]}_{\underline{2}}s)x)\\ & =_\beta & & \lambda sx.\ [\lambda y.\ s(sy)](s(sx)) & & \mbox{~~~~~~| } t := s,\ p := s,\ z := x\\ & =_\beta & & \lambda sx.\ s(s[s(sx)]) & & \mbox{~~~~~~| } y := s(sx)\\ & = & & \underline{4} \end{align} }

Ciekawym termem jest też term reprezentujący poprzednik:

Parser nie mógł rozpoznać (nieznana funkcja „\aligned”): {\displaystyle \aligned P & = & \lambda n. (n (\lambda z. <\!\! A\underline{1} (z\underline{0}), (z\underline{0})\!\!>) <\!\!\underline{0}, \underline{0}\!\!>) \underline{1}, \end{align}}

gdzie $A$ oznacza wspominany już wcześniej term dodawania, $z$ jest parą uporządkowaną, której pierwsza składowa to $z{\underline {0}}$, natomiast druga to $z{\underline {1}}$. Jaką procedurę opisuje term $P$? Mówi on tyle: „weź liczbę naturalną $n$, a następnie $n$ razy wykonaj algorytm weź parę $z$ i utwórz nową parę $<\!\!1+z0,z0\!\!>$, startując od pary $<\!\!{\underline {0}},{\underline {0}}\!\!>$; jako wynik zwróć drugą składową ostatnio otrzymanej pary”. Uwaga: term rerprezentujący parę uporządkowaną zapisujemy tu w nawiasach kątowych, by odróżnić je od nawiasów grupujących fragmenty termów.

Wygląda to następująco:

Parser nie mógł rozpoznać (nieznana funkcja „\aligned”): {\displaystyle \aligned <0, 0> & \mbox{~}\\ <1, 0> & \mbox{~~~~~~krok 1}\\ <2, 1> & \mbox{~~~~~~{krok 2}}\\ ... \\ <n, n-1> & \mbox{~~~~~~krok } n \end{align} }

Zatem term $P$ definiuje funkcję $p(n)=(f^{(n)}(0,0))_{2}$, gdzie $f(x,y)=<\!x+1,x\!>$.

Przykład Zobaczmy teraz, jak działa term opisujący powyższą procedurę. Policzmy:

Parser nie mógł rozpoznać (nieznana funkcja „\aligned”): {\displaystyle \aligned P\underline{2} & = & & \{\lambda n. (n (\lambda z. <\!\!A\underline{1} (z\underline{0}), (z\underline{0}) \!\!>) <\!\!\underline{0}, \underline{0}\!\!>)\underline{1}\}\underline{2}\\ & =_\beta & & (\underline{2} (\lambda z. <\!\! A\underline{1} (z\underline{0}), (z\underline{0}) \!\!> ) <\!\!\underline{0}, \underline{0}\!\!> )\underline{1}\\ & = & & ((\underbrace{\lambda sx.\ s(sx)}_{\mbox{\tiny procedura licząca 2}}) (\underbrace{\lambda z. <\!\!A\underline{1}(z\underline{0}), (z\underline{0}) \!\!>}_{\mbox{\tiny następnik}}) \underbrace{<\!\!\underline{0}, \underline{0}\!\!>}_{\mbox{\tiny zero}}) \underline{1}\\ & =_\beta & & ((\lambda z. <\!\! A\underline{1} (z\underline{0}), (z\underline{0}) \!\!> ) [(\lambda z. <\!\! A\underline{1} (z\underline{0}), (z\underline{0}) \!\!> ) <\!\! \underline{0}, \underline{0} \!\!>])\underline{1}\\ & =_\beta & & ((\lambda z. <\!\! A\underline{1} (z\underline{0}), (z\underline{0}) \!\!> ) <\!\! A\underline{1} \underline{0}, \underline{0} \!\!> )\underline{1}\\ & =_\beta & & ((\lambda z. <\!\! A\underline{1} (z\underline{0}), (z\underline{0}) \!\!> ) <\!\! \underline{1}, \underline{0} \!\!> )\underline{1}\\ & =_\beta & & ( <\!\! A\underline{1} \underline{1}, \underline{1}\!\!> ) \underline{1}\\ & =_\beta & & ( <\!\! \underline{2}, \underline{1}\!\!> ) \underline{1}\\ & =_\beta & & \underline{1} \end{align} }

Operator punktu stałego

Podaliśmy tutaj tylko przykłady funkcji reprezentowalnych w rachunku lambda. Okazuje się, że beztypowy rachunek lambda to model obliczeń równoważny funkcjom rekurencyjnym (obliczalnym). Oznacza to, że każdą funkcję obliczalną można reprezentować w rachunku lambda oraz że każdy term rachunku lambda reprezentuje pewną funkcję obliczalną.

Aby móc dowolną funkcję rekurencyjną reprezentować w rachunku lambda, konieczne jest wprowadzenie operatora punktu stałego ${\cal {Y}}$. Operator punktu stałego to term, który dla dowolnego termu $M$ daje jego punkt stały, tzn.

${\cal {Y}}M=_{\beta }M({\cal {Y}}M).$

Zauważmy, że term

${\cal {Y}}=\lambda y.(\lambda x.y(xx))(\lambda x.y(xx))$

jest oczekiwanym operatorem. Zobaczmy, jak term ${\cal {Y}}$ zachowuje się zaaplikowany do dowolnego termu $M$:

Parser nie mógł rozpoznać (nieznana funkcja „\aligned”): {\displaystyle \aligned {\cal Y} M & = & &( \lambda y. (\lambda x. y(xx))(\lambda x. y(xx)))M & & \mbox{~~~~~~| z definicji } {\cal Y} \\ & =_\beta & & (\lambda x. M(xx))\underbrace{(\lambda x. M(xx))}_B & & \mbox{~~~~~~| } y := M\\ & =_\beta & & M(\underbrace{(\lambda x. M(xx))}_B \underbrace{(\lambda x. M(xx))}_B ) & & \mbox{~~~~~~| } x := B\\ & =_\beta & & M( {\cal Y} M ) & & \mbox{~~~~~~| } {\cal Y} M = (\lambda x. M(xx))(\lambda x. M(xx))\\ \end{align} }

Typowany rachunek lambda

Znaczenie typowanego rachunku lambda dla informatyki bierze się z analogii do struktury typów w typowanych językach programowania. W rachunku tym każda zmienna ma przypisany typ, tzn. zakresem jej zmienności jest zbiór opisywany przez ten typ. Typ wyrażenia konstruuje się indukcyjnie z typów jego składowych. Term może być stworzony poprzez aplikację funkcji do argumentu jedynie wtedy, gdy typy funkcji i argumentu są zgodne, tzn. argument należy do dziedziny funkcji.

Rachunek lambda z typami prostymi wprowadzony został przez Churcha i Curry'ego. Jednakże istnieją istotne różnice pomiędzy zaproponowanymi przez nich systemami typów. W systemie Curry'ego termy typowanego rachunku lambda są po prostu wyróżnione spośród termów beztypowego rachunku poprzez relację ustalającą typy. Tak więc term $\lambda x.x$ jest typowalny i należy do wyróżnionego zbioru termów, a term $\lambda x.xx$ typowalny nie jest i do zbioru nie należy. W systemie Churcha reguły nadające typy zostały wbudowane w reguły tworzenia termów. Nie będziemy omawiać żadnego z systemów konkretnie, a jedynie przedstawimy intuicje związane z systemem Churcha nadawania typów.

Zakładamy, że mamy nieskończony, przeliczalny zbiór zmiennych (różnych od zmiennych ze zbioru $Var$). Typ to wyrażenie zdefiniowane indukcyjnie:

• Każda zmienna jest typem, zwanym typem atomowym.

• Jeżeli $\sigma$ i $\tau$ są typami, to $(\sigma \to \tau )$ jest typem, zwanym typem złożonym.

Typy atomowe oznaczamy najczęściej $\alpha$, $\beta$, $\gamma$, a typy ogólnie $\sigma$, $\tau$, ... Nawiasy są często pomijane zgodnie z zasadą łączności prawostronnej, tzn.

$\gamma \to \sigma \to \tau \equiv (\gamma \to (\sigma \to \tau )).$

Fakt, że term $M$ jest typu $\tau$ (ma przypisany typ $\tau$), zapisujemy jako $M\in \tau$ lub poprzez indeks dolny, na przykład $\lambda x.M_{\tau }$. Typ, który nie może zostać przypisany żadnemu termowi, nazywamy typem pustym.

Termom nadajemy typy w następujący sposób:

• Jeżeli term $M$ jest pojedynczą zmienną typu $\tau$, to $M$ jest typu $\tau$, czyli $M\in \tau$.

• Jeżeli term $M=\lambda x:\tau .N:\sigma$, to $M\in (\tau \to \sigma )$. Innymi słowy, jeżeli tworzymy program, który oczekuje na parametr typu $\tau$, a zwraca wynik typu $\sigma$, to całość jest typu $\tau \to \sigma$.

• Jeżeli term $M=PQ$, gdzie $P\in (\tau \to \sigma )$, a $Q\in \tau$, to $M\in \sigma$. Innymi słowy, jeżeli aplikujemy „funkcję” $P$ typu $\tau \to \sigma$ do argumentu $Q$ typu $\tau$, to wynik jest typu $\sigma$.

Pytanie, czy term jest danego typu, jest problemem rozstrzygalnym, tzn. istnieje algorytm, który dla zadanego termu $M$ oraz typu $\tau$ odpowiada, czy $M$ jest typu $\tau .$ Rozstrzygalny jest także problem, czy danemu termowi przypisać można typ zgodnie z zasadami opisanymi powyżej.

Przykład

Parser nie mógł rozpoznać (nieznana funkcja „\aligned”): {\displaystyle \aligned \mbox{\bf Term:} & & \mbox{\bf Typ:}\\ \hline \lambda x : \alpha.x & & \alpha\to \alpha\\ \lambda x : \alpha\to \beta. x & & (\alpha\to \beta)\to (\alpha\to \beta)\\ \lambda x : \alpha. \lambda y : \beta. x & & \alpha\to (\beta\to \alpha)\\ \lambda x : \alpha\to \alpha. \lambda y : \alpha. x & & (\alpha\to \alpha)\to (\alpha\to (\alpha\to \alpha))\\ \lambda x : \alpha. \lambda y : \beta. y & & \alpha\to (\beta\to \beta)\\ \lambda x : \alpha\to \beta. \lambda y : \gamma\to \alpha. \lambda z : \gamma. x(yz) & & (\alpha\to \beta)\to((\gamma\to \alpha)\to (\gamma\to \beta))\\ \lambda x.xx & & \mbox{term nie jest typowalny} \\ \lambda xyz.xy(xz) & & \mbox{term nie jest typowalny} \\ \mbox{typ pusty} & & (\alpha\to \alpha) \to \beta\\ \mbox{typ pusty} & & ((\alpha\to \beta)\to \alpha)\to \alpha \end{align} }

Jeżeli $\tau _{1},\ldots ,\tau _{n},$ $\tau$ są typami, to zapis $\tau _{1},...,\tau _{n}\to \tau$ oznacza typ $\tau _{1}\to (\tau _{2}\to ...\to (\tau _{n}\to \tau )...)$. Zatem każdy typ może być przedstawiony w postaci $\tau _{1},...,\tau _{n}\to \alpha$, gdzie $n\geq 0$, a $\alpha$ jest typem atomowym.