Tugev dinaturaalsus ja initsiaalalgebrad

Tarmo Uustalu

Dept. of Informatics
University of Minho

Neljapäev, 01.02.2001, kell 14.45
Liivi 2, ruum 208


Ülevaade: Eeljärjestuste ja monotoonsete funktsioonide jaoks teame kaht Tarskile omistatavat püsipunktiteoreemi, millest üks, nn konstruktiivne omab väga otsest ja hästituntud üldistust kategooriate ja funktorite jaoks. Teise, nn mittekonstruktiivset teoreemi kohta aga kiputakse uskuma, et see samavõrd loomulikult ei üldistu. Ettekandes näitame, et niisugune arvamus on ekslik; teoreemi otsene üldistus on lihtsalt konstrueeritav, kui valikuline infiimum üldistada ebatraditsiooniliselt kasutades tugeva dinaturaalsuse mõistet. Programmeerimise jaoks tähendab see, et nn in-cata ja cata-build lähenemised induktiivsetele tüüpidele on ekvivalentsed.


Varmo Vene
Viimati muudetud 30.01.2001