1-AIN-625 Introduction to Mathematical Logic for Programmers

News

Info

Here you will find the course information sheet.

Goal

Syllabus

Primitive Recursive Functions. Basic functions and operations (composition of functions and primitive recursion). Explicit definitions. Bounded minimalization. Pairing function and arithmetization. Backward recursion. Recursion with substitution in parameters. Nested simple recursion. Recursion with measure. Regular recursive definitions.

General Recursive Functions. Beyond primitive recursion: Ackermann-Péter function, universal function for primitive recursive functions. Primitive recursive indices. Transfinite recursion. General recursive functions. Regular minimalization. μ-Recursive functions.

Partial Recursive Functions. First recursion theorem (fixed point theorem). Computation model. Equivalence of the operational and denotational semantics. Partial recursive functions. Unbounded minimalization. Arithmetization of computation. Kleene normal-form theorem. Universal function. Recursive indices. Enumeration theorem. Partial μ-recursive functions. Recursively undecidable problems. Recursively decidable, semidecidable and undecidable problems. Church thesis.

Literature

• 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.

Prerequisities

Recommended:

• 1-AIN-506 Introduction to Declarative Programming

Semesters

• Winter 2007/08
• Winter 2008/09
• Winter 2009/10
• Winter 2010/11
• Winter 2011/12
• Winter 2012/13
• Winter 2013/14
• Winter 2014/15