Исчисление конструкций

Исчисление конструкций (англ. calculus of constructions, CoC) — теория типов на основе полиморфного λ-исчисления высшего порядка с зависимыми типами, разработана Тьерри Коканом и Жераром Юэ в 1986 году. Находится в высшей точке лямбда-куба Барендрегта, являясь наиболее широкой из входящих в него систем — . Может быть применена как основа для построения типизированного языка программирования, так и в качестве системы конструктивных оснований математики.

Используется как базис для системы интерактивного доказательства Coq и ряда подобных инструментов (в том числе Matita[англ.]).

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

С точки зрения соответствия Карри — Ховарда исчисление конструкций устанавливает взаимосвязь между зависимыми типами и доказательствами в секвенциальном интуиционистском исчислении предикатов.

Структура

Термы

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

  • T — это терм (так же его обозначают как Type);
  • P — это терм (так же его обозначают как Prop, это — тип, к которому относятся все утверждения);
  • Переменные (x, y, …) — это термы;
  • Если A и B — это термы, то выражение (A B) также является термом;
  • Если A и B — это термы и x — это переменная, то нижеследующие выражения также являются термами:
    • x:A . B),
    • (∀x:A . B).

Другими словами, синтаксис терма, если записать его при помощи BNF, следующий:

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

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

Суждения

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

можно прочесть как импликацию:

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

Допустимые суждения для исчисления конструкций могут быть получены из набора правил вывода. В дальнейшем мы используем символ чтобы обозначить последовательность присвоений типов , и K чтобы обозначить либо P либо T. Формула будет использоваться для замены терма для каждой свободной переменной в терме .

Правила вывода записываются в следующем формате:

это означает:

Если является валидным суждением, то

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

1.

2.

3.

4.

5.

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

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

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

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

Булевы значения
Натуральные числа
Произведение
Исключающее объединение (запись с вариантами)

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

Примечания

  1. Исчисление индуктивных конструкций Архивная копия от 10 июня 2020 на Wayback Machine, и в базовых стандартных библиотеках Coq: Datatypes Архивная копия от 10 июня 2020 на Wayback Machine and Logic Архивная копия от 10 июня 2020 на Wayback Machine.
  2. Standard Library | The Coq Proof Assistant. Дата обращения: 24 июня 2020. Архивировано 21 июля 2011 года.