Видеокурс "Комбинаторная логика".

Лекция 1. Ламбда-конверсии

• Запись функции с использованием оператора функциональной абстракции
• Строение формальной системы ламбда-конверсий
• Объекты
• Интерпретация объектов ламбда-исчисления
• Свободные и связанные переменные
• Нормальные формы
• Редукция. Конверсии
• Подстановка
• Постулаты формальной системы ламбда-конверсий
• Метаоператоры аппликации и абстракции

Лекция 2. Комбинаторы

• Выражение общих законов комбинаторами
• Конверсии и строение формальной системы комбинаторной логики
• Синтез объекта с заданными свойствами
• Представление абстракции
• Интерпретация объектов комбинаторной логики
• Парадоксальный комбинатор Карри Y
• Неподвижная точка. Теорема о неподвижной точке

Лекция 3. Базисы

• Метод погружения
• Базис I, K, S и алгоритм разложения в базисе
• Свойство базисности
• Базис I, B, C, S и алгоритм разложения в базисе

Лекция 4. Нумералы

• Представление нумералов
• Свойства нумералов
• Функция "следование за"
• Вычисления с нумералами
• Вычисления с неподвижной точкой

Лекция 5. Встроенные системы

• Погружение и встроенные вычислительные системы
• Осуществление погружения. Большой пример
• Содержательная идея, предформализация, формализация
• Аксиоматизация встроенной системы
• Пример формулировки теоремы о погружении
• Доказательство теоремы о погружении разбором случаев
• Концепт-теория и индивид-теория

Лекция 6. Вычисления в категории

• Представление о категориальной абстрактной машине (КАМ). Вычисление значения в д.з.к.
• Оценивающее отображение. Среда. Примеры вычисления значения выражений
• Коллизии переменных. Устранение коллизий. Кодирование по Дебрейну. Числа Дебрейна
• Вычисление значения в д.з.к. с учетом кодирования по Дебрейну
• Комбинаторный "клей"
• Формулировки теорий вычисления и обоснование их свойств

Лекция 7. Значение выражений: теория вычислений в категории

• Значение выражений и техника вычисления значений
• Среда вычисления значений и ее представление
• Теория вычисления значений по Дебрейну
• Синтаксическая теория вычислений
• Различные формы вычисления значения выражений

Лекция 8. Значение выражений: способы вычисления в категории

• Способы вычислений
• Исполнение скомпилированного кода
• Применение сборки кода
• Сравнение способов вычислений

Лекция 9. Конструирование в категории абстрактной машины (АМ)

• Представление о конструировании абстрактной машины
• Работа абстрактной машины. Состояния
• Цикл работы абстрактной машины
• Примеры вычислений. Компилирование кода и его исполнение

Лекция 10. Цикл работы абстрактной машины

• Описание всевозможных переходов состояний
• Пример вычисление значения 2-местного предиката
• Компилирование кода
• Исполнение кода

Лекция 11. Оптимизация вычислений в категории

• Вычисление на абстрактной машине свертывания по постулату (бета)
• Компилирование кода и его эквивалентные преобразования
• Экономии кодирования и обоснование вычисления бета-свертывания
• Принцип оптимизации (Beta) и его вывод
• Оптимизация и экономия на примере вычисления значения 2-местного оператора

Лекция 12. Расширение и реализация абстрактной машины

• Неподвижная точка в вычислениях и инструкция ветвления
• Кодогенерация для выражения с неподвижной точкой
• Рекурсивная модификация среды (р.м.с.)
• Пример вычисления с р.м.с.
• Большой пример. Выполнение кодогенерации с оптимизацией

Лекция 13. Исполнение кода с рекурсивной модификацией среды на абстрактной машине

• Большой пример. Вспомогательные обозначения для упрощения кода
• Большой пример. Исполнение кода с р.м.с.
• Анализ цикличности в вычислениях. Параметры цикла