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

Uzyskane wyniki -- unifikacja

W dziedzinie unifikacji wyższego rzędu przedstawiony został zupełnie nowy dowód nierozstrzygalności problemu unifikacji drugiego rzędu. Uzyskany dowód nie odwołuje się do 10. problemu Hilberta, co stanowi istotne koncepcyjne uproszczenie znanego dowodu unifikacji 2. rzędu. Dowód ten jednocześnie działa dla ciekawego podproblemu unifikacji drugiego rzędu -- problemu unifikacji z prostymi instancjami, gdzie w argumentach niewiadomych mogą występować tylko termy bez niewiadomych. Dzięki temu ograniczeniu możliwe było udowodnienie nierozstrzygalności wyprowadzania typów dla polimorficznego rachunku $\lambda$ w wersji z jawnymi adnotacjami typowymi. Przy okazji dowodu nierozstrzygalności unifikacji zostały przedstawione ciekawe związki między unifikacją a przepisywaniem termów.

Dodatkowo pokazany został ciekawy rozstrzygalny podproblem unifikacji drugiego rzędu -- unifikację ze zmiennymi w pozycjach czołowych. W unifkacji tej niewiadome mogą występować tylko na początku termu.


Aleksy Schubert 2001-03-15