WikiDer > Расчет конструкций

Calculus of constructions

В математическая логика и Информатика, то Расчет конструкций (CoC) это теория типов сделано Тьерри Кокванд. Он может служить как типизированным языком программирования, так и конструктивный фундамент математики. По этой второй причине CoC и его варианты были основой для Coq и другие помощники доказательства.

Некоторые из его вариантов включают Исчисление индуктивных построений.[1] (что добавляет индуктивные типы), исчисление (Co) индуктивных конструкций (которое добавляет коиндукция) и предсказательное исчисление индуктивных построений (которое устраняет некоторые непредсказуемость).

Общие черты

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

CoC - это сильно нормализующий, хотя доказать это свойство в рамках CoC невозможно, поскольку оно предполагает согласованность, которая Теорема Гёделя о неполноте невозможно доказать изнутри самой системы.

использование

CoC был разработан вместе с Coq помощник доказательства. По мере добавления функций (или устранения возможных недостатков) в теорию они стали доступны в Coq.

Варианты CoC используются в других помощниках по доказательству, таких как Матита.

Основы расчета конструкций

Исчисление конструкций можно рассматривать как расширение Изоморфизм Карри – Ховарда. Изоморфизм Карри – Ховарда связывает член в просто типизированное лямбда-исчисление с каждым доказательством естественного вывода в интуиционистская логика высказываний. Исчисление конструкций расширяет этот изоморфизм до доказательств в полном интуиционистском исчислении предикатов, которое включает в себя доказательства количественных утверждений (которые мы также будем называть «предложениями»).

Условия

А срок в Исчислении построений строится по следующим правилам:

  • это термин (также называемый Тип);
  • это термин (также называемый Опора, тип всех предложений);
  • Переменные () являются терминами;
  • Если и термины, то так ;
  • Если и условия и является переменной, то следующие термины также:
    • ,
    • .

Другими словами, синтаксис термина в BNF, затем:

Исчисление конструкций включает пять видов объектов:

  1. доказательства, которые являются терминами, типы которых предложения;
  2. предложения, которые также известны как маленькие типы;
  3. предикаты, которые являются функциями, возвращающими предложения;
  4. большие типы, которые являются типами предикатов ( пример большого шрифта);
  5. сам по себе, который является типом больших типов.

Суждения

Исчисление конструкций позволяет доказать печатать суждения:

Что можно прочитать как следствие

Если переменные иметь типы , то срок имеет тип .

Действительные суждения для исчисления построений выводятся из набора правил вывода. В дальнейшем мы используем означать последовательность присвоений типов ; означать термины; и иметь в виду либо или же . Напишем означать результат замены термина для свободной переменной в срок .

Правило вывода записывается в виде

что значит

Если верное суждение, то так

Правила вывода для исчисления конструкций

1.

2.

3.

4.

5.

6.

Определение логических операторов

В Исчислении построений очень мало основных операторов: единственный логический оператор для формирования предложений - это . Однако одного этого оператора достаточно для определения всех остальных логических операторов:

Определение типов данных

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

Булевы
Naturals
Товар
Несвязный союз

Обратите внимание, что логические и натуральные значения определяются так же, как в Церковная кодировка. Однако дополнительные проблемы возникают из-за пропозициональной протяженности и нерелевантности доказательства.[2]

Смотрите также

Рекомендации

  1. ^ Исчисление индуктивных конструкций, и базовые стандартные библиотеки: Типы данных и Логика.
  2. ^ "Стандартная библиотека | Помощник по проверке Coq". coq.inria.fr. Получено 2020-08-08.