Uniwersytet Warszawski University of Warsaw
Menu
Wyszukiwarka
 W bieżącym katalogu
next up previous
Next: Uzyskane wyniki Up: Autoreferat pracy doktorskiej pt. Previous: Rachunki a unifikacja

Uzyskane wyniki -- wyprowadzanie typów

W rozprawie doktorskiej przedstawiony zosta³ dowód nierozstrzygalno¶ci problemu wyprowadzania typów dla polimorficznego rachunku $\lambda$ w wersji z jawnymi adnotacjami typowymi. Oznacza to, ¿e przy stosowaniu jêzyków opartych na tym systemie nie mo¿na liczyæ na w pe³ni rozdzieln± kompilacjê. Z drugiej strony pokazany zosta³ dowód rozstrzygalno¶ci problemu kontekstowego wyprowadzania typów dla zanurzenia logiki 1. rzêdu w $\lambda P$ (w wersji bez jawnych adnotacji typowych), co oznacza, ¿e mo¿na przedstawiæ jêzyk programowania z typami monomorficznymi, w którym mo¿liwe jest u¿ywanie typów bêd±cych formu³ami pierwszego rzêdu. Rozwa¿ania dotycz±ce rozstrzygalno¶ci zosta³y wzbogacone o adaptacjê znanej wcze¶niej konstrukcji G. Doweka, która dowodzi, ¿e dla niewielkiego rozszerzenia jêzyka typów -- mo¿liwe jest kwantyfikowanie po symbolach funkcyjnych -- kontekstowe wyprowadzanie staje siê nierozstrzygalne.


Aleksy Schubert 2001-03-15