1-AIN-625 Úvod do matematickej logiky pre programátorov

Novinky

O kurze

Tu nájdete informačný list predmetu.

Cieľ predmetu

Vybudovať matematické základy deklaratívnych programovacích jazykov. Programy sú definície rekurzívnych funkcií. Výpočtový model je založený na redukcií termov. Dátové štruktúry sa kódujú do prirodzených čísel. Problémy sa riešia na cvičeniach v programovacom jazyku CL.

Stručná osnova predmetu

Primitívne rekurzívne funkcie. Základné funkcie a operácie (kompozícia funkcií, primitívna rekurzia). Explicitné definície. Ohraničená minimalizácia. Párovacia funkcia a aritmetizácia. Spätná rekurzia. Rekurzia so substitúciou v parametri. Vnorená jednoduchá rekurzia. Rekurzia s mierou. Regulárne rekurzívne definície.

Obecne rekurzívne funkcie. Poza primitívnu rekurziu: Ackermann-Péterovej funkcia, univerzálna funkcia pre primitívne rekurzívne funkcie. Primitívne rekurzívne indexy. Transfinitná rekurzia. Obecne rekurzívne funkcie. Regulárna minimalizácia. μ-Rekurzívne funkcie.

Čiastočne rekurzívne funkcie. Prvá veta o rekurzii (veta o pevnom bode). Výpočtový model. Ekvivalentnosť operačnej a denotačnej sémantiky. Čiastočne rekurzívne funkcie. Neohraničená minimalizácia. Aritmetizácia výpočtového modelu. Kleeneho veta o normálnej forme. Univerzálna funkcia. Rekurzívne indexy. Veta o enumerácií. Čiastočne μ-rekurzívne funkcie. Rekurzívne rozhodnuteľné, polorozhodnuteľné a nerozhodnuteľné problémy. Churchova téza.

Literatúra

J. Komara. Recursive Functions. Downloadable lecture notes available through the web page of the course.
J. Komara and P. J. Voda. Lecture Notes in Theory of Computability. 2001. (PostScript) (Adobe Acrobat Document)
J. Komara and P. J. Voda. Metamathematics of Computer Programming. 2001. (PostScript) (Adobe Acrobat Document)
I. Korec. Úvod do teórie algoritmov. Skriptá MFF UK, 1981.

Podmieňujúce predmety

Doporučené:

1-AIN-506 Úvod do deklaratívneho programovania

Výučba

* – aktualizované v priebehu posledných 7 dní

Posledná zmena: 2015-09-17T15:12+0200