Курс: Модели вычислений Описание
Введение

Что в курсе изучается

Для кого курс

Как курс читается

Примерный перечень вопросов к экзамену

Примерный перечень задач к экзамену

Видеокурс

Введение

Курс моделей вычислений считается базовым для компьютерных наук и информационных технологий, а поиск новых моделей, изучение их свойств и выявление технологических преимуществ находятся на переднем крае научных исследований.

Вверх

Что в курсе изучается?

Вот те некоторые вещи, которые, как ожидается, будут изучены (некоторые -- ознакомительно, другие -- углубленно. Особое место отводится вычислениям с объектами и их связи с системами высших порядков.
  • В начале рассматриваются вычисления на основе функций с оператором абстракции.
  • Исходя из развитых представлений, изучается структура формальной системы комбинаторной логики и ламбда-исчисления.
  • Показываются связи между возможными формами представления объектов, комбинаторная редукция, экспансия и конверсии.
  • Подробно рассматривается задача синтеза объекта с заданной комбинаторной характеристикой.
  • Дается формулировка синтаксической теории вычислений, вводится представление о бестиповой системе.
  • Изучаются комбинаторные базисы и их свойства, а также разложение произвольного объекта в базисах.
  • Доказывается теорема о неподвижной точке, рассматривается парадоксальный комбинатор Y и его применения к циклическим вычислениям.
  • Рассматриваются приемы назначения типа объекту, исходя из структуры подобъектов.
  • Изучается метод погружения и рассматривается задача построения погруженной вычислительной системы.
  • Изучается динамика вычислений, процесс компилирования комбинаторного кода.
  • Рассматриваются механизмы вычислений, их параметризации и оптимизации.
  • Изучается вычисление значения объекта с применением декартово замкнутой категории.
  • Рассматривается строение категориальной абстрактной машины, реализация объектно-функциональных языков.
  • Излагаются механизмы вычислений и вычисления в категории.
  • На основе эквациональных систем устанавливается взаимная сводимость различных форм теории вычислений.
  • Рассматривается кодогенерация, даются доказательства оптимизационных равенств.
  • Изучается цикл работы абстрактной машины, рекурсивная модификация среды вычислений.
  • Даются примеры реализации в языках CAML и F#.

Вверх

Для кого курс (кому этот курс особенно полезен)

В базовом или сокращенном объеме курс может расцениваться как ознакомительный со всеми этими принципами. В таком случае он может служить отличным вводным курсом в проблематику моделей вычислений в информационных технологиях.

В особенности приятно работать со студентами, которые мыслят нетривиально и изобретательны, а также с теми, кто имеет серьезную установку на научно-исследовательскую работу. Конечно, курс удобен и для тех, кто ожидает хорошо структурированный учебник, по которому можно все усвоить. Кончено, лучше всего материал увязывать с постоянно растущим и нестабильным объемом результатов в направлении новых информационных технологий и программных средств. Весь этот вкус выполнения живого исследования с помощью моделей вычислений хотелось бы во время занятий ощущать вместе со студентами.

Вверх

Как курс читается?

Организация учебного процесса заключается в следующем:

  • лекции, которые читаются в аудитории,
  • выполнение самостоятельной работы, результаты которой обсуждаются в аудитории в форме студенческих презентаций,
  • небольшие контрольные работы/проверки уровня знания,
  • самостоятельно выполняемая в течение семестра курсовая работа/домашнее задание

Конечно, студенту надо посещать все занятия, причем исключением может быть уважительная причина. К каждому занятию надо готовиться, прочитав уже изложенный материал и просмотрев новый материал, это лучше всего. Вместе с тем это -- минимальное академическое требование. Активная работа на занятиях, участие в разборе решения задач и примеров является важным показателем уровня ваших знаний по предмету, степенью активного владения методами. Компонентами изучения предмета являются (а) презентации в аудитории, (б) активное участие в занятии, (в) выполненная курсовая работа, а также (г) промежуточный зачет в середине семестра.

Образовательная философия: для всех нас интерес представляет "научиться тому, как учиться", а не просто освоение информации, которая кем-то излагается в упорядоченном виде.

Вверх

Примерный перечень вопросов к экзамену

Раздел I. Программирование с переменными. Объекты, абстракция, переменные, диапазоны, формальный и фактический параметр, подстановка, связывание формального и фактического параметра.
1. Определение объекта (на примере ламбда-исчисления). МСВО-2004, Гл. 5, с. 137-148;
КЛП-2003, Гл. 1, с. 27-44
 
2. Конвертирование программ и данных (на примере постулатов ламбда-исчисления). Примитивная система программирования со связанными переменными. МСВО-2004, Гл. 5, с. 137-166;
КЛП-2003, Гл. 1, с. 27-44
 
Раздел II. Программирование без связанных переменных. Объекты, константные формы, комбинирование, комбинаторный код. Эквивалентные преобразования объектов и отношение конвертирования. Редукции объектов.
3. Определение объекта (на примере комбинаторной логики). МСВО-2004, Гл. 6, с. 179-188;  
4. Конвертирование программ и данных (на примере постулатов комбинаторной логики). Примитивная система программирования без связанных переменных. МСВО-2004, Гл. 6, с. 179-195;  

5. Трансляция одной примитивной системы программирования в другую (на примере связи ламбда-исчисления и комбинаторной логики).

МСВО-2004, Гл. 6, с. 195-199; Гл. 7, с. 207-214;  
Раздел III. Синтез объекта. Неподвижная точка в вычислениях. Циклические вычисления с объектами. Рекурсивные определения и их преобразования.
6. Постановка задачи синтеза нового объекта с заданными свойствами. Синтез алгоритма, реализующего объект, как вывод. МСВО-2004, Гл. 6, с. 192-195;
КЛП-2003, Гл. 2, с. 45-64
 
7. Определение неподвижной точки. Циклические вычисления с объектами. Применения. МСВО-2004, Гл. 14, с. 460-466;
КЛП-2003, Гл. 3, с. 65-74; Гл. 9, с. 123-132
 
8. Комбинатор неподвижной точки. Примеры реализаций. МСВО-2004, Гл. 14, с. 460-474;
КЛП-2003, Гл. 3, с. 65-74; Гл. 9, с. 123-132 
 
9. Исследование свойств комбинатора неподвижной точки. МСВО-2004, Гл. 14, с. 460-474;
КЛП-2003, Гл. 3, с. 65-74; Гл. 9, с. 123-132
 
10. Теорема о неподвижной точке. Применения в программировании. МСВО-2004, Гл. 14, с. 460-474;
КЛП-2003, Гл. 3, с. 65-74; Гл. 9, с. 123-132 
 
Раздел IV. Простейшая форма компилирования кода. Базисы объектов. Устранение переменных в процедуре или функции.
11. Базисы объектов. Алгоритм разложения в базисе I, K, S. Условия применимости и пример. МСВО-2004, Гл. 7, с. 213-214;
КЛП-2003, Гл. 7, с. 113-116
 
12. Алгоритм разложения в базисе I, B, C, S. Условия применимости и пример. МСВО-2004, Гл. 7, с. 213-214;
КЛП-2003, Гл. 8, с. 117-122
 
Раздел V. Типы в программе. Приписывание типов. Объекты с типами. Правильная типизация и вывод типа через уже известные типы. Правила работы с типами.
13. Исчисление объектов с типами (на примере комбинаторной логики). Правила приписывания типов (F ), (I), (K), (S). Пример использования. МСВО-2004, Гл. 16, с. 560-568;
КЛП-2003, Гл. 6, с. 93-96
 

14. Приписывание типа объектам (на примере ламбда-исчисления). Правила приписывания типов (λ), (F ). Пример использования.

МСВО-2004, Гл. 15, с. 541-543;
КЛП-2003, Гл. 6, с. 97
 
15. Приписать тип объектам I, K, S. МСВО-2004, Гл. 16, с. 560-568;
КЛП-2003, Гл. 6, с. 97-112
 
Раздел VI. Приемы кодирования информации. Символьные преобразования. Программирование эквивалентных преобразований информации и конверсии объектов. Устранение коллизий и побочных эффектов. Компилирование кода. Кодогенерация. Оптимизация кода. Экономии в вычислениях. Исполнение кода. Абстрактная машина.
16. Пример коллизии переменных. Связь с постулатами (α) и (β). МСВО-2004, Гл. 5, с. 154-156;
КЛП-2003, Гл. 19, с. 223-226; Гл. 20, с. 227-229
КАМ-2002, Гл. 1, с. 23
17. Коды де Брейна. Применения. Ликвидация коллизий. МСВО-2004, Гл. 12, с. 342-352;
КЛП-2003, Гл. 20, с. 227-229
КАМ-2002, Гл. 1, с. 20-22
18. Понятие о среде. Правила вычисления значения объекта ламбда-исчисления. МСВО-2004, Гл. 12, с. 343-359;
КЛП-2003, Гл. 20, с. 227-232
КАМ-2002, Гл. 1, с. 13-19
19. Теория вычислений. Связь с кодами де Брейна. МСВО-2004, Гл. 12, с. 359-374;
КЛП-2003, Гл. 20, с. 227-232
КАМ-2002, Гл. 1, с. 24-27
20. Теория вычислений. Определение свойств объектов S, Λ, ε. МСВО-2004, Гл. 12, с. 359-374;
КЛП-2003, Гл. 20, с. 227-232
КАМ-2002, Гл. 2, с.39-43
21. Теория вычислений в синтаксической форме. Равенства (ass), (fst), (snd), (dpair), (ac), (quote). МСВО-2004, Гл. 12, с. 359-374;
КЛП-2003, Гл. 20, с. 231
КАМ-2002, Гл. 2, с. 44-47
22. Для объекта M обосновать равенство ´M = Λ(M ° Snd). МСВО-2004, Гл. 12, с. 377-380;
КЛП-2003, Гл. 20, с. 231
КАМ-2002, Гл. 2, с. 46
23. Понятие о категориальной абстрактной машине. Кодогенерация. Вычисление значения. МСВО-2004, Гл. 12, с. 374-378;
КЛП-2003, Гл. 20, Гл. 21
КАМ-2002, Гл. 2, с. 48-50; с. 25-31
24. Цикл работы категориальной абстрактной машины. МСВО-2004, Гл. 12, с. 374-377;
КЛП-2003, Гл. 21, с. 233-240
КАМ-2002, Гл. 2, с. 50-57
25. Оптимизация кода. Правило (Beta). МСВО-2004, Гл. 12, с. 369-370;
КЛП-2003, Гл. 22, с. 243-251
КАМ-2002, Гл. 3, с. 65-67
26. Обоснование кодогенерации и КАМ-вычисления для 2-х местного оператора. МСВО-2004, Гл. 12, с. 377-380;
КЛП-2003, Гл. 21, с. 241
КАМ-2002, Гл. 3, с. 67-68
27. Обоснование вычисления свертывания. Связь постулатов (β) и правила (Beta). МСВО-2004, Гл. 12, с. 369-370; КАМ-2002, Гл. 3, с. 65-68
28. Экономии в кодировании. МСВО-2004, Гл. 12, с. 380-382; КАМ-2002, Гл. 3, с. 65-68
29. Расширение и реализация категориальной абстрактной машины. МСВО-2004, Гл. 12, с. 382-384; КАМ-2002, Гл. 4, с. 69-73
30. Схема вычисления на категориальной абстрактной машине объекта с комбинаторной характеристикой YM = M(YM). МСВО-2004, Гл. 12, с. 383; КАМ-2002, Гл. 4, с. 71-72

31. Схема вычисления на КАМ объекта, содержащего неподвижную точку. Решение при ограничении ||M|| = ||λλ.P||.

МСВО-2004, Гл. 12, с. 383-384; КАМ-2002, Гл. 4, с. 71-73
32. Стек рекурсии на КАМ. Его представление гиперграфом. МСВО-2004, Гл. 12, с. 382-386; КАМ-2002, Гл. 4, с. 71-73
33. Вычислить на КАМ 1!. Записать выражение, выполнить кодогенерацию и произвести оптимизацию кода, дать его полное табличное исполнение, указав точки рекурсивной модификации среды. МСВО-2004, Гл. 12, с. 382-385; КАМ-2002, Гл. 4, с. 73-77
34. Вычислить на КАМ 2!. Записать выражение, выполнить кодогенерацию и произвести оптимизацию кода, дать его полное табличное исполнение, указав точки рекурсивной модификации среды. МСВО-2004, Гл. 12, с. 386-387; КАМ-2002, Гл. 4, с. 77-79
35. Вычислить на КАМ 3!. Записать выражение, выполнить кодогенерацию и произвести оптимизацию кода, дать его полное табличное исполнение, указав точки рекурсивной модификации среды. МСВО-2004, Гл. 12, с. 382-387; КАМ-2002, Гл. 4, с. 73-79

Основная литература

[МСВО-2004] Вольфенгаген В.Э. Методы и средства вычислений с объектами. Аппликативные вычислительные системы. -- М.:АО ``Центр ЮрИнфоР’’, 2004. - xvi+789 с.
[КАМ-2002] Вольфенгаген В.Э. Категориальная абстрактная машина. -- М.:МИФИ, 1993. 2-е изд. – М.: АО “ Центр ЮрИнфоР ”, 2002. – 96 с.
[КЛП-2003] Вольфенгаген В.Э. Комбинаторная логика в программировании. Вычисления с объектами в примерах и задачах. -- М.:МИФИ, 1994; 2-е изд. – М.: АО “ Центр ЮрИнфоР ”, 2003. – 336 с.

Вверх

Примерный перечень задач к экзамену

Задача 1 КЛП-2003, задача 22.1, с. 243-251 Включена в билет
Задача 2 КЛП-2003, задача 21.1, с. 240-241 Включена в билет
Задача 3 КЛП-2003, задача 19.1, с. 223-225 Включена в билет
Задача 4 КЛП-2003, задача 18.1, с. 217-221 Включена в билет
Задача 5 КЛП-2003, задача 17.1, с. 213-216 Включена в билет
Задача 6 КЛП-2003, задача 16.1, с. 201-203 Включена в билет
Задача 7 КЛП-2003, Гл. 14.1, задача, с.158-161 Включена в билет
Задача 8 КЛП-2003, задача 9.1 (п. 2), с. 128-131 Включена в билет
Задача 9 КЛП-2003, задача 9.1 (п. 3), с. 128-131 Включена в билет
Задача 10 КЛП-2003, задача 9.1 (п. 4), с. 128-131 Включена в билет
Задача 11 КЛП-2003, задача 9.1 (п. 5), с. 128-131 Включена в билет
Задача 12 КЛП-2003, задача 9.1 (п. 6), с. 128-131 Включена в билет
Задача 13 КЛП-2003, задача 8.1 (п. 2), с. 120-121 Включена в билет
Задача 14 КЛП-2003, задача 7.1 (п. 2), с. 114-115 Включена в билет
Задача 15 КЛП-2003, задача 6.1, с. 99-100 Включена в билет
Задача 16 КЛП-2003, задача 6.2, с. 100 Включена в билет
Задача 17 КЛП-2003, задача 6.3, с. 100-101 Включена в билет
Задача 18 КЛП-2003, задача 6.4, с. 101-102 Включена в билет
Задача 19 КЛП-2003, задача 6.5, с. 102-103 Включена в билет
Задача 20 КЛП-2003, задача 6.16, с. 111-112 Включена в билет
Задача 21 КЛП-2003, задача 6.6, с. 103-104 Включена в билет
Задача 22 КЛП-2003, задача 6.7, с. 104-105 Включена в билет
Задача 23 КЛП-2003, задача 6.8, с. 105 Включена в билет
Задача 24 КЛП-2003, задача 6.9, с. 105-106 Включена в билет
Задача 25 КЛП-2003, задача 6.10, с. 106-107 Включена в билет
Задача 26 КЛП-2003, задача 6.11, с. 107-108 Включена в билет
Задача 27 КЛП-2003, задача 6.12, с. 108 Включена в билет
Задача 28 КЛП-2003, задача 6.13, с. 109 Включена в билет
Задача 29 КЛП-2003, задача 6.14, с. 109-110 Включена в билет
Задача 30 КЛП-2003, задача 6.15, 6.16, с. 110-112 Включена в билет

Вверх

Содержание видеокурса (Как купить, см. URL http://www.jurinfor.ru/educ/dvdcl.php)

Часть I. Аппликативный компьютинг.

1. Ламбда-конверсии
1.1. Запись функции с использованием оператора функциональной абстракции.
1.2. Строение формальной системы ламбда-конверсий.
1.2.1. Объекты.
1.2.2. Интерпретация объектов ламбда-исчисления.
1.3. Свободные и связанные переменные.
1.4. Нормальные формы.
1.5. Редукция. Конверсии.
1.6. Подстановка.
1.7. Постулаты формальной системы ламбда-конверсий.
1.8. Метаоператоры аппликации и абстракции.

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

3. Базисы
3.1. Метод погружения.
3.2. Базис I, K, S и алгоритм разложения в базисе .
3.3. Свойство базисности.
3.4. Базис I, B, C, S и алгоритм разложения в базисе .

4. Нумералы
4.1. Представление нумералов.
4.2. Свойства нумералов.
4.3. Функция “следование за”.
4.4. Вычисления с нумералами.
4.5. Вычисления с неподвижной точкой.

5. Встроенные системы
5.1. Погружение и встроенные вычислительные системы.
5.2. Осуществление погружения. Большой пример.
5.3. Содержательная идея, предформализация, формализация.
5.4. Аксиоматизация встроенной системы.
5.5. Пример формулировки теоремы о погружении.
5.6. Доказательство теоремы о погружении разбором случаев.
5.7. Концепт-теория и индивид-теория.

Часть II. Компьютинг в декартово замкнутой категории (д.з.к.).

6. Вычисления в категории.
6.1. Представление о категориальной абстрактной машине (КАМ). Вычисление значения в д.з.к.
6.2. Оценивающее отображение. Среда. Примеры вычисления значения выражений.
6.3. Коллизии переменных. Устранение коллизий. Кодирование по Дебрейну. Числа Дебрейна.
6.4. Вычисление значения в д.з.к. с учетом кодирования по Дебрейну.
6.5. Комбинаторный “клей”.
6.6. Формулировки теорий вычисления и обоснование их свойств.

7. Значение выражений: теория вычислений в категории
7.1. Значение выражений и техника вычисления значений.
7.2. Среда вычисления значений и ее представление.
7.3. Теория вычисления значений по Дебрейну.
7.4. Синтаксическая теория вычислений.
7.5. Различные формы вычисления значения выражений.

8. Значение выражений: способы вычисления в категории
8.1. Способы вычислений.
8.2. Исполнение скомпилированного кода.
8.3. Применение сборки кода.
8.4. Сравнение способов вычислений.

9. Конструирование в категории абстрактной машины (АМ).
9.1. Представление о конструировании абстрактной машины.
9.2. Работа абстрактной машины. Состояния.
9.3. Цикл работы абстрактной машины.
9.4. Примеры вычислений. Компилирование кода и его исполнение.

10. Цикл работы абстрактной машины.
10.1. Описание всевозможных переходов состояний.
10.2. Пример вычисление значения 2-местного предиката.
10.2.1. Компилирование кода.
102.2. Исполнение кода.

11. Оптимизация вычислений в категории.
11.1. Вычисление на абстрактной машине свертывания по постулату (β).
11.2. Компилирование кода и его эквивалентные преобразования
11.3. Экономии кодирования и обоснование вычисления β-свертывания.
11.4. Принцип оптимизации (Beta) и его вывод.
11.5. Оптимизация и экономия на примере вычисления значения 2-местного оператора.

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

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

Вверх

Last update: 05/07/07    

Модели вычислений: учебный курс, Модели вычислений: что читать, Модели вычислений: программа, Модели вычислений: студенты