Next: Uzyskane wyniki Up: Autoreferat pracy doktorskiej pt. Previous: Unifikacja
Rachunki 
a unifikacja
Algorytmy wyprowadzania typów dla rachunków z typami zwykle
wykorzystują taką własność wyprowadzania, że na podstawie
wyprowadzenia dla podtermów można skonstruować wyprowadzenie dla termu
z nich złożonego. Jednak pojawia się tutaj taki problem, że typy
podtermów muszą się ze sobą w odpowiedni sposób zgadzać. Ten mechanizm
powoduje, że nierzadko w algorytmach wyprowadzenia typów znajduje
zastosowanie unifikacja. Ma to miejsce na przykład w systemie typów
dla rachunku z typami prostymi oraz w popularnym
systemie typów Milnera używanym w funkcyjnych językach
programowania. We wspomnianych systemach zastosowanie znalazła
unifikacja pierwszego rzędu. Pojawia się tutaj oczywiste pytanie, jaką
rolę gra w wyprowadzaniu typów unifikacja wyższego rzędu,
w szczególności unifikacja rzędu drugiego.
Aleksy Schubert 2001-03-15