Tekst źródłowy strony 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&nbsp;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 <math>\Lambda</math> termów
rachunku lambda konstruuje się indukcyjnie jako zbiór słów nad alfabetem
<math>Var \cup \{(,),\lambda\}</math>, gdzie <math>Var</math> jest przeliczalnym zbiorem ziennych.
Do zbioru <math>\Lambda</math> należą tylko termy skonstruowane w poniższy sposób:
* Dowolna zmienna ze zbioru <math>Var</math> jest termem rachunku lambda, czyli jeżeli <math>x\in Var</math>, to <math>x\in\Lambda</math>.

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

* Inna metoda to metoda ''aplikacji'', czyli jeżeli termy <math>M\in\Lambda</math> i <math>N\in\Lambda,</math> to <math>(MN)\in\Lambda</math>.

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

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

''Zbiór zmiennych wolnych'' termu <math>M</math>,
oznaczany przez <math>FV(M)</math>, zdefiniowany jest, w&nbsp;zależności od budowy termu <math>M</math>,
w&nbsp;następujący sposób:

* Jeżeli <math>M</math> jest pojedynczą zmienną, tzn. <math>M\equiv x</math>, to zmienna ta jest wolna, a zatem <math>FV(M) = \{x\}</math>.

* Jeżeli <math>M</math> jest postaci <math>\lambda x.M'</math>, to <math>\lambda x</math> wiąże wszystkie wolne wystąpienia zmiennej <math>x</math> w termie <math>M'</math>, a&nbsp;zatem <math>FV(M) = FV(M')-\{x\}</math>.

* Jeżeli <math>M</math> jest postaci <math>PQ</math>, to zmiennymi wolnymi termu <math>M</math> są wszystkie zmienne wolne występujące w termach <math>P</math> i&nbsp;<math>Q</math>, czyli <math>FV(M) = FV(P)\cup FV(Q).</math>

Zmienna jest ''zmienną wolną'' termu <math>M</math>, jeżeli należy do
zbioru <math>FV(M),</math>
a&nbsp;''zmienną związaną'' w&nbsp;przeciwnym wypadku.

Term <math>M</math> jest ''domknięty'' wtedy i tylko wtedy, gdy <math>FV(M)=\emptyset.</math>

'''Przykład'''

* W&nbsp;termie <math>M = y(\lambda x.x)</math> zmienna <math>y</math> jest zmienną wolną, a <math>x</math> zmienną związaną. W&nbsp;termie <math>\lambda y.M</math> nie ma zmiennych wolnych, jest to więc term domknięty.

* W&nbsp;termie <math>M = x(\lambda x.x)</math> tylko pierwsze wystąpienie zmiennej <math>x</math> jest wolne, chociaż <math>FV(M) = \{x\}</math>. Oczywiście term <math>M</math> nie jest termem domkniętym.

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


<center><math>\lambda \underbrace{x_1... x_n}_{\mbox{\tiny parametry}}.
\underbrace{M}_{\mbox{\tiny ciało procedury}}</math></center>


===Alfa-konwersja i beta-redukcja, czyli obliczanie===

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

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


<center><math>\lambda x. M\rightarrow_\alpha \lambda y. M[x/ y],</math></center>


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

Będziemy używać oznaczenia <math>T_1 =_\alpha T_2</math>, aby powiedzieć, że
termy <math>T_1</math> i&nbsp;<math>T_2</math> są równe modulo <math>\alpha</math>-konwersja, tzn.
że mogą być zredukowane do tego samego
termu dzięki zastosowaniu skończonej liczby <math>\alpha</math>-konwersji.

'''Przykład'''
Niech <math>x</math>, <math>y</math>, <math>z</math> oznaczają różne zmienne. Wówczas


<center><math>\aligned
\lambda x.x & =_\alpha & \lambda y.y\\
\lambda x.xz & =_\alpha & \lambda y.yz\\
\lambda x.xy & \neq_{\alpha} & \lambda x.xz.
\endaligned</math></center>


'''<math>\beta</math>-redukcja''' —
obliczenia wykonywane przez procedurę symulowane są w&nbsp;rachunku lambda
poprzez proces zwany <math>\beta</math>-redukcją. Aplikujemy procedurę
<math>\lambda x. M</math> do argumentu <math>N</math>:


<center><math>(\lambda x. M)N\rightarrow_\beta M[x/N]</math></center>


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


<center><math>(\lambda xy. xy)y \rightarrow \lambda y. yy</math></center>


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


<center><math>(\lambda xy. xy)y =_\alpha (\lambda xz. xz)y =_\beta \lambda z. yz.</math></center>


Używamy oznaczenia <math>T_1 =_\beta T_2</math>, aby powiedzieć, że
termy <math>T_1</math> i&nbsp;<math>T_2</math> są równe modulo <math>\beta</math>-konwersja, tzn.
że mogą być zredukowane do tego samego
termu dzięki zastosowaniu skończonej liczby <math>\beta</math>-konwersji.

Aplikację <math>PQ</math> nazywamy ''<math>\beta</math>-redeksem'', jeżeli term <math>P</math> jest w&nbsp;postaci <math>\lambda</math>-abstrakcji.
Term <math>M</math> jest w&nbsp;''postaci normalnej,'' jeżeli nie
zawiera <math>\beta</math>-redeksów, tzn. żaden podterm termu
<math>M</math> nie jest <math>\beta</math>-redeksem.

===Własność Churcha-Rossera===

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

Jeżeli term <math>M</math> poprzez pewne ciągi <math>\beta</math>-redukcji redukuje się do termów <math>N_1</math> i&nbsp;<math>N_2</math>,
to istnieje term <math>M' </math> taki, że zarówno <math>N_1</math>, jak i&nbsp;<math>N_2</math> można zredukować do <math>M' </math>
(poprzez ciągi <math>\beta</math>-redukcji):


[[Grafika:pp-8-graf.png|Paradygmaty programowania/Moduł8|center]]


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

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


<center><math>\Delta\Delta = (\lambda x.xx)\Delta =_\beta \Delta\Delta.</math></center>


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


<center><math>
\aligned
\overbrace{(\lambda x.y) (\underbrace{\Delta\Delta}_{(1)})}^{(2)}
& =_\beta & (\lambda x.y)(\Delta\Delta) & =_\beta & ... & \mbox{redukując (1)}\\
 & =_\beta & y & & & \mbox{redukując (2)}
\endaligned
</math></center>


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&nbsp;lambda reprezentowalności tych
funkcji. Okazuje się jednak, że w&nbsp;rachunku lambda nie potrzeba
żadnych dodatkowych oznaczeń: pojęcie liczby i&nbsp;funkcji daje się
wprowadzić na bazie do tej pory przyjętych definicji.

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

* Term <math>\lambda sx.\ x</math> reprezentuje liczbę naturalną 0.

* Term <math>\lambda sx.\ \underbrace{s( s( ... (s}_{\mbox{\tiny n razy}}x) ...))</math> reprezentuje liczbę naturalną <math>n</math>.

Term <math>\lambda sx.\ x</math> to po prostu
algorytm: „weź następnik <math>s</math>, weź zero <math>x</math> i&nbsp;zwróć zero”; natomiast term <math>\lambda sx.\ \underbrace{s( s( ... (s}_{\mbox{\tiny n razy}}x) ...))</math> to algorytm:
„weź następnik <math>s</math>, weź zero <math>x</math>, zastosuj <math>n</math>-krotnie następnik do zera i&nbsp;zwróć wynik”.
Zatem liczba naturalna w&nbsp;naszym rozumieniu to procedura, która
ma dwa parametry: <math>s</math> (następnik) oraz <math>x</math> (zero).

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

Mówimy, że ''term <math>E</math> rachunku lambda reprezentuje funkcję'' na
liczbach naturalnych <math>e:\mathbb{N}^k\to \mathbb{N}</math> wtedy
i&nbsp;tylko wtedy, gdy <math>E\underline{n_1}... \underline{n_k} =_{\alpha\beta} \underline{e(n_1, ..., n_k)}</math>, gdzie <math>\underline{n}</math> oznacza reprezentację liczby <math>n</math> w&nbsp;rachunku lambda.


===Operacje na liczbach===

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

Term

<center><math>\aligned
A & = & \lambda mnsx. (ms)(nsx)
\endaligned</math></center>

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


'''Przykład'''
Zobaczmy, jak działa term <math>A</math> na liczbach 1 i 2:
<center><math>\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}
\endaligned</math></center>

