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 $M$ jest domknięty wtedy i tylko wtedy, gdy $FV(M)=\emptyset .$

Przykład

• W termie $M=y(\lambda x.x)$ zmienna $y$ jest zmienną wolną, a $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ć (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 \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ć (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 \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ć (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 \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ć (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 \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ć (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 \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ć (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 \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ć (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 \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ć (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 \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ć (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 \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ć (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 \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ć (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 \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ć (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 \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ć (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 \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ć (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 \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ć (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 \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ć (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 \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ć (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 \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ć (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 \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ć (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 \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.