Ламбда-исчисление, Его синтаксис и семантика, Барендрегт X., 1985

Ламбда-исчисление, Его синтаксис и семантика, Барендрегт X., 1985.

   Монография посвящена классическим и новым результатам в активно развивающемся направлении математической логики,— так называемом ламбда-исчислении. Оно находит применение в теории доказательств, семантике языков программирования, алгебре, топологии, теории категорий. Изложение отличается полнотой и доступностью. Автор книги — известный голландский математик.
Для математиков разных специальностей, преподавателей, аспирантов и студентов университетов.




Аспекты ламбда-исчисления.
Ламбда-исчисление — это бестиповая теория, рассматривающая функции как правила, а не как графики. Понятие «функции как закона или правила» кажется старомодным и подразумевает переход от аргумента к значению, процесс, закодированный некоторым определением. Приписываемая обычно Дирихле мысль о том, что функции можно рассматривать как графики, т. е. множества, состоящие из пар аргумент — значение, была важным вкладом в математику. Тем не менее ламбда-исчисление снова рассматривает функции как правила, чтобы подчеркнуть их вычислительные аспекты.

Функции как правила рассматриваются в полной общности. Например, мы можем считать, что функции заданы определениями на обычном русском языке и применяются к аргументам, также описанным по-русски. Конкретнее, рассмотрим функции, заданные программами для машин и применяемые к другим таким программам. В обоих случаях перед нами бестиповая структура, где объекты изучения являются одновременно и функциями, и аргументами. Это — отправная точка бестипового λ-исчисления. В частности, функция может применяться к самой себе. При обычном понимании функции в математике (скажем, в теории множеств Цермело — Френкеля) это невозможно (из-за аксиомы фундирования). (См. также упр. 18.5.30.).

ОГЛАВЛЕНИЕ.
Предисловие к русскому изданию.
Предисловие автора к русскому изданию.
Предисловие.
Указания читателю.
Часть I. На пути к теории.
Глава 1. Введение.
1.1. Аспекты ламбда-исчисления.
1.2. Полные частично упорядоченные множества и топология Скотта.
1.3. Упражнения.
Глава 2. Конверсия.
2.1. Ламбда-термы и конверсия.
2.2. Некоторые варианты теории λ.
2.3. Обзор части II.
2.4. Упражнения.
Глава 3. Редукция.
3.1. Понятие редукции.
3.2. Бета-редукция.
3.3. η-редукция.
3.4. Обзор части III.
3.6. Упражнения.
Глава 4. Теории.
4.1. Ламбда-теории.
4.2. Обзор части IV.
4.3. Упражнения.
Глава 5. Модели.
6.1. Комбинаторные алгебры.
5.2. Ламбда-алгебры и ламбда-модели.
6.3. Синтаксические модели.
6.4. Модели в конкретных декартово замкнутых категориях.
6.5. Модели в произвольных декартово замкнутых категориях.
5.6. Другие описания моделей. Категоричные модели.
6.7. Обзор части V.
6.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 и λ.
7.4. Упражнения.
Глава 8. Классическое ламбда-исчисление (продолжение)
8.1. Базисы и перечисления.
82. Равномерность; бесконечные последовательности.
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 и FDI.
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. βη-редукцня.
15.2. βηΩ-редукция.
15.3. Дельта-редукция.
15.4. Упражнения.
Часть IV. Теории.
Глава 16. Осмысленные теории.
16.1. Теория H.
16.2. Теория H*.
16.3. 2 осмысленных теорий.
16.4. Теория B.
16.5. Упражнения.
Глава 17. Другие ламбда-теории.
17.1. Полуосмысленные и р. п. теории.
17.2. Омега-теории.
17.3. Частичная корректность w-правила в λη.
17.4. w-правило и теория Hη.
17.5. Упражнения.
Часть V. Модели.
Глава 18. Построение моделей.
18.1. Графиковая модель Рw.
18.2. Модель D∞.
18.3. Модель B.
18.4. Упражнения.
Глава 19. Локальная структура моделей.
19.1. Локальная структура модели Рw.
19.2. Локальная структура модели D∞.
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(λη) и G(H*).
21.4. Упражнения.
Приложения.
Приложение А. Типовое ламбда-исчисление.
А.1. Чистое типовое ламбда-исчисление.
А.2. Примитивно рекурсивные функционалы.
А.3. Формулы-типы.
Приложение В. Иллативная комбинаторная логика.
Приложение С. Переменные
Заключительные упражнения.
Добавления.
Литература.
Предметный указатель
Указатель обозначений



Бесплатно скачать электронную книгу в удобном формате, смотреть и читать:
Скачать книгу Ламбда-исчисление, Его синтаксис и семантика, Барендрегт X., 1985 - fileskachat.com, быстрое и бесплатное скачивание.

Скачать djvu
Ниже можно купить эту книгу по лучшей цене со скидкой с доставкой по всей России.Купить эту книгу


Скачать - djvu - Яндекс.Диск.




Теги: учебник по математике :: математика :: Барендрегт :: ламбда