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ę:

$\lambda \underbrace {x_{1}\dots x_{n}} _{\mbox{parametry}}.\underbrace {M} _{\mbox{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

${\begin{aligned}\lambda x.x&=_{\alpha }\lambda y.y\\\lambda x.xz&=_{\alpha }\lambda y.yz\\\lambda x.xy&\neq _{\alpha }\lambda x.xz.\end{aligned}}$

$\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:

${\begin{aligned}\overbrace {(\lambda x.y)(\underbrace {\Delta \Delta } _{(1)})} ^{(2)}&=_{\beta }(\lambda x.y)(\Delta \Delta )=_{\beta }&|{\text{ redukując (1)}}\\&=_{\beta }y&|{\text{ redukując (2)}}\end{aligned}}$

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 $\lambda sx.\ \underbrace {s(s(...(s} _{\mbox{ 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 $\lambda sx.\ \underbrace {s(s(...(s} _{\mbox{ 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

${\begin{aligned}A&=&\lambda mnsx.(ms)(nsx)\end{aligned}}$

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:

${\begin{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}}&&|m:=2\\&=_{\beta }&&\lambda sx.\ ({\underline {2}}s)({\underline {1}}sx)&&|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]&&|t:=s\\&=_{\beta }&&\lambda sx.\ ({\underline {2}}s)(sx)&&|y:=x\\&=&&\lambda sx.\ \{\underbrace {[\lambda t.\ (\lambda y.t(ty))]} _{\mbox{ procedura licząca 2}}s\}\underbrace {(sx)} _{\mbox{ „zero”}}&&|{\mbox{ dopisując nawiasy i }}\lambda \\&=_{\beta }&&\lambda sx.\ (\lambda y.\ s(sy))(sx)&&|t:=s\\&=_{\beta }&&\lambda sx.\ s(s(sx))&&|y:=sx\\&=&&{\underline {3}}\end{aligned}}$

Term

${\begin{aligned}M&=&\lambda mnsx.n(ms)x\end{aligned}}$

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

${\begin{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}}&&|m:=2\\&=_{\beta }&&\lambda sx.\ {\underline {2}}({\underline {2}}s)x&&|n:=2\\&=&&\lambda sx.\ {\underline {2}}[\underbrace {(\lambda t.\ (\lambda y.\ t(ty)))} _{\mbox{ procedura licząca 2}}s]x&&|{\mbox{ dopisując nawiasy i }}\lambda \\&=_{\beta }&&\lambda sx.\ {\underline {2}}[\lambda y.\ s(sy)]x&&|t:=s\\&=&&\lambda sx.\ \underbrace {[\lambda t.\ (\lambda z.t(tz))]} _{\mbox{ procedura licząca 2}}\underbrace {[\lambda y.s(sy)]} _{\mbox{ dodawanie 2}}x&&|{\mbox{ dopisując nawiasy i }}\lambda \\&=_{\beta }&&\lambda sx.\ (\lambda z.\ [\lambda y.s(sy)]([\lambda y.s(sy)]z))x&&|t:=[\lambda y.s(sy)]\\&=_{\beta }&&\lambda sx.\ [\lambda y.s(sy)]([\lambda y.s(sy)]z)&&|z:=x\\&=_{\beta }&&\lambda sx.\ s(s[s(sx)])&&|y:=s(sx)\\&=&&{\underline {4}}\end{aligned}}$

Term

${\begin{aligned}C&=&\lambda mnksx.m(\lambda y.nsx)(ksx)\end{aligned}}$

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

${\begin{aligned}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{aligned}}$

Przykład drugi

${\begin{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} _{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{aligned}}$

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

${\begin{aligned}E&=&\lambda mn.(mn)\end{aligned}}$

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:

${\begin{aligned}E{\underline {2}}\ {\underline {2}}&=&&[\lambda mn.\ (mn)]{\underline {2}}\ {\underline {2}}\\&=_{\beta }&&{\underline {2}}\ {\underline {2}}&&|m:={\underline {2}},\ n:={\underline {2}}\\&=&&\underbrace {[\lambda sx.\ s(sx)]} _{\underline {2}}{\underline {2}}&\\&=_{\beta }&&\lambda x.\ {\underline {2}}({\underline {2}}x)&&|s:={\underline {2}}\\&=_{\alpha }&&\lambda s.\ {\underline {2}}({\underline {2}}s)&&|x:=s\\&=&&\lambda s.[\lambda tx.\ t(tx)]({\underline {2}}s)\\&=_{\beta }&&\lambda sx.\ ({\underline {2}}s)(({\underline {2}}s)x)&&|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))&&|t:=s,\ p:=s,\ z:=x\\&=_{\beta }&&\lambda sx.\ s(s[s(sx)])&&|y:=s(sx)\\&=&&{\underline {4}}\end{aligned}}$

Ciekawym termem jest też term reprezentujący poprzednik:

${\begin{aligned}P&=&\lambda n.(n(\lambda z.<\!\!A{\underline {1}}(z{\underline {0}}),(z{\underline {0}})\!\!>)<\!\!{\underline {0}},{\underline {0}}\!\!>){\underline {1}},\end{aligned}}$

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:

${\begin{aligned}<0,0>&\ \\<1,0>&\ \ \ \ {\mbox{ krok 1}}\\<2,1>&\ \ \ \ {\mbox{ krok 2}}\\...\\<n,n-1>&\ \ \ \ {\mbox{ krok }}n\end{aligned}}$

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:

${\begin{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{ procedura licząca 2}})(\underbrace {\lambda z.<\!\!A{\underline {1}}(z{\underline {0}}),(z{\underline {0}})\!\!>} _{\mbox{ następnik}})\underbrace {<\!\!{\underline {0}},{\underline {0}}\!\!>} _{\mbox{ 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{aligned}}$

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$:

${\begin{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}&&|y:=M\\&=_{\beta }&&M(\underbrace {(\lambda x.M(xx))} _{B}\underbrace {(\lambda x.M(xx))} _{B})&&|x:=B\\&=_{\beta }&&M({\cal {Y}}M)&&|{\cal {Y}}M=(\lambda x.M(xx))(\lambda x.M(xx))\\\end{aligned}}$

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

${\begin{aligned}\mathbf {Term:} &&\mathbf {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{aligned}}$

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.