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 $\mathrm{\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 $\mathrm{\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 \mathrm{\Lambda }$.

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

• Inna metoda to metoda aplikacji, czyli jeżeli termy $M\in \mathrm{\Lambda }$ i $N\in \mathrm{\Lambda }$, to $(MN)\in \mathrm{\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^{\prime }$, to $\lambda x$ wiąże wszystkie wolne wystąpienia zmiennej $x$ w termie $M^{\prime }$, a zatem $FV(M)=FV(M^{\prime })-\{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)=\mathrm{\varnothing }$.

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 \underset{\text{parametry}}{\underbrace{x_1\dots x_n}}.\underset{\text{ciało procedury}}{\underbrace{M}}$

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{\to }_{\alpha }\lambda y.M[x/y]$,

gdzie $y\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{array}{rl}\lambda x.x& {=}_{\alpha }\lambda y.y\\ \lambda x.xz& {=}_{\alpha }\lambda y.yz\\ \lambda x.xy& {\ne }_{\alpha }\lambda x.xz.\end{array}$

$\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{\to }_{\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\to \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^{\prime }$ taki, że zarówno $N_1$, jak i $N_2$ można zredukować do $M^{\prime }$ (poprzez ciągi $\beta$-redukcji):

Paradygmaty programowania/Moduł8

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: $\mathrm{\Delta }=\lambda x.xx$. Najprostszym przykładem termu nie posiadającego postaci normalnej jest $\mathrm{\Delta }\mathrm{\Delta }$:

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

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

$\begin{array}{rlr}\stackrel{(2)}{\overbrace{(\lambda x.y)(\underset{(1)}{\underbrace{\mathrm{\Delta }\mathrm{\Delta }}})}}& {=}_{\beta }(\lambda x.y)(\mathrm{\Delta }\mathrm{\Delta }){=}_{\beta }& |\text{ redukując (1)}\\ & {=}_{\beta }y& |\text{ redukując (2)}\end{array}$

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.\underset{\text{ n razy}}{\underbrace{s(s(...(s}}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.\underset{\text{ n razy}}{\underbrace{s(s(...(s}}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{\mathbb{N}}}^k\to \mathbb{\mathbb{N}}$ wtedy i tylko wtedy, gdy $E\underset{\_}{n_1}...\underset{\_}{n_k}{=}_{\alpha \beta }\underset{\_}{e(n_1,...,n_k)}$, gdzie $\underset{\_}{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{array}{rlr}A& =& \lambda mnsx.(ms)(nsx)\end{array}$

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{array}{rlrlrl}A\underset{\_}{1}\underset{\_}{2}& =& & \{[\lambda m.(\lambda n.(\lambda sx.(ms)(nsx))]\underset{\_}{1}\}\underset{\_}{2}& & |\text{dopisując nawiasy i }\lambda \\ & {=}_{\beta }& & [\lambda n.(\lambda sx.(\underset{\_}{2}s)(nsx)]\underset{\_}{1}& & |m:=2\\ & {=}_{\beta }& & \lambda sx.(\underset{\_}{2}s)(\underset{\_}{1}sx)& & |n:=1\\ & =& & \lambda sx.(\underset{\_}{2}s)\{[(\lambda t.(\lambda y.ty))s]x\}& & |\text{ dopisując nawiasy i }\lambda \\ & {=}_{\beta }& & \lambda sx.(\underset{\_}{2}s)[(\lambda y.sy)x]& & |t:=s\\ & {=}_{\beta }& & \lambda sx.(\underset{\_}{2}s)(sx)& & |y:=x\\ & =& & \lambda sx.\{\underset{\text{ procedura licząca 2}}{\underbrace{[\lambda t.(\lambda y.t(ty))]}}s\}\underset{\text{ „zero”}}{\underbrace{(sx)}}& & |\text{ dopisując nawiasy i }\lambda \\ & {=}_{\beta }& & \lambda sx.(\lambda y.s(sy))(sx)& & |t:=s\\ & {=}_{\beta }& & \lambda sx.s(s(sx))& & |y:=sx\\ & =& & \underset{\_}{3}\end{array}$

Term

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

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

Term

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

reprezentuje funkcję $i{f}_{-}the{n}_{-}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\ne 0$.

Przykład pierwszy

$\begin{array}{rlrl}C\underset{\_}{0}\underset{\_}{n}\underset{\_}{k}& {=}_{\beta }& & \lambda sx.\underset{\_}{0}(\lambda y.\underset{\_}{n}sx)(\underset{\_}{k}sx)\\ & =& & \lambda sx.\underset{\underset{\_}{0}}{\underbrace{(\lambda tz.z)}}(\lambda y.\underset{\_}{n}sx)(\underset{\_}{k}sx)\\ & {=}_{\beta }& & \lambda sx.\underset{\_}{k}sx\\ & {=}_{\beta }& & \underset{\_}{k}\end{array}$

Przykład drugi

$\begin{array}{rlrl}C\underset{\_}{m}\underset{\_}{n}\underset{\_}{k}& {=}_{\beta }& & \lambda sx.\underset{\_}{m}(\lambda y.\underset{\_}{n}sx)(\underset{\_}{k}sx)\\ & =& & \lambda sx.[\lambda tz.\underset{m\ne 0\text{ razy}}{\underbrace{t(...(t}}y)...)](\lambda y.\underset{\_}{n}sx)(\underset{\_}{k}sx)\\ & {=}_{\beta }& & \lambda sx.[\lambda y.\underset{\_}{n}sx](...([\lambda y.\underset{\_}{n}sx](\underset{\_}{k}sx))...)\\ & {=}_{\beta }& & \lambda sx.\underset{\_}{n}sx\end{array}$

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{array}{rlr}E& =& \lambda mn.(mn)\end{array}$

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{array}{rlrl}E\underset{\_}{2}\underset{\_}{2}& =& & [\lambda mn.(mn)]\underset{\_}{2}\underset{\_}{2}\\ & {=}_{\beta }& & \underset{\_}{2}\underset{\_}{2}& & |m:=\underset{\_}{2},n:=\underset{\_}{2}\\ & =& & \underset{\underset{\_}{2}}{\underbrace{[\lambda sx.s(sx)]}}\underset{\_}{2}& \\ & {=}_{\beta }& & \lambda x.\underset{\_}{2}(\underset{\_}{2}x)& & |s:=\underset{\_}{2}\\ & {=}_{\alpha }& & \lambda s.\underset{\_}{2}(\underset{\_}{2}s)& & |x:=s\\ & =& & \lambda s.[\lambda tx.t(tx)](\underset{\_}{2}s)\\ & {=}_{\beta }& & \lambda sx.(\underset{\_}{2}s)((\underset{\_}{2}s)x)& & |t:=\underset{\_}{2}s\\ & =& & \lambda sx.(\underset{\underset{\_}{2}}{\underbrace{[\lambda ty.t(ty)]}}s)((\underset{\underset{\_}{2}}{\underbrace{[\lambda pz.p(pz)]}}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)\\ & =& & \underset{\_}{4}\end{array}$

Ciekawym termem jest też term reprezentujący poprzednik:

$\begin{array}{rlr}P& =& \lambda n.(n(\lambda z.<A\underset{\_}{1}(z\underset{\_}{0}),(z\underset{\_}{0})>)<\underset{\_}{0},\underset{\_}{0}>)\underset{\_}{1},\end{array}$

gdzie $A$ oznacza wspominany już wcześniej term dodawania, $z$ jest parą uporządkowaną, której pierwsza składowa to $z\underset{\_}{0}$, natomiast druga to $z\underset{\_}{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 $<\underset{\_}{0},\underset{\_}{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{array}{rl}<0,0>& \\ <1,0>& \text{ krok 1}\\ <2,1>& \text{ krok 2}\\ ...\\ <n,n-1>& \text{ krok }n\end{array}$

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{array}{rlrl}P\underset{\_}{2}& =& & \{\lambda n.(n(\lambda z.<A\underset{\_}{1}(z\underset{\_}{0}),(z\underset{\_}{0})>)<\underset{\_}{0},\underset{\_}{0}>)\underset{\_}{1}\}\underset{\_}{2}\\ & {=}_{\beta }& & (\underset{\_}{2}(\lambda z.<A\underset{\_}{1}(z\underset{\_}{0}),(z\underset{\_}{0})>)<\underset{\_}{0},\underset{\_}{0}>)\underset{\_}{1}\\ & =& & ((\underset{\text{ procedura licząca 2}}{\underbrace{\lambda sx.s(sx)}})(\underset{\text{ następnik}}{\underbrace{\lambda z.<A\underset{\_}{1}(z\underset{\_}{0}),(z\underset{\_}{0})>}})\underset{\text{ zero}}{\underbrace{<\underset{\_}{0},\underset{\_}{0}>}})\underset{\_}{1}\\ & {=}_{\beta }& & ((\lambda z.<A\underset{\_}{1}(z\underset{\_}{0}),(z\underset{\_}{0})>)[(\lambda z.<A\underset{\_}{1}(z\underset{\_}{0}),(z\underset{\_}{0})>)<\underset{\_}{0},\underset{\_}{0}>])\underset{\_}{1}\\ & {=}_{\beta }& & ((\lambda z.<A\underset{\_}{1}(z\underset{\_}{0}),(z\underset{\_}{0})>)<A\underset{\_}{1}\underset{\_}{0},\underset{\_}{0}>)\underset{\_}{1}\\ & {=}_{\beta }& & ((\lambda z.<A\underset{\_}{1}(z\underset{\_}{0}),(z\underset{\_}{0})>)<\underset{\_}{1},\underset{\_}{0}>)\underset{\_}{1}\\ & {=}_{\beta }& & (<A\underset{\_}{1}\underset{\_}{1},\underset{\_}{1}>)\underset{\_}{1}\\ & {=}_{\beta }& & (<\underset{\_}{2},\underset{\_}{1}>)\underset{\_}{1}\\ & {=}_{\beta }& & \underset{\_}{1}\end{array}$

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 ${𝒴}$. Operator punktu stałego to term, który dla dowolnego termu $M$ daje jego punkt stały, tzn.

${𝒴}M{=}_{\beta }M({𝒴}M)$.

Zauważmy, że term

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

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

$\begin{array}{rlrlrl}{𝒴}M& =& & (\lambda y.(\lambda x.y(xx))(\lambda x.y(xx)))M& & |\text{ z definicji }{𝒴}\\ & {=}_{\beta }& & (\lambda x.M(xx))\underset{B}{\underbrace{(\lambda x.M(xx))}}& & |y:=M\\ & {=}_{\beta }& & M(\underset{B}{\underbrace{(\lambda x.M(xx))}}\underset{B}{\underbrace{(\lambda x.M(xx))}})& & |x:=B\\ & {=}_{\beta }& & M({𝒴}M)& & |{𝒴}M=(\lambda x.M(xx))(\lambda x.M(xx))\\ \end{array}$

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{array}{rlr}\mathbf{𝐓}\mathbf{𝐞}\mathbf{𝐫}\mathbf{𝐦}\mathbf{:}& & \mathbf{𝐓}\mathbf{𝐲}\mathbf{𝐩}\mathbf{:}\\ HLINE\; TBD\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& & \text{term nie jest typowalny}\\ \lambda xyz.xy(xz)& & \text{term nie jest typowalny}\\ \text{typ pusty}& & (\alpha \to \alpha )\to \beta \\ \text{typ pusty}& & ((\alpha \to \beta )\to \alpha )\to \alpha \end{array}$

Jeżeli ${\tau }_1,\dots ,{\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\ge 0$, a $\alpha$ jest typem atomowym.