Wydział MIM UW - Zastosowania rachunku

Next: Wyprowadzanie typów Up: Autoreferat pracy doktorskiej pt. Previous: Rachunek

Zastosowania rachunku $\lambda$

Rachunek $\lambda$ od momentu swego powstania w latach trzydziestych stanowił podstawę dla różnego rodzaju języków formalnych -- i to tak w dziedzinie szeroko rozumianej logiki jak i teorii obliczeń wraz ze ściśle z nią związanymi językami programowania. Początkowo miał on służyć za podstawy matematyki, jednak pewne niepowodzenia w tym zakresie spowodowały, że bardziej zaznaczył on swoją obecność w teorii obliczeń. Po wielu latach z tego właśnie nurtu wyrosły funkcyjne języki programowania, do których należą m.in. LISP oraz ML. Nurt logiczny w dziedzinie rachunku $\lambda$ miał bardzo silny wpływ na tworzenie matematyki konstruktywistycznej (określanej także mianem intuicjonistycznej), której istotę można zwięźle streścić hasłem: ,,jeśli pokazujesz, że coś istnieje, to pokaż to coś''. Z punktu widzenia zastosowania w informatyce nurt ten zaowocował powstaniem różnego rodzaju sytemów automatycznego lub półautomatycznego dowodzenia twierdzeń m.in. LEGO, Coq, Alf i inne.

Szczególną rolę w zastosowaniach grają rachunki $\lambda$ z typami będące w ścisłym związku z pierwotnym -- beztypowym rachunkiem lambda. Języki programowania wywodzące się z ML-a (SML, Caml, Haskell, Miranda i inne) oparte są właśnie na pewnym rachunku $\lambda$ z typami. Rachunek ten posiada istotną cechę zwaną polimorfizmem. Polimorfizm odznacza się możliwością deklarowania operacji, które potem mogą być wykonywane dla wielu typów danych. Klasycznym przykładem tego typu operacji jest operacja wykonania odwzorowania na wszystkich elementach listy i utworzenia drugiej listy wyników wykonania tej operacji. W klasycznych językach programowania takich jak Pascal czy C operacja taka wymagałaby oddzielnej procedury dla list liczb naturalnych i oddzielnej dla liczb rzeczywistych. W językach korzystających z dobrodziejstw polimorfizmu dla wszystkich typów, w tym dla liczb naturalnych i rzeczywistych, pisze się jeden taki operator.

Podobnie wymienione systemy dowodzenia twierdzeń LEGO, Coq, Alf są oparte na różnych, bardzo silnych rachunkach $\lambda$ z typami. Rachunki te działają na zasadzie izomorfizmu Curry'ego-Howarda, który mówi, że dla danej logiki intuicjonistycznej mamy do dyspozycji odpowiedni rachunek $\lambda$ z typami, taki że dowody w tej logice (przedstawionej w systemie naturalnej dedukcji) są we wzajemnie jednoznacznej odpowiedniości z termami owego rachunku $\lambda$ . W związku z tym o formule można myśleć jak o typie, a o budowaniu dowodu -- jak o budowaniu $\lambda$ -termu mającego ten typ.

Next: Wyprowadzanie typów Up: Autoreferat pracy doktorskiej pt. Previous: Rachunek

Aleksy Schubert 2001-03-15