Исчисление конструкций () — теория типов на основе полиморфного λ-исчисления высшего порядка с зависимыми типами, разработана Тьерри Коканом и Жераром Юэ в 1986 году. Находится в высшей точке лямбда-куба Барендрегта, являясь наиболее широкой из входящих в него систем — . Может быть применена как основа для построения типизированного языка программирования, так и в качестве системы конструктивных оснований математики.
Используется как базис для системы интерактивного доказательства Coq и ряда подобных инструментов (в том числе ).
Среди вариантов исчисления — исчисление индуктивных конструкцийИсчисление индуктивных конструкций , и в базовых стандартных библиотеках Coq: Datatypes and Logic . (использует индуктивные типы), исчисление коиндуктивных конструкций (с применением коиндукции), предикативное исчисление индуктивных конструкций (устраняет некоторую часть непредикативности).
С точки зрения соответствия Карри — Ховарда исчисление конструкций устанавливает взаимосвязь между зависимыми типами и доказательствами в секвенциальном интуиционистском исчислении предикатов.
Структура
Термы Терм в исчислении конструкций конструируется по следующим правилами:
T — это терм (так же его обозначают как Type); P — это терм (так же его обозначают как Prop, это — тип, к которому относятся все утверждения); Переменные (x, y, …) — это термы; Если A и B — это термы, то выражение (A B) также является термом; Если A и B — это термы и x — это переменная, то нижеследующие выражения также являются термами: (λx:A . B), (∀x:A . B).
Другими словами, синтаксис терма, если записать его при помощи BNF, следующий:
Исчисление конструкций использует пять типов объектов: доказательства, которые имеют типом те или иные утверждения; утверждения, также называемые малыми типами; предикаты, являющиеся функциями, возвращающими утверждения; большие типы, являющиеся типами для предикатов (P — пример такого большого типа); T как таковой, который является типом, к которому относятся большие типы.
Суждения Исчисление конструкций позволяет доказывать суждения о типах.
можно прочесть как импликацию:
Если переменные имеют типы , то терм имеет тип .
Допустимые суждения для исчисления конструкций могут быть получены из набора правил вывода. В дальнейшем мы используем символ чтобы обозначить последовательность присвоений типов , и K чтобы обозначить либо P либо T. Формула будет использоваться для замены терма для каждой свободной переменной в терме .
Правила вывода записываются в следующем формате:
это означает:
Если является валидным суждением, то
Правила вывода для исчисления конструкций 1.
2.
3.
4.
5.
Определение логических операторов Исчисление конструкций включает в себя совсем небольшое число основных операторов: единственный логический оператор для формирования утверждений . Однако одного этого оператора достаточно для определения всех других логических операторов:
Определение типов данных Исчисление конструкций позволяет определить базовые типы данных, используемые в информатике:
Булевы значения Натуральные числа Произведение Исключающее объединение (запись с вариантами)
Обратите внимания на то, что булевы и числовые значения определяются способом, аналогичным кодированию Чёрча. Однако дополнительные проблемы возникают из-за экстенсиональности утверждений и иррелевантности доказательств.
Примечания
Категория:Лямбда-исчисление Категория:Теория типов Категория:Программирование с зависимыми типами