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

---

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

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

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

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

Допустимые суждения для исчисления конструкций могут быть получены из набора правил вывода. В дальнейшем мы используем символ ${\displaystyle \Gamma }$ чтобы обозначить последовательность присвоений типов ${\displaystyle x_{1}:A_{1},x_{2}:A_{2},\ldots }$, и K чтобы обозначить либо P либо T. Формула ${\displaystyle B[x:=N]}$ будет использоваться для замены терма${\displaystyle N}$ для каждой свободной переменной ${\displaystyle x}$ в терме ${\displaystyle B}$.

1. ${\displaystyle {{} \over {}\Gamma \vdash P:T}}$

---