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

From Studia Informatyczne


Spis treści

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 PQ, czyli FV(M) = FV(P)\cup FV(Q).

Zmienna jest zmienną wolną termu M, jeżeli należy do zbioru FV(M),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... 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_1T_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


\aligned \lambda x.x & =_\alpha \lambda y.y\\ \lambda x.xz & =_\alpha \lambda y.yz\\ \lambda x.xy & \neq_{\alpha} \lambda x.xz. \endaligned


\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_1T_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_1N_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):


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


\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)} \endaligned


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{\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 \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

\aligned A & = & \lambda mnsx. (ms)(nsx) \endaligned

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:

\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

Term

\aligned M & = & \lambda mnsx. n(ms)x \endaligned

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

\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

Term

\aligned C & = & \lambda mnksx. m(\lambda y.nsx)(ksx) \endaligned

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

\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

Przykład drugi

\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 \endaligned

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


\aligned E & = & \lambda mn. (mn) \endaligned


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:


\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


Ciekawym termem jest też term reprezentujący poprzednik:


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


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:

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


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:


\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

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:


\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

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


\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


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\ge 0, a \alpha jest typem atomowym.