- Артикул:00-01105219
- Автор: Барендрегт X.
- Тираж: 4800 экз.
- Обложка: Твердая обложка
- Издательство: МИР (все книги издательства)
- Город: Москва
- Страниц: 606
- Формат: 60х90 1/16
- Год: 1985
- Вес: 831 г
Ламбда-исчисление. Его синтаксис и семантика
Репринтное издание
Монография посвящена классическим и новым результатам в активно развивающемся направлении математической логики,-так называемом ламбда-исчислении. Оно находит применение в теории доказательств, семантике языков программирования, алгебре, топологии, теории категорий. Изложение отличается полнотой и доступностью. Автор книги - известный голландский математик.
Для математиков разных специальностей, преподавателей, аспирантов и студентов университетов.
Содержание
Предисловие к русскому изданию
Предисловие автора к русскому изданию
Предисловие
Указания читателю
Часть I. На пути к теории
Глава 1. Введение
1.1. Аспекты ламбда-исчисления
1.2. Полные частично упорядоченные множества и топология Скотта
1.3. Упражнения
Глава 2. Конверсия
2.1. Ламбда-термы и конверсия
2.2. Некоторые варианты теории X
2.3. Обзор части II
2.4. Упражнения
Глава 3. Редукция
3.1. Понятие редукции
3.2. Бета-редукция
3.3. r)-редукция
3.4. Обзор части III
З.Б. Упражнения
Глава 4. Теории
4.1. Ламбда-теории
4.2. Обзор части IV
4.3. Упражнения
Глава 5. Модели
5.1. Комбинаторные алгебры
5.2. Ламбда-алгебры и ламбда-модели
5.3. Синтаксические модели
5.4. Модели в конкретных декартово замкнутых категориях
5.5 Модели в произвольных декартово замкнутых категориях
5.6. Другие описания моделей. Категоричные модели
5.7. Обзор части V
5.8. Упражнения
Часть II. Конверсия
Глава 6. Классическое ламбда-исчисление
6.1. Комбинаторы неподвижной точки
6.2. Стандартные комбинаторы
6.3. Ламбда-определимость
6.4. Цифровые системы
6.5. Еще о неподвижных точках; гёделевские номера
6.6. Результаты о неразрешимости
6.7. Отступление: рефлексивные предложения и теорема о рекурсии
6.8. Упражнения
Глава 7. Теория комбинаторов
7.1. Комбинаторная логика
7.2. Редукция для CL
7.3. Соотношение между CL и X
7.4. Упражнения
Глава 8. Классическое ламбда-исчисление (продолжение)
8.1. Базисы и перечисления
8 2. Равномерность; бесконечные последовательности
8.3. Разрешимость; головные нормальные формы
8.4. Ламбда-определимость частичных функций
8.5. Упражнения
Глава 9. лI-исчисление
9.1. Общие соображения
9.2. Определимость
9.3. Комбинаторы
9.4 Разрешимость
9.5. Упражнения
Глава 10. Деревья Бёма
10.1. Основные факты
10.2. Сравнение деревьев Бёма. Топология деревьев на Л
10.3. Техника выворачивания по Бёму
10.4. Отделимость термов
10.5. Отделимость в лI -исчислении
10.6. Упражнения
Часть III. Редукция
Глава 11. Фундаментальные теоремы
11.1. Теорема Чёрча - Россера
11.2. Конечность разверток
11.3. Теорема о консервативности для лI
11.4. Стандартизация
11.5. Упражнения
Глава 12. Сильно эквивалентные редукции
12.1. Редукционные диаграммы
12.2. Сильные варианты теорем CR и FD
12.3. Сильный вариант теоремы стандартизации!
12.4. Упражнения
Глава 13. Редукционные стратегии
13.1. Классификация стратегий
13.2. Эффективные нормализующие и кофинальные стратегии
13.3. Рекурсивная CR-стратегия
13.4. Эффективная зацикливающая стратегия
13.5. Оптимальные стратегии
13.6. Упражнения
Глава 14. Помеченная редукция
14.1. Сильная нормализация
14.2. Приложения
14.3. Непрерывность
14.4. Последовательность вычислений и устойчивость
14.5. Упражнения
Глава 15. Другие понятия редукции
15.1. Bn-редукция
15.2. BnO-редукция
15.3. Дельта-редукция
15.4. Упражнения
Часть IV. Теории
Глава 16. Осмысленные теории
16.1. Теория Н
16.2. Теория Н
16.3. 2Ко осмысленных теорий
16.4. Теория В
16.5. Упражнения
Глава 17. Другие ламбда-теории
17.1. Полуосмысленные и р.п. теории
17.2. Омега-теории
17.3. Частичная корректность ш-правила в лn
17.4. w-правило и теория нn
17.5. Упражнения
Часть V. Модели
Глава 18. Построение моделей
18.1. Графиковая модель Рw
18.2. Модель Doo
18.3. Модель B
18.4. Упражнения
Глава 19. Локальная структура моделей
19.1. Локальная структура модели Pw
19.2. Локальная структура модели Doo
19.3. Непрерывные л-модели
19.4. Упражнения
Глава 20. Глобальная структура моделей
20.1. Экстенсиональность, категоричность
20.2. Свойство области
20.3. Результаты о неопределимости
20.4. Локальная и глобальная представимость
20.5. Топология деревьев на моделях
20.6. Упражнения
Глава 21. Комбинаторные группы
21.1. Комбинаторные полугруппы
21.2. Характеризация обратимости
21.3. Группы G(лn) и G(Н)
21.4. Упражнения
Приложения
Приложение А. Типовое ламбда-исчисление
А.1. Чистое типовое ламбда-исчисление
А.2. Примитивно рекурсивные функционалы
А.З. Формулы-типы
Приложение В. Иллативная комбинаторная логика
Приложение С. Переменные
Заключительные упражнения
Добавления
Литература
Предметный указатель
Указатель обозначений
Рекомендуем
