2-INF-264 Teória deklaratívneho programovania

Novinky

O kurze

Tu nájdete informačný list predmetu.

Cieľ predmetu

Študent sa zoznámi s matematickými základmi deklaratívnych programovacích jazykov.

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. Substitúcia 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. Operátor minimalizácie. 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-505 Úvod do deklaratívneho programovania
• 1-INF-465 Deklaratívne programovanie
• 1-AIN-470 Špecifikácia a verifikácia programov

Nadväzujúce predmety

Výučba

• Zimný semester ak.r. 2015/16