#import "template.lib.typ": *
#show: formatting
#set page(background: image("pictures/troubles-faded.jpg", width: 100%, height: 100%, fit: "stretch"))

#head([ Программа курса ])

+ Определение множества л-выражений. Сокращённая нотация. Свободные и связанные переменные. Совместимость отношения с операциями. ал-конгруэнтность.
+ Корректные л-выражения. Если $M$ корректно, то $BV(M) union.sq FV(M) = TV(M)$. Всякое л-выражение ал-конгруэнтно корректному. Правило переменных.
+ Определение оператора подстановки. Оператор подстановки уважает ал-конгруэнтность. Лемма о подстановке.
+ Определение бэ-конверсии. Теорема о неподвижной точке. Оператор подстановки уважает конверсию.
+ Определение комбинатора. Стандартные комбинаторы. Комбинатор фиксированной точки. Терминология л-теории (равенства, замкнутость, согласованность, противоречивость, несовместимость). $#I$ несовместимо с $#K$.
+ Определение редукции (отношения $(->)$, $(->>)$, $(=)$ с вариантами (б-), (эт-), (бэ-)). Редексы. Нормальные формы. Редукционный путь. Нормальная форма ни к чему не редуцируется. Определение редукционного графа. Свойство Чёрча-Россера.
+ Теорема о минимальном элементе. $CR(rel) ==> CR(Trans(rel))$.
+ Оператор подстановки уважает "рефлексивную б-редукцию" $arr$ (лемма 1.6.2.).
+ $arr$ удовлетворяет свойству Чёрча-Россера.
+ $->_beta$ --- это транзитивное замыкание $arr$. Теорема Чёрча-Россера для $->>_beta$. Следствия.
+ Диаграммы бинарных отношений. Коммутирующие отношения. Лемма Хиндли-Росена.
+ Если для $rel1$, $rel2$ выполняется определённая диаграмма, то $Preord(rel1)$ и $Preord(rel2)$ коммутируют.
+ $->>_eta$ удовлетворяет свойству Чёрча-Россера.
+ $->>_beta$ и $->>_eta$ коммутируют.
+ Оператор подстановки уважает отношение $Refl(->_eta)$. Теорема Чёрча-Россера для $->>_(beta eta)$. Следствия.
+ Внешние/внутренние редексы/нормальные формы. Разбиение редукции на внешнюю и внутреннюю.
+ Стандартный редукционный путь. Для любой редукции $M ->> N$ существует стандартная редукция $M ->>_s N$.
+ Нормализующая редукционная стратегия. Определение крайней левой стратегии $F_l$. $F_l$ --- нормализующая.
+ Комбинаторы $#T$ и $#F$. Упорядоченные пары. Конечные кортежи (+проекции). Обобщённая теорема о неподвижной точке.
+ Числа Барендрегта (л-числа). Определение класса рекурсивных функций (суперпозиция, примитивная рекурсия, минимизация). л-представимость.
+ Все рекурсивные функции л-представимы.
+ Все л-представимые функции рекурсивны (эскиз доказательства). Кодирование, функция комбинации, функция нумерации.
+ Числа Чёрча. Функции перехода от чисел Барендрегта к числам Чёрча и обратно. Функция $phi : NN_0^p -> NN_0$ рекурсивна $<==>$ $phi$ л-представима с помощью чисел Чёрча.
+ л-выражения $#Ap$, $#Am$ и $#Ae$ л-представляют сложение, умножение и возведение в степень на числах Чёрча.
+ Числовые системы. Критерий адекватности числовой системы.
+ Рекурсивно сепарабельные и рекурсивные множества. Множества, замкнутые относительно конверсии.
+ Теорема Скотта-Карри о неразрешимости. Следствия.
