Andrej Bauer: Na prvi pogled nemogoči funkcionali

Predavatelj: Andrej Bauer

Povzetek:
Naj bo C = int -> {0,1} Cantorjev prostor vseh neskončnih zaporedij ničel in enic. Predikat na C je funkcija p : C -> {0,1}. Ali lahko za izračunljive p na izračunljiv način ugotovimo, ali obstaja zaporedje a, za katerega je p(a) = 1? Na prvi pogled se to zdi nemogoče, saj iščemo a iz neskončne domene C.

Na seminarju bom predstavil funkcional, ki za dani predikat p poišče neskončno zaporedje a, za katero velja p(a) = 1. Če tako zaporedje ne obstaja, funkcional to ugotovi in vrne rezultat "ne obstaja". Pojasnil bom, zakaj funkcional deluje in kako je to povezano s topološkimi lastnostmi Cantorjevega prostora. Predstavitev bo povzeta po članku Martina Escardoja Seemingly impossible functional programs.