Term

<center><math>\aligned
M & = & \lambda mnsx. n(ms)x
\endaligned</math></center>

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

'''Przykład'''
<center><math>\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}
\endaligned</math></center>

Term

<center><math>\aligned
C & = & \lambda mnksx. m(\lambda y.nsx)(ksx)
\endaligned</math></center>

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

'''Przykład'''
Zobaczmy dwa przykłady działania termu <math>C</math> -- pierwszy, gdy
<math>m = 0</math>, oraz drugi, gdy <math>m \neq 0</math>.

Przykład pierwszy
<center><math>\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}
\endaligned</math></center>

Przykład drugi
<center><math>\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 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
\endaligned</math></center>

===Przekazanie funkcji jako parametru===

Musimy częściowo zapomnieć o&nbsp;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, &nbsp;w&nbsp;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


<center><math>\aligned
E & = & \lambda mn. (mn)
\endaligned</math></center>


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


<center><math>
\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}
\endaligned
</math></center>


Ciekawym termem jest też term reprezentujący poprzednik:


<center><math>\aligned
P & = & \lambda n. (n (\lambda z. <\!\! A\underline{1} (z\underline{0}),
(z\underline{0})\!\!>) <\!\!\underline{0}, \underline{0}\!\!>)
\underline{1},
\endaligned</math></center>


