ЮрИнфоР >>> Библиотека ЮрИнфоР >>> Компьютерные науки и информационные технологии >>>
Методы и средства вычислений с объектами. Аппликативные вычислительные системы
|
|
Систематически рассмотрены модели, методы и средства, для которых центральной сущностью является представление об объекте. Применен подход, основанный на использовании операций аппликации и абстракции, что позволило выполнить замкнутое изложений техники аппликативных вычислений, оставаясь в рамках элементарных средств. Книга основана на материале, который в различных вариантах использовался для проведения занятий по соответствующим разделам курса компьютерных наук. Приводится необходимый теоретический минимум, соответствующий мировым стандартам, иллюстрируются основные вычислительные идеи, понятия и определения.
Для специалистов, студентов и аспирантов, занятых в области компьютерных наук. Может быть использована для первоначального самостоятельного изучения предмета.
Those models, methods and means are covered that are based on the notation of object. An approach based on the operations of application and functional abstraction is used resulting in the closed consideration of applicative computations within the elementary framework. The material covered in this book was used for delivering the various versions of courses in computer science.
The essential theoretical background corresponds to the high international level, and the basic computational ideas, notions and definitions are explicated.
The book is intended for computer science students and professionals in informatics. It may be used as a sourcebook for graduate course on theoretical computer science.
См. также
Содержание
Предисловие редактора серии
Предисловие
Круг вопросов (Л.Ю. Исмаилова, С.В. Косиков)
Курсы лекций
Введение
I Формализм
- Предисловие к части I
- 1 Формализация
- Вычисление и классы
- 1.1.1 Процесс вычисления
- 1.1.2 Концептуальные классы
- 1.1.3 Классы и типы в программировании
- 1.2 Системы
- 1.2.1 Строение системы
- 1.2.2 Системы объектов
- 1.2.3 \lambda-исчисление
- 1.2.4 Комбинаторы
- 1.3 Дополнительные вопросы
- 2 Классы
- 2.1 Принадлежность
- 2.2 Агрегации
- 2.2.1 Классы и свойства
- 2.2.2 Сведение абстрактных сущностей
- 2.3 Онтология
- 2.3.1 Принадлежность элемента классу
- 2.3.2 Выразимость одних связок через другие
- 2.4 Абстракция
- 2.4.1 Противоречия
- 2.4.2 Конструкция абстракции
- 2.4.3 Тождественность
- 2.4.4 Абстракция в контексте
- 2.5 Дескрипции и имена
- 2.5.1 Дескрипции
- 2.5.2 Имена
- 2.6 Логическое произведение, дополнение и сумма
- 2.7 Включение
- 2.8 Единичный класс
- 2.9 Дополнительные вопросы
- 3 Отношения
- 3.1 Пары и отношения
- 3.1.1 Представление отношения
- 3.1.2 Представление пары
- 3.1.3 Многоместные отношения
- 3.2 Абстракция отношений
- 3.3 Функции
- 3.4 Абстракция функций
- 3.4.1 Представление функциональной абстракции
- 3.4.2 Абстракция и имя функции
- 3.5 Тождественное преобразование
- 3.6 Дополнительные вопросы
- 4 Система объектов
- 4.1 Абстрактная теория
- 4.1.1 Неформальные примитивные идеи
- 4.1.2 Формальные примитивные идеи
- 4.2 Анализ процесса подстановки
- 4.2.1 Неформальные примитивные идеи
- 4.2.2 Формальные примитивные идеи
- 4.3 Дополнительные вопросы
II Аппликативные вычисления
- Предисловие к части II
- 5 \lambda-исчисление
- 5.1 Содержательные $\lambda$-обозначения
- 5.1.1 Содержательные функции
- 5.1.2 Содержательный смысл вычислений
- 5.1.3 Каррирование
- 5.2 Формальная система: об-система
- 5.2.1 Соглашения об обозначениях
- 5.2.2 Метаоператоры
- 5.2.3 Содержательная интерпретация
- 5.2.4 Вхождение и подстановка
- 5.2.5 Построение исчислений
- 5.3 Экстенсиональность
- 5.4 Дополнительные понятия и определения
- 5.4.1 Конгруэнтность
- 5.4.2 Теорема Черча-Россера
- 5.5 Программирование в терминах $\lambda$-исчисления
- 5.5.1 Истинностные значения
- 5.5.2 Натуральные числа
- 5.6 Дополнительные вопросы
- 6 Комбинаторы
- 6.1 Содержательный смысл
- 6.1.1 Комбинирование сущностей
- 6.1.2 Содержательный смысл операторов
- 6.1.3 Принцип экстенсиональности
- 6.2 Рассуждения с комбинаторами
- 6.2.1 Объекты
- 6.2.2 Аксиоматизация системы объектов
- 6.3 Элементарная комбинаторная логика
- 6.3.1 Простейшие комбинаторы
- 6.3.2 Пример вычислений
- 6.4 Строение исчисления объектов
- 6.5 Обозначения
- 6.6 Основные понятия и определения
- 6.6.1 Подстановка
- 6.6.2 Редукция
- 6.6.3 Абстракция
- 6.6.4 Теорема Черча-Россера
- 6.7 Дополнительные вопросы
- 7 Связь \lambda-конверсии и теории комбинаторов
- 7.1 Основные понятия и определения
- 7.2 Связь $\lambda$- и $-преобразований
III Теория вычислений
- Предисловие к части III
- 8 Вычисления в декартово замкнутой категории
- 8.1 Теория функций
- 8.1.1 Множества
- 8.1.2 Классы
- 8.1.3 Непрерывность
- 8.2 Функции в категории
- 8.3 Некоторая теория типов
- 8.3.1 Произведения
- 8.3.2 Вычисление значения
- 8.4 Каррирование
- 8.5 Типовый $\lambda$-язык
- 8.6 Функтор-как-объект
- 8.6.1 Типовая теория
- 8.6.2 Функторная категория
- 8.6.3 Естественные преобразования
- 8.6.4 Переменный объект
- 8.7 Связь с аппликативными вычислениями
- 8.7.1 Теория-оболочка
- 8.7.2 Логика высших порядков
- 8.8 Дополнительные вопросы
- 9 Содержательные объекты: индивиды и концепты
- 9.1 Структура предметной области
- 9.1.1 Индивиды
- 9.1.2 Соотнесения
- 9.1.3 Истинностные значения
- 9.1.4 Логический язык
- 9.2 Концепты
- 9.2.1 Дескрипции
- 9.2.2 Эквациональная теория
- 9.2.3 Интенсионалы и экстенсионалы
- 9.3 Интенсиональные операторы
- 9.3.1 Бинарные отношения
- 9.3.2 Экстенсиональные отношения
- 9.3.3 Интенсиональные отношения
- 10 Экстенсиональное равенство
- 10.1 Содержательный смысл
- 10.2 Экстенсиональность равенства в д.з.к.
- 10.3 Экстенсиональность равенства в АВС
- 10.4 Основные теоремы
- 10.4.1 Связь альтернативных формулировок
- 10.4.2 Финитная аксиоматизация
IV Языки программирования
- Предисловие к части IV
- 11 Представление рекурсивных функций
- 11.1 Кодирования
- 11.1.1 Отождествление выражений с числами
- 11.1.2 Расширение формализации
- 11.1.3 Кодирование комбинаторами
- 11.2 Основные понятия и определения
- 11.2.1 Нумералы
- 11.2.2 Числовые функции
- 11.3 Комбинаторная определимость
- 11.4 Дополнительные вопросы
- 12 Категориальная абстрактная машина
- 12.1 Основные понятия {342 {section.12.1
- 12.1.1 Среда
- 12.1.2 Моделирование \beta-редукции
- 12.1.3 Оптимизация
- 12.1.4 Категориальная комбинаторная логика CCL
- 12.2 Команды
- 12.2.1 Машинные инструкции
- 12.2.2 Примеры исполнения
- 12.3 Рекурсия
- 12.4 Дополнительные вопросы
- 13 Конструкции аппликативного языка
- 13.1 Исходные принципы
- 13.1.1 Аппликативный подход
- 13.1.2 Абстрактный синтаксис
- 13.1.3 Выражения и их значения
- 13.1.4 Использование типов
- 13.2 Выражения
- 13.2.1 Выражения и определения
- 13.2.2 Элементарные типы
- 13.2.3 Декартово произведение
- 13.2.4 Функции
- 13.2.5 Полиморфизм
- 13.2.6 Синтаксические соглашения
- 13.2.7 Диапазон идентификаторов
- 13.2.8 Эквивалентные функциональные пространства
- 13.3 Структуры данных
- 13.3.1 Именованные декартовы произведения
- 13.3.2 Конструкторы
- 13.3.3 Списки
- 14 Семантика конструкций языка
- 14.1 Семантика
- 14.1.1 Вычисление значений
- 14.1.2 Стратегии
- 14.1.3 Рекурсия
- 14.1.4 Стратегии вычислений
- 14.1.5 Семантика программы
- 14.1.6 Корректность программ
- 14.1.7 Доказательство завершаемости
- 14.1.8 Примеры доказательства свойств программ
- 14.1.9 Приписывание типа
- 14.1.10 Вычисление значений
- 14.2 Императивность
- 14.2.1 Исключения
- 14.2.2 Ввод/вывод
- 14.2.3 Потоки символов
- 14.2.4 Модифицируемые структуры данных
- 14.2.5 Семантика деструктивных операций
- 14.3 Дополнительные вопросы
- 15 $\lambda $-исчисление с типами
- 15.1 Аппликативная структура
- 15.1.1 Термы
- 15.1.2 Приписывание
- 15.1.3 Оценивающее отображение
- 15.1.4 Подстановка
- 15.2 Модели с типами
- 15.2.1 Типы
- 15.2.2 Переменные и термы
- 15.2.3 Предструктура
- 15.2.4 Приписывание
- 15.2.5 Структура
- 15.2.6 Подстановка
- 15.2.7 Непротиворечивость
- 15.3 Формула-как-тип
- 15.3.1 Секвенциальное исчисление
- 15.3.2 Типы, термы и конструкции
- 15.4 Дополнительные вопросы
- 16 Объекты с типами: от типов к объектам
- 16.1 Обозначения и определения
- 16.1.1 Содержательная интерпретация
- 16.1.2 Соглашения
- 16.2.1 Комбинаторные термы с типами
- 16.2.2 Типы комбинаторов
- 16.2.3 Типизация при подстановке
- 16.2.4 Типовая слабая редукция и равенство
- 17.1 Обозначения и соглашения
- 17.1.1 Атомарные константы
- 17.1.2 Приписывание типа
- 17.2 Базисные свойства
- 17.2.1 Слабое назначение типов объектам
- 17.2.2 Стратифицированные объекты
- 17.2.3 Абстракция и типы
- 17.2.4 Теорема объектной редукции
- 17.3 Дополнительные вопросы
VI Логика
- Предисловие к части VI
- 18 Логика функциональности (С.В. Косиков)
- 18.1 Генценовский вариант натуральной дедукции
- 18.1.1 Натуральный вывод и неформальное рассуждение
- 18.1.2 Генценовский вариант натурального вывода
- 18.1.3 Особенности генценовских систем
- 18.1.4 Правила заключения и выводы
- 18.2 Система натуральной дедукции для анализа функциональности
- 18.2.1 Приписывание типа абстракции
- 18.2.2 Альтернативная формулировка
- 18.3 Генценовская $-система
- 18.3.1 Конечные базисы
- 18.3.2 Формулировка $-системы
- 18.3.3 Правило сечения
- 18.4 Дополнительные вопросы
- 19 Логика объектов (Л.Ю. Исмаилова)
- 19.1 Проблематика
- 19.2 Иллативная комбинаторная логика
- 19.3 Парадоксальность прямого построения логики
- 19.3.1 Парадокс Карри
- 19.3.2 Теорема дедукции
- 19.4 Логические константы
- 19.4.1 Связки и кванторы
- 19.4.2 Функциональность и эквиваленция
- 19.5 Дополнительные вопросы
- 20 Канонические объекты
- 20.1 Теорема дедукции
- 20.1.1 Канонические термы
- 20.1.2 Теорема дедукции для $\Xi$
- 20.2 $-система Генцена
- 20.2.1 Канонические термы
- 20.2.2 $-формулировка
- 20.3 Универсальная общность
- 20.4 Дополнительные вопросы
VII Приложение
- A Доказательство теоремы Черча-Россера
- A.1 Основные определения
- A.2 Леммы
- A.3 Основное доказательство
- A.4 Дополнительные вопросы
- B Сильная редукция
- B.1 Основные понятия и определения
- B.2 Теорема Черча-Россера
- C Точная арифметика
- C.1 Представление целых чисел списками
- C.1.1 База
- C.1.2 Операции над наименее значащими цифрами
- C.1.3 Операции над цифрой и числом
- C.1.4 Операции над представлениями чисел
- C.1.5 Операции сравнения
- C.1.6 Операция деления
- C.1.7 Алгоритм деления
- C.1.8 Тип натуральных чисел
- C.1.9 Метод Ньютона
- C.1.10 Экспоненцирование
- C.1.11 Вывод натуральных чисел
- C.2 Пример: вычисление \pi
- C.2.1 Рекуррентные соотношения
- C.2.2 Эффективные вычисления
Библиография
Диссертации
Именной указатель
Указатель символов
Указатель терминов
Глоссарий
Об авторе
- В.Э. Вольфенгаген