Расчет конструкций
В математической логике и информатике исчисление конструкций ( CoC ) — это теория типов, созданная Тьерри Кокандом . Он может служить как типизированным языком программирования , так и конструктивной основой математики . По этой второй причине CoC и его варианты легли в основу Coq и других помощников по доказательствам .
Некоторые из его вариантов включают исчисление индуктивных конструкций. [1] (которое добавляет индуктивные типы ), исчисление (ко)индуктивных конструкций (которое добавляет коиндукцию ) и предикативное исчисление индуктивных конструкций (которое устраняет некоторую непредикативность ).
Общие черты [ править ]
CoC — это типизированное лямбда-исчисление высшего порядка , первоначально разработанное Тьерри Кокандом . Он хорошо известен тем, что находится на вершине Барендрегта куба лямбда- . В CoC можно определять функции от терминов к терминам, а также термины к типам, типы к типам и типы к терминам.
Кодекс поведения является строго нормализующим и, следовательно, последовательным . [2]
Использование [ править ]
CoC был разработан вместе с Coq помощником по проверке доказательств . По мере того, как в теорию добавлялись функции (или устранялись возможные недостатки), они становились доступными в Coq.
Варианты CoC используются в других помощниках по доказательству, таких как Matita и Lean .
Основы строительного исчисления [ править ]
Исчисление конструкций можно рассматривать как расширение изоморфизма Карри–Говарда . Изоморфизм Карри-Ховарда связывает термин в просто типизированном лямбда-исчислении с каждым доказательством естественной дедукции в интуиционистской логике высказываний . Исчисление конструкций расширяет этот изоморфизм до доказательств в полном интуиционистском исчислении предикатов , которое включает в себя доказательства кванторных утверждений (которые мы также будем называть «предложениями»).
Условия [ править ]
Терм : в исчислении конструкций строится по следующим правилам
- — это термин (также называемый типом );
- — это термин (также называемый prop , тип всех предложений);
- Переменные ( ) — термины;
- Если и это термины, то и так ;
- Если и это термины и является переменной, то следующие термины также являются термами:
- ,
- .
Другими словами, термин «синтаксис» в форме Бэкуса-Наура выглядит следующим образом:
Исчисление конструкций имеет пять видов объектов:
- доказательства , которые представляют собой термины, типами которых являются предложения ;
- предложения , которые также известны как малые типы ;
- предикаты — функции, возвращающие предложения;
- большие типы , которые являются типами предикатов ( является примером крупного типа);
- сам по себе, что является типом больших типов.
Решения [ править ]
Исчисление конструкций позволяет доказать типичные суждения :
- ,
что можно прочитать как импликацию
- Если переменные имеют соответственно типы , то срок имеет тип .
Действительные суждения для исчисления конструкций выводятся из набора правил вывода. Далее мы используем означать последовательность присвоений типов ; означать термины; и означать либо или . Мы напишем означать результат замены термина для свободной переменной в срок .
Правило вывода записывается в виде
- ,
что означает
- если является действительным суждением, то таковым является и .
Правила вывода для исчисления конструкций [ править ]
1 .
2 .
3 .
4 .
5 .
6 .
Определение логических операторов [ править ]
В исчислении конструкций очень мало основных операторов: единственным логическим оператором для формирования предложений является . Однако этого одного оператора достаточно для определения всех остальных логических операторов:
Определение типов данных [ править ]
Основные типы данных, используемые в информатике, можно определить в рамках исчисления конструкций:
- логические значения
- естественный
- Продукт
- Непересекающийся союз
Обратите внимание, что логические значения и натуральные значения определяются так же, как и в кодировке Чёрча . Однако дополнительные проблемы возникают из-за пропозициональной экстенсиональности и нерелевантности доказательств. [3]
См. также [ править ]
- Система чистого типа
- Лямбда-куб
- Система Ф
- Зависимый тип
- Интуиционистская теория типов
- Теория гомотопических типов
Ссылки [ править ]
- ^ Исчисление индуктивных конструкций и основные стандартные библиотеки:
Datatypes
иLogic
. - ^ Коканд, Тьерри; Галье, Жан Х. (июль 1990 г.). «Доказательство сильной нормализации теории конструкций с использованием интерпретации типа Крипке» . Технические отчеты (СНГ) : 14.
- ^ «Стандартная библиотека | Помощник по проверке Coq» . coq.inria.fr . Проверено 8 августа 2020 г.
Источники [ править ]
- Коканд, Тьерри ; Юэ, Жерар (1988). «Строительный расчет» (PDF) . Информация и вычисления . 76 (2–3): 95–120. дои : 10.1016/0890-5401(88)90005-3 .
- Также имеется в свободном доступе онлайн: Коканд, Тьерри; Юэ, Жерар (1986). Расчет конструкций (Технический отчет). ИНРИА , Центр Рокенкур. 530.
Обратите внимание, что терминология довольно разная. Например, ( ) пишется [ x : A ] B .
- Также имеется в свободном доступе онлайн: Коканд, Тьерри; Юэ, Жерар (1986). Расчет конструкций (Технический отчет). ИНРИА , Центр Рокенкур. 530.
- Бандер, М.В.; Селдин, Джонатан П. (2004). «Варианты основного расчета конструкций» . CiteSeer х : 10.1.1.88.9497 .
- Фраде, Мария Жуан (2009). «Исчисление индуктивных конструкций» (PDF) . Архивировано из оригинала (обсуждение) 29 мая 2014 г. Проверено 03 марта 2013 г.
- Юэ, Жерар (1988). «Принципы индукции, формализованные в расчете конструкций» (PDF) . Ин Фучи, К.; Ниват, М. (ред.). Программирование компьютеров будущего поколения . Северная Голландия. стр. 205–216. ISBN 0444704108 . Архивировано из оригинала (PDF) 1 июля 2015 г. — Заявление КоК