gdzie <math>A</math> oznacza wspominany już wcześniej term dodawania, <math>z</math> jest parą uporządkowaną, której pierwsza składowa to <math>z\underline{0}</math>, natomiast druga to <math>z\underline{1}</math>. Jaką procedurę opisuje term <math>P</math>? Mówi on tyle: „weź liczbę naturalną <math>n</math>, a&nbsp;następnie <math>n</math> razy wykonaj algorytm ''weź parę <math>z</math> i&nbsp;utwórz nową parę <math><\!\!1+z0, z0\!\!></math>'', startując od pary <math><\!\!\underline{0}, \underline{0}\!\!></math>; 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:

<center><math>
\aligned
<0, 0> & \mbox{~}\\
<1, 0> & \mbox{~~~~~~krok 1}\\
<2, 1> & \mbox{~~~~~~{krok 2}}\\
... \\
<n, n-1> & \mbox{~~~~~~krok } n
\endaligned
</math></center>


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

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


<center><math>
\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}
\endaligned
</math></center>

===Operator punktu stałego===

Podaliśmy tutaj tylko przykłady funkcji reprezentowalnych w&nbsp;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&nbsp;rachunku lambda
oraz że każdy term rachunku lambda reprezentuje pewną funkcję
obliczalną.

Aby móc dowolną funkcję rekurencyjną reprezentować w&nbsp;rachunku lambda, konieczne jest wprowadzenie ''operatora punktu stałego'' <math>\cal Y</math>. Operator punktu stałego to term, który dla dowolnego termu <math>M</math> daje jego punkt stały, tzn. 


<center><math>{\cal Y}M =_\beta M({\cal Y}M).</math></center>


Zauważmy, że term


<center><math>{\cal Y} = \lambda y. (\lambda x. y(xx))(\lambda x. y(xx))</math></center>


jest oczekiwanym operatorem. Zobaczmy, jak term <math>\cal Y</math> zachowuje
się zaaplikowany do dowolnego termu <math>M</math>:


<center><math>\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))\\
\endaligned
</math></center>

==Typowany rachunek lambda==

Znaczenie typowanego rachunku lambda dla informatyki bierze się
z&nbsp;analogii do struktury typów w&nbsp;typowanych językach programowania.
W&nbsp;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&nbsp;typów jego składowych. Term może być
stworzony poprzez aplikację funkcji do argumentu jedynie wtedy, gdy
typy funkcji i&nbsp;argumentu są zgodne, tzn. argument należy do
dziedziny funkcji.

Rachunek lambda z&nbsp;typami prostymi wprowadzony został przez Churcha
i&nbsp;Curry'ego. Jednakże istnieją istotne różnice pomiędzy
zaproponowanymi przez nich systemami typów. W&nbsp;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 <math>\lambda x.x</math> jest typowalny i&nbsp;należy do wyróżnionego zbioru termów, a&nbsp;term <math>\lambda x.xx</math> typowalny nie jest i&nbsp;do zbioru nie należy. W&nbsp;systemie Churcha reguły nadające typy zostały wbudowane w&nbsp;reguły tworzenia termów. Nie będziemy omawiać żadnego z systemów konkretnie, a jedynie przedstawimy intuicje związane z&nbsp;systemem
Churcha nadawania typów.

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

* Każda zmienna jest typem, zwanym ''typem atomowym.''

* Jeżeli <math>\sigma</math> i&nbsp;<math>\tau</math> są typami, to <math>(\sigma\to \tau)</math> jest typem, zwanym ''typem złożonym.''

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

<center><math>\gamma\to \sigma\to \tau \equiv (\gamma\to (\sigma\to \tau)).</math></center>


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

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

* Jeżeli term <math>M</math> jest pojedynczą zmienną typu <math>\tau</math>, to <math>M</math> jest typu <math>\tau</math>, czyli <math>M\in \tau</math>.

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

* Jeżeli term <math>M = PQ</math>, gdzie <math>P\in (\tau\to \sigma)</math>, a&nbsp;<math>Q\in \tau</math>, to <math>M\in \sigma</math>. Innymi słowy, jeżeli aplikujemy „funkcję” <math>P</math> typu <math>\tau\to \sigma</math> do argumentu <math>Q</math> typu <math>\tau</math>, to wynik jest typu <math>\sigma</math>.

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

'''Przykład'''


<center><math>
\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
\endaligned
</math></center>


Jeżeli <math>\tau_1,\ldots, \tau_n,</math> <math>\tau</math> są  typami, to zapis
<math>\tau_1, ..., \tau_n\to \tau</math> oznacza typ <math>\tau_1\to (\tau_2\to
... \to (\tau_n\to \tau)...)</math>. Zatem każdy typ może być przedstawiony
w&nbsp;postaci <math>\tau_1, ..., \tau_n \to \alpha</math>, gdzie <math>n\ge 0</math>, a&nbsp;<math>\alpha</math>
jest typem atomowym.