ПЛАН КУРСУ

Назва курсу:	Теорія програмування
Викладач:	Проф. Григорій ЖОЛТКЕВИЧ, д.т.н.; email: g.zholtkevych@karazin.ua декан факультету математики і інформатики Харківського національного університету імені В.Н. Каразіна; професор кафедри теоретичної та прикладної інформатики
Короткий опис курсу:	Курс складається з двох частин, що відповідають парадигмам імперативного та функціонального програмування. Тому вступна лекція присвячена поняттю парадигми програмування. У першій частині курсу вивчаються обчислюваність і пов’язані з нею концепції. Презентація цієї частини базується на концепції рекурсивної функції та моделі Unlimited Register Machine (URM). Перше використовується для пояснення поняття денотаційної семантики, тоді як друге використовується для демонстрації поняття операційної семантики. На цій основі показано: зв'язок між операційним і денотаційним підходами до моделювання семантики; існування універсальних програм та їх практичне значення; теореми Райса та Райса-Шапіро; теореми Кліні про фіксовану точку та нормальну форму. Натомість друга частина присвячена функціональному програмуванню. Студенти знайомляться з безтиповим лямбда-численням і відповідною обчислювальною моделлю. Крім того, пояснюється метод симулювання імперативних програм за допомогою безтипового лямбда-числення. Це демонструє обчислювальну еквівалентність імперативної та функціональної парадигм у програмуванні. Продемонстровано функціональні аномалії обчислювального процесу. Таким чином, постає проблема подолання цих аномалій. Для вирішення цієї проблеми пропонується типізація лямбда-термів. Відповідна методика продемонстрована на прикладі простого типізованого лямбда-числення. Також обговорюється відповідність між збагаченим простим лямбда-численням і конструктивною пропозиційною логікою (відповідність Каррі-Говарда). Дорожню карту для збагачення введення лямбда-термінів представлено з використанням лямбда-куба Берендрегта. Наприкінці курсу студенти знайомляться з Coq Proof Assistant – потужним програмним інструментарієм для програмних рішень перевірки.

Зміст курсу

№	Тема	Примітки
G00	Вступ. Концепція парадигми програмування
I01	Примітивно рекурсивні та рекурсивні функції. Розв'язні та нерозв'язні проблнми
I02	Модель Unlimited Register Machine
I03	Any recursive function is computed with URM-program
I04	Gödel numbering of URM-programs. The existing of a non-recursive function
I05	Universal URM-programs and smn-Theorem
I06	Program properties. Their decidability, semidecidability and undecidability
I07	Rice and Rice-Shapiro Theorems
I08	Kleene fixed-point and normal form Theorem
F01	The notion of a function
F02	Typeless lambda calculus: Syntax
F03	Typeless lambda calculus: Equalities
F04	Computing