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

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania


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 termów rachunku lambda konstruuje się indukcyjnie jako zbiór słów nad alfabetem , gdzie jest przeliczalnym zbiorem ziennych. Do zbioru należą tylko termy skonstruowane w poniższy sposób:

  • Dowolna zmienna ze zbioru jest termem rachunku lambda, czyli jeżeli , to .
  • Jeżeli weźmiemy dowolny term ze zbioru , oraz dowolną zmienną ze zbioru , to term postaci jest termem rachunku lambda, czyli jeżeli i to . Powyższy sposób tworzenia termu nazywamy abstrakcją.
  • Inna metoda to metoda aplikacji, czyli jeżeli termy i to .

Nawiasy są często pomijane według zasady łączności lewostronnej: na przykład Wieloargumentowe funkcje są reprezentowane przez funkcje jednoargumentowe, których argumentami są funkcje. Zatem to, co zwykle jest zapisywane w postaci , w rachunku lambda zapisuje się Powtórzenia symbolu pomijane są według zasady łączności prawostronnej, tzn.

W termie rachunku lambda zmienna może być wolna albo związana. Wolnym wystapieniem zmiennej nazywamy tylko takie wystąpienie tej zmiennej, które nie jest „w zasięgu” żadnego .

Zbiór zmiennych wolnych termu , oznaczany przez , zdefiniowany jest, w zależności od budowy termu , w następujący sposób:

  • Jeżeli jest pojedynczą zmienną, tzn. , to zmienna ta jest wolna, a zatem .
  • Jeżeli jest postaci , to wiąże wszystkie wolne wystąpienia zmiennej w termie , a zatem .
  • Jeżeli jest postaci , to zmiennymi wolnymi termu są wszystkie zmienne wolne występujące w termach , czyli

Zmienna jest zmienną wolną termu , jeżeli należy do zbioru zmienną związaną w przeciwnym wypadku.

Term jest domknięty wtedy i tylko wtedy, gdy

Przykład

  • W termie zmienna jest zmienną wolną, a zmienną związaną. W termie nie ma zmiennych wolnych, jest to więc term domknięty.
  • W termie tylko pierwsze wystąpienie zmiennej jest wolne, chociaż . Oczywiście term 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ę:



Alfa-konwersja i beta-redukcja, czyli obliczanie

Termy rachunku lambda możemy przekształcać, korzystając z -konwersji i -redukcji.

-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 -konwersję, która pozwala zapewnić unikalność nazw.



gdzie , a  oznacza wynik postawienia zmiennej za każde wolne wystąpienie zmiennej w termie .

Będziemy używać oznaczenia , aby powiedzieć, że termy są równe modulo -konwersja, tzn. że mogą być zredukowane do tego samego termu dzięki zastosowaniu skończonej liczby -konwersji.

Przykład Niech , , oznaczają różne zmienne. Wówczas



-redukcja — obliczenia wykonywane przez procedurę symulowane są w rachunku lambda poprzez proces zwany -redukcją. Aplikujemy procedurę do argumentu :



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



jest nieprawidłowym użyciem -konwersji, gdyż dochodzi do konfliktu oznaczeń i do utraty pierwotnego znaczenia termu-procedury. Jednakże można temu zaradzić, stosując -konwersję:



Używamy oznaczenia , aby powiedzieć, że termy są równe modulo -konwersja, tzn. że mogą być zredukowane do tego samego termu dzięki zastosowaniu skończonej liczby -konwersji.

Aplikację nazywamy -redeksem, jeżeli term jest w postaci -abstrakcji. Term jest w postaci normalnej, jeżeli nie zawiera -redeksów, tzn. żaden podterm termu nie jest -redeksem.

Własność Churcha-Rossera

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

Jeżeli term poprzez pewne ciągi -redukcji redukuje się do termów , to istnieje term taki, że zarówno , jak i  można zredukować do (poprzez ciągi -redukcji):


Paradygmaty programowania/Moduł8


Powyższa własność mówi, że postać normalna (o ile istnieje) jest unikalna z dokładnością do -konwersji.

Term 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: . Najprostszym przykładem termu nie posiadającego postaci normalnej jest :



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



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ą jak na procedurę, która -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 reprezentuje liczbę naturalną 0.
  • Term reprezentuje liczbę naturalną .

Term to po prostu algorytm: „weź następnik , weź zero i zwróć zero”; natomiast term to algorytm: „weź następnik , weź zero , zastosuj -krotnie następnik do zera i zwróć wynik”. Zatem liczba naturalna w naszym rozumieniu to procedura, która ma dwa parametry: (następnik) oraz (zero).

Oczywiście powyższe termy podane są z dokładnością do -konwersji. Np. term reprezentuje 2, gdyż .

Mówimy, że term rachunku lambda reprezentuje funkcję na liczbach naturalnych wtedy i tylko wtedy, gdy , gdzie oznacza reprezentację liczby w rachunku lambda.


Operacje na liczbach

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

Term

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


Przykład Zobaczmy, jak działa term na liczbach 1 i 2:

Term

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

Przykład

Term

reprezentuje funkcję . Term oczekuje na podanie trzech argumentów i tak jak w poprzednich przykładach zwraca procedurę obliczającą liczbę naturalną. W przypadku, gdy pierwszy parametr jest zerem, procedura wynikowa liczy liczbę , w przeciwnym przypadku — liczbę .

Przykład Zobaczmy dwa przykłady działania termu -- pierwszy, gdy , oraz drugi, gdy .

Przykład pierwszy

Przykład drugi

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



reprezentuje funkcję i ma pewną „niezwykłą” własność: w wyniku zwraca algorytm, który „zero” jednego z parametrów traktuje jako następnik. Oto przykład:



Ciekawym termem jest też term reprezentujący poprzednik:



gdzie oznacza wspominany już wcześniej term dodawania, jest parą uporządkowaną, której pierwsza składowa to , natomiast druga to . Jaką procedurę opisuje term ? Mówi on tyle: „weź liczbę naturalną , a następnie razy wykonaj algorytm weź parę i utwórz nową parę , startując od pary ; 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:


Zatem term definiuje funkcję , gdzie .

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


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 daje jego punkt stały, tzn.



Zauważmy, że term



jest oczekiwanym operatorem. Zobaczmy, jak term zachowuje się zaaplikowany do dowolnego termu :


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 jest typowalny i należy do wyróżnionego zbioru termów, a term 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 ). Typ to wyrażenie zdefiniowane indukcyjnie:

  • Każda zmienna jest typem, zwanym typem atomowym.
  • Jeżeli są typami, to jest typem, zwanym typem złożonym.

Typy atomowe oznaczamy najczęściej , , , a typy ogólnie , , ... Nawiasy są często pomijane zgodnie z zasadą łączności prawostronnej, tzn.


Fakt, że term jest typu (ma przypisany typ ), zapisujemy jako lub poprzez indeks dolny, na przykład . 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 jest pojedynczą zmienną typu , to jest typu , czyli .
  • Jeżeli term , to . Innymi słowy, jeżeli tworzymy program, który oczekuje na parametr typu , a zwraca wynik typu , to całość jest typu .
  • Jeżeli term , gdzie , a , to . Innymi słowy, jeżeli aplikujemy „funkcję” typu do argumentu typu , to wynik jest typu .

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

Przykład



Jeżeli są typami, to zapis oznacza typ . Zatem każdy typ może być przedstawiony w postaci , gdzie , a  jest typem atomowym.