Uniwersytet Warszawski University of Warsaw
Menu
Wyszukiwarka
 W bieżącym katalogu
next up previous
Next: Zastosowania rachunku Up: Autoreferat pracy doktorskiej pt. Previous: Autoreferat pracy doktorskiej pt.

Rachunek $\lambda$

Rachunek $\lambda$ powstał na początku lat trzydziestych. Jest to język formalny pozwalający na budowanie różnego rodzaju operatorów oraz na stosowanie tych operatorów do wszelkich obiektów wyrażalnych w tym rachunku. Mamy zatem tutaj możliwość wprowadzania obiektów (zmiennych) np. $x, y, z$ itp. Mamy możliwość tworzenia z jednego operatora lub obiektu (np. $M$) operatora (w tym wypadku $\lambda x.M$ -- nazywanego lambda abstrakcją) oraz mamy możliwość użycia (zaaplikowania) operatora do obiektu (jeśli operatorem jest $M$, a obiektem $N$, to zastosowanie operatora do obiektu zapisujemy jako $MN$). Do tego dodana jest operacja $\beta$-redukcji, która pozwala określić wynik wykonania operacji na obiekcie. Taki system pozwala na symulowanie dowolnych obliczeń maszyny Turinga, w związku z czym ma on szerokie zastosowanie w informatyce.

Powyższy formalizm został uzupełniony o pojęcie typu. Typ operatora czy obiektu informuje, jaką własność posiada dany operator (obiekt). Najprostszym przykładem takiej własności jest własność postaci $\alpha\to\alpha$, która informuje, że jeśli operator dostanie element typu $\alpha$, to da w wyniku element tego samego typu. Wprowadzono wiele tego rodzaju formalizmów typowych. Tutaj będziemy się interesowali rachunkiem $\lambda$ z typami prostymi, polimorficznym rachunkiem $\lambda$ oraz rachunkiem typów zależnych ($\lambda P$).

Rachunek $\lambda$ z typami prostymi pozwala na wyrażanie informacji o operatorach w rodzaju: jeśli operator weźmie argumenty wskazanych typów wejściowych, to da wynik typu wyjściowego, przy czym same typy bazowe mają tylko postać nie mających struktury atomów. Polimorficzny rachunek $\lambda$ pozwala na wyrażanie informacji o tym, że dany pojedynczy operator może przyjmować argumenty wielu typów, o ile tylko ich ogólny schemat odpowiada temu, co jest zapisane w argumencie operatora. Wreszcie rachunek typów zależnych pozwala na wyrażanie informacji bardziej szczegółowych na temat argumentów i wyników. Można tutaj wyrażać własności wyrażalne w logice pierwszego rzędu.

Warto może jeszcze nadmienić, że rachunki $\lambda$ z typami występują w dwóch odmianach: z jawnymi adnotacjami typowymi (tzw. rachunek $\lambda$ w wersji Churcha) oraz bez adnotacji typowych (tzw. rachunek $\lambda$ w wersji Curry'ego).

next up previous
Next: Zastosowania rachunku Up: Autoreferat pracy doktorskiej pt. Previous: Autoreferat pracy doktorskiej pt.
Aleksy Schubert 2001-03-15