Исчисление построений

Традиционно, основания математики строятся следующим образом: берётся логика первого порядка, и дополняется отношениями и аксиомами, постулирующими, что некоторые объекты существуют и обладают требуемыми свойствами. Но хотя этот подход адекватен для создания теорий, способных выразить почти всю математику, он не вполне удовлетворителен с практической точки зрения.

Дело в том, что в построенной подобным образом теории, любое вычисление, даже столь простое как \(1+1 \longrightarrow 2\), должно быть выражено рассуждением, описывающим мельчайшие шаги вычисления. Как результат, любое нетривиальное доказательство огромно и непригодно для написания человеком.

Некоторые системы доказательства теорем решают эту проблему, генерирую части формального доказательства автоматически. Но мы подойдём иначе: обратив внимание на вычислительную природу самой логики, мы выведем исчисление, объединяющее вычисления и доказательства.

Для начала, вспомним естественный вывод. В нём мы выводили одни суждения из других согласно некоторому набору правил. Типичное суждение в естественном выводе имело вид:

\[{\color{red}A},{\color{red}B},\ldots ⊢ {\color{red}P}\]

Это суждение утверждает истинность \(\color{red}P\) в предположении истинности высказываний \({\color{red}A},{\color{red}B},\ldots\)

Правила, описывающие вывод заключения из посылок имели вид:

\[\frac{\mathcal J_1 \quad \dots \quad \mathcal J_n}{\mathcal C}\]

Сочетая различные правила друг с другом, мы строили дерево вывода, выражающее доказательство некоторого высказывания.

Доказательства, однако, являются внешними относительно правил вывода, так как суждения упоминают лишь сами высказывания, но не их доказательства.

Но доказательства в логике интереснее, чем высказывания. Поэтому интернализуем доказательства: вместо суждений об истинности высказываний рассмотрим суждения о том, что некоторые построения свидетельствуют об истинности некоторых высказываний.

Будем записывать суждение, что выражение \(\color{red}e\) свидетельствует об истинности \(\color{red}P\) как

\[⊢ {\color{red}e}: {\color{red}P}\]

Рассуждения могут использовать предположения, и, аналогично, свидетельство истинности высказывания может использовать гипотетические свидетельства истинности предположений. Эти свидетельства обозначаются переменными по левую сторону от турникета:

\[{\color{red}x}: {\color{red}A}, \ldots ⊢ {\color{red}e}: {\color{red}P}\]

Так как доказательство высказывания не должно зависеть от того, как именно будут доказаны предположения, только переменные используются на местах свидетельств в контексте.

Правила естественного вывода для предположений легко обобщаются в правила для гипотетических свидетельств:

\[\frac{}{\Gamma,\, {\color{red}x}:{\color{red}P} \vdash {\color{red}x}:{\color{red}P}} \qquad \frac{\Gamma \vdash {\color{red}e}:{\color{red}Q}}{\Gamma,\, {\color{red}x}:{\color{red}P} \vdash {\color{red}e}:{\color{red}Q}},\quad {\color{red}x} \mathbin{\#} Γ\]

Запись \({\color{red}x} \mathbin{\#} Γ\) означает, что переменная \(x\) не входит в \(Γ\). Смысл этих правил тот же, что и у правил естественного вывода: первое правило позволяет использовать гипотетические свидетельства, когда же второе позволяет их не использовать.

Перейдём к импликации. В естественном выводе мы формулировали правила введения и удаления импликации:

\[\cfrac{Γ,{\color{red}P} \vdash {\color{red}Q}}{Γ \vdash {\color{red}P} → {\color{red}Q}} \qquad \cfrac{Γ \vdash {\color{red}P} \qquad Γ\vdash {\color{red}P} → {\color{red}Q}}{Γ \vdash {\color{red}Q}}\]

Они обобщаются в следующие правила со свидетельствами:

\[\cfrac{Γ,\, {\color{red}x}:{\color{red}P} \vdash {\color{red}e}:{\color{red}Q}}{Γ \vdash (\lambda {\color{red}x}:{\color{red}P}.\; {\color{red}e}): {\color{red}P} → {\color{red}Q}} \qquad \cfrac{Γ \vdash {\color{red}v}:{\color{red}P} \qquad Γ\vdash {\color{red}f}: {\color{red}P} → {\color{red}Q}}{Γ \vdash ({\color{red}f\ v}):{\color{red}Q}}\]

В этих правилах мы ввели два новых построения: \(\lambda {\color{red}x}:{\color{red}P}.\; {\color{red}e}\) и \(\color{red}f\ v\). Их внешнее сходство с соответствующими выражениями лямбда-исчисления не случайно.

Вспомним, что последовательное введение и удаление импликации в доказательстве может быть редуцировано, при этом доказательство предположения подставляется в те места, где это предположение используется. Редукция лямбда-выражения также сводится к подстановке, только на этот раз выражения, к которому применяется функция, на места связанных переменных.

Чтобы увидеть это соответствие наглядно, вспомним пример редукции последовательного введения и удаления импликации:

Дереву вывода слева соответствует следующее дерево со свидетельствами:

Правому дереву же соответствует следующее дерево:

Можно видеть, что вывод импликации сопровождается построением соответствующего лямбда-выражения из его частей. И при редукции, подстановке поддерева соответствует подстановка выражения на места связанных переменных, а стиранию предположения — стирание связывающей переменной.

Доказательства по шагам можно также соотнести с построением соответствующего лямбда-выражения. Покажем это соответствие на примере доказательства следующего высказывания: если \(P → Q\), и если \(Q → R\), то тогда \(P → R\).

1. Пусть из \(P\) следует \(Q\) \(\quad [λpq: P → Q.]\)

   1. Пусть из \(Q\) следует \(R\) \(\quad [λqr: Q → R.]\)

      1. Пусть \(P\) \(\quad [λp: P.]\)

         1. Тогда \(Q\) \(\quad [pq\ p]\)

         2. И отсюда \(R\) \(\quad [qr\ (pq\ p)]\)

      2. Следовательно, \(P → R\)

   2. Следовательно, \((Q → R) → (P → R)\)

2. Следовательно, \((P → Q) → (Q → R) → (P → R)\)

Итоговое лямбда-выражение:

\[λpq: P → Q.\; λqr: Q → R.\; λp: P.\; qr\ (pq\ p)\]

Слову «пусть» соответствует введение лямбда-абстракции. Вывод следствие сопровождается построением выражения с помощью применения, а слово «следовательно» закрывает лямбда-абстракцию.

Если мы посмотрим на новые правила введения и удаления импликации внимательно, то обнаружим, что они не ограничиваются логикой. Они описывают построение и использование произвольных функций. Единственное различие между \(λ{\color{red}x}.\; {\color{red}e}\) и \(λ{\color{red}x} : {\color{red}P}.\; {\color{red}e}\) заключается в том, что если лямбда-функцию можно применить к любому значению, то функция \(λ{\color{red}x} : {\color{red}P}.\; {\color{red}e}\) применима лишь к значениям, построенным определённым образом.

Введём понятия, обобщающие всё сказанное. Будем называть типом класс значений по построению. Доказательство любого высказывания строится определённым образом, и любому доказательству соответствует единственное высказывание, которое оно доказывает. Поэтому любое высказывание является типом, а любое свидетельство истинности высказывания — значением соответствующего типа.

Если \({\color{red}σ}\) и \({\color{red}τ}\) это типы, то можно построить тип функций из \({\color{red}σ}\) в \({\color{red}τ}\), который записывается как \({\color{red}σ} → {\color{red}τ}\). Импликация \({\color{red}P} → {\color{red}Q}\) это частный случай типа функций, где типы \({\color{red}P}\) и \({\color{red}Q}\) являются высказываниями.

Суждение \(⊢ {\color{red}e}: {\color{red}τ}\) теперь утверждает, что \({\color{red}e}\) является значением типа \({\color{red}τ}\). Правила вывода таких суждений же называются правилами типизации. Эти правила выводят суждение о том, что некоторое значение имеет некоторый тип, и одновременно описывают построение корректного значения некоторого типа.

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

Тип, значениями которого являются другие типы, называется вселенной типов. Будем считать, что каждый тип является значением типа \(\mathcal U\).

Обобщив импликацию до функций, мы можем рассмотреть теперь функции типа \({\color{red}τ} → \mathcal U\). Такие функции естественно называть свойствами значения типа \({\color{red}τ}\), и им в математике соответствуют множества.

Свойства

Отвлечёмся от типов ради краткого введения в теорию множеств.

Множества состоят из элементов. Высказывание, что значение \(e\) является элементом множества \(S\) (или, по другому, принадлежит множеству \(S\)) записывается как \(e ∈ S\).

Множества определены тем, какие элементы им принадлежат. Два множества \(A\) и \(B\) равны, если любое значение \(e\) принадлежит \(A\) тогда и только тогда, когда оно принадлежит и \(B\).

Мы говорим, что множество \(A\) является (нестрогим) подмножеством множества \(B\) (записывается как \(A ⊆ B\)), если все элементы, что принадлежат \(A\), также принадлежат и \(B\). Ясно, что если \(A ⊆ B\) и \(B ⊆ A\), то тогда множества A и B равны.

Множество можно задать, перечислив его элементы в фигурных скобках. Например, множество, единственными элементами которого являются \(1\), \(2\) и \(3\) записывается как \(\{1,2,3\}\).

Запись \(\{\}\) означает множество, которому не принадлежит никакое значение. Оно называется пустым множеством и также обозначается как \(\varnothing\).

Множество можно задать логической формулой. Запись \(\{x \mid {\color{red}\phi} \}\) означает множество всех таких \(x\), для которых формула \(\phi\) истинна. Любое значение \(e\) принадлежит множеству \(\{x \mid {\color{red}\phi} \}\) тогда и только тогда, когда высказывание \({\color{red}\phi}[x := e]\) истинно.

Множества, задаваемые перечислением элементов, можно также задать и формулой. Например:

\[\{1,2,3\} = \{x \mid x = 1 ∨ x = 2 ∨ x = 3\}\]

Но выделение множеств с помощью формулы позволяет работать и с бесконечными множествами. Так, если \(ℕ\) это множество натуральных чисел, то тогда можно множество чётных натуральных чисел можно записать следующим образом:

\[\{n \mid ∃k.\; k ∈ ℕ ∧ n = 2k\}\]

Схему выделения множеств можно обобщить, позволив использовать слева от черты не только переменную, но и произвольное выражение, в которое переменная входит свободно:

\[\{f(x) \mid {\color{red}\phi}\} := \{y \mid ∃x.\; {\color{red}\phi} ∧ (y = f(x))\}\]

Эта запись позволяет записать множество чётных натуральных чисел как

\[\{2k \mid k ∈ ℕ\}\]

Ничем не ограниченная схема выделения множеств ведёт к теории, в которой выводимо любое утверждение. Пусть \(Q\) это произвольное высказывание. Рассмотрим множество

\[ω := \{x \mid (x ∈ x) → Q\}\]

В силу определения, для любого \(e\) верно

\[e ∈ \{x \mid x ∈ x → Q\} ↔ (e ∈ e → Q)\]

Однако, если мы возьмём в качестве элемента \(e\) само множество \(ω\)

\[ω ∈ ω ↔ (ω ∈ ω → Q)\]

Из этого утверждения следует истинность произвольного высказывания \(Q\). В частности, если вместо \(Q\) взять абсурд, то получится знаменитый парадокс Рассела.

Аксиоматическая теория множеств ограничивая схему выделения множеств, позволяя лишь выделять подмножества некоторых существующих множеств. Существование прочих множеств же гарантируется аксиомами.

Вернёмся к типам. Внимательный читатель, вероятно, заметил соответствие между множествами и лямбда-исчислением:

\[\begin{split}\begin{aligned} v ∈ \{x \mid {\color{red}\phi} \} &↔ {\color{red}\phi}[x := v]\\ (λx.\; {\color{red}\phi})\ v &\equiv {\color{red}\phi}[x := v] \end{aligned}\end{split}\]

В теории типов, аналогом множеств являются функции из \({\color{red}τ}\) в \(\mathcal U\), которые мы называем свойствами значения типа \({\color{red}τ}\). Типы иначе решают проблемы, связанные с неограниченным выделением множеств: мы не можем построить выражение \(x\ x\), так как ни одно значение не является одновременно и значением типа \({\color{red}τ}\), и значением типа \({\color{red}τ} → \mathcal U\).

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

\[\frac { Γ ⊢ \textcolor{red}e: \textcolor{red}α\qquad \textcolor{red}α \equiv \textcolor{red}β\qquad Γ ⊢ \textcolor{red}β: \mathcal U } {Γ ⊢ \textcolor{red}e:\textcolor{red}β}\]

Чтобы формулировать свойства, нам нужны логические связки и кванторы. Мы пока что типизировали лишь импликацию. Время перейти к квантору всеобщности.

Зависимые функции

Вспомним правила введения и удаления квантора всеобщности в естественном выводе:

\[\cfrac{Γ,{\color{red}x} \vdash {\color{red}\phi}}{Γ\vdash ∀{\color{red}x}.\;{\color{red}\phi}} \qquad \cfrac{Γ \vdash ∀{\color{red}x}.\;{\color{red}\phi}}{Γ \vdash {\color{red}\phi}[{\color{red}x} := {\color{red}t}]}\]

Дополнив их типами и свидетельствами, получаем:

\[\cfrac{Γ,\, {\color{red}x} : {\color{red}τ} \vdash {\color{red}e} : {\color{red}\phi}}{Γ\vdash (λ {\color{red}x} : {\color{red}τ}.\; {\color{red}e}) : (∀{\color{red}x} : {\color{red}τ}.\;{\color{red}\phi})} \qquad \cfrac{Γ \vdash {\color{red}v}: {\color{red}τ} \qquad Γ \vdash {\color{red} f}: ∀{\color{red}x} : {\color{red}τ}.\;{\color{red}\phi}} {Γ \vdash ({\color{red}f\ v}) : {\color{red}\phi}[{\color{red}x} := {\color{red}v}]}\]

Эти правила отличаются от правил типизации функций лишь тем, что тип результата может зависеть от значения, к которому применяется функция. Поэтому, будем называть тип \(∀{\color{red}x} : {\color{red}τ}.\;{\color{red}\phi}\) типом зависимых функций для \({\color{red}x}\) типа \({\color{red}τ}\) в \({\color{red}\phi}\). Правила будем называть, соответственно, правилами построения и разбора зависимых функций.

Обычные функции можно рассматривать как частный случай зависимых функций, где переменная при кванторе не используется. То есть, тип \({\color{red}σ} → {\color{red}τ}\) можно считать тем же типом, что и \(∀{\color{red}x}:{\color{red}σ}.\; {\color{red}τ}\), где переменная \({\color{red}x}\) не входит свободно в \({\color{red}τ}\).

Тип зависимых функций для \({\color{red}x}\) типа \({\color{red}τ}\) в \({\color{red}\phi}\) также записывается как \(({\color{red}x} : {\color{red}τ}) → {\color{red}\phi}\).

Зависимые функции позволяют формулировать высказывания про высказывания. Так, например, высказывание «для любых высказываний \(P\) и \(Q\), если \(P\), то тогда \(Q → P\)» можно записать как \(∀P\, Q:\mathcal U.\; P → (Q → P)\).

С помощью высказываний про высказывания можно выразить квантор всеобщности и все оставшиеся логические связки.

Чтобы показать это, докажем сначала следующее: любое высказывание \(P\) равносильно \(∀α:\mathcal U.\; (P → α) → α\). Сначала докажем, что из первого следует второе:

1. Пусть \(P\) это высказывание \(\quad[λP: \mathcal U.]\)

   1. Пусть \(P\) \(\quad[λp: P.]\)

      1. Пусть \(α\) это высказывание \(\quad[λα: \mathcal U.]\)

         1. Пусть из \(P\) следует \(α\) \(\quad[λf: P → α.]\)

            1. Тогда \(α\) \(\quad [f\ p]\)

         2. Следовательно, \((P → α) → α\)

      2. Следовательно, \(∀α: \mathcal U.\; (P → α) → α\)

   2. Следовательно, \(P → ∀α: \mathcal U.\; (P → α) → α\)

2. Следовательно, \(∀P: \mathcal U.\; P → ∀α: \mathcal U.\; (P → α) → α\)

Этому доказательству соответствует следующее свидетельство:

\[λP: \mathcal U.\; λp: P.\; λα: \mathcal U.\; λf: P → α.\; f\ p\]

Теперь докажем, что для любого высказывания \(P\), из \(∀α:\mathcal U.\; (P → α) → α\) следует \(P\).

1. Пусть \(P\) это высказывание \(\quad[λP: \mathcal U.]\)

   1. Пусть \(∀α:\mathcal U.\; (P → α) → α\) \(\quad[λf: (α:\mathcal U) → (P → α) → α.]\)

      1. Тогда \((P → P) → P\) \(\quad[f\ P]\)

      2. И отсюда \(P\) \(\quad[f\ P\ (λp:P.\; p)]\)

   2. Следовательно, \((∀α:\mathcal U.\; (P → α) → α) → P\)

2. Следовательно, \(∀P: \mathcal U.\; (∀α:\mathcal U.\; (P → α) → α) → P\)

Соответствующее выражение:

\[λP: \mathcal U.\; λf: (α:\mathcal U) → (P → α) → α.\; f\ P\ (λp:P.\; p)\]

Предположим, что мы каким-то образом определили высказывания \({\color{red}P} ∧ {\color{red}Q}\), \({\color{red}P} ∨ {\color{red}Q}\) и \(∃{\color{red}x}:{\color{red}τ}.\; {\color{red}\phi}\). Тогда в силу доказанного:

\[\begin{split}\begin{aligned} ({\color{red}P} ∧ {\color{red}Q}) &\leftrightarrow ∀α: \mathcal U.\; ({\color{red}P} ∧ {\color{red}Q} → α) → α \\ ({\color{red}P} ∨ {\color{red}Q}) &\leftrightarrow ∀α: \mathcal U.\; ({\color{red}P} ∨ {\color{red}Q} → α) → α \\ (∃{\color{red}x}:{\color{red}τ}.\; {\color{red}\phi}) &\leftrightarrow ∀α: \mathcal U.\; ((∃{\color{red}x}:{\color{red}τ}.\; {\color{red}\phi}) → α) → α \end{aligned}\end{split}\]

В естественном выводе для любых высказываний \({\color{red}P}\) и \({\color{red}Q}\), любой формулы \({\color{red}\phi}\) и любого высказывания \({\color{red}α}\), в которое переменная \(\color{red}x\) не входит свободно, можно доказать

\[\begin{split}\begin{aligned} ({\color{red}P} ∧ {\color{red}Q} → {\color{red}α}) &\leftrightarrow ({\color{red}P} → {\color{red}Q} → {\color{red}α}) \\ ({\color{red}P} ∨ {\color{red}Q} → {\color{red}α}) &\leftrightarrow ({\color{red}P} → {\color{red}α}) ∧ ({\color{red}Q} → {\color{red}α}) \\ ((∃{\color{red}x}.\; {\color{red}\phi}) → {\color{red}α}) &\leftrightarrow (∀{\color{red}x}.\; {\color{red}\phi} → {\color{red}α}) \end{aligned}\end{split}\]

Считая, что аналогичные высказывания верны и для типизированных высказываний, и комбинируя эквивалентности, получаем:

\[\begin{split}\begin{aligned} ({\color{red}P} ∧ {\color{red}Q}) &\leftrightarrow ∀α: \mathcal U.\; ({\color{red}P} → {\color{red}Q} → α) → α \\ ({\color{red}P} ∨ {\color{red}Q}) &\leftrightarrow ∀α: \mathcal U.\; ({\color{red}P} → α) → ({\color{red}Q} → α) → α \\ (∃{\color{red}x}: {\color{red}τ}.\; {\color{red}\phi}) &\leftrightarrow ∀α: \mathcal U.\; (∀{\color{red}x}: {\color{red}τ}.\; {\color{red}\phi} → α) → α \end{aligned}\end{split}\]

Эти эквивалентности можно рассматривать как определения конъюнкции, дизъюнкции и квантора существования.

Чтобы выразить отрицание, вспомним, что в естественном выводе мы определяли высказывание \(¬{\color{red}P}\) как \({\color{red}P} → ⊥\). Абсурд равносилен тому, что любое высказывание истинно, и, соответственно, высказывание \(¬{\color{red}P}\) можно определить как \({\color{red}P} → ∀α: \mathcal U.\; α\).

Исчисление построений

Мы почти закончили формулировать теорию типов. Осталось лишь сформулировать правила типизации самих типов.

Мы говорили, что каждый тип имеет тип \(\mathcal U\) и для любых двух типов \({\color{red}σ}\) и \({\color{red}τ}\) можно построить функцию \(({\color{red}x}: {\color{red}σ}) → {\color{red}τ}\). Это соответствует следующим правилам типизации:

\[\frac{}{Γ ⊢ \mathcal U : \mathcal U}\qquad \frac{Γ ⊢ {\color{red}σ}: \mathcal U \qquad Γ, ({\color{red}σ}: \mathcal U) ⊢ {\color{red}τ}: \mathcal U}{Γ ⊢ (∀{\color{red}x}: {\color{red}σ}.\; {\color{red}τ}) : \mathcal U}\]

Но добавив эти правила к остальным, мы получим формальную систему, в которой выводимо свидетельство любого высказывания. Конкретно, в ней можно построить парадокс, аналогичный парадоксу Бурали-Форти в теории множеств, который называется парадоксом Жирара. Этот парадокс слишком сложен, чтобы приводить его здесь.

Парадокс Жирара можно предотвратить следующим образом. Вместо единой вселенной всех типов, мы вводим бесконечную иерархию вселенных типов

\[\mathcal U_0 : \mathcal U_1 : \mathcal U_2 : \dots\]

И используем следующее правило типизации типов функций:

\[\frac{ Γ ⊢ {\color{red}σ}: \mathcal U_i \qquad Γ,({\color{red}x}: {\color{red}σ}) ⊢ {\color{red}τ}: \mathcal U_j }{Γ ⊢ (∀{\color{red}x}:{\color{red}σ}.\; {\color{red}τ}): \mathcal U_k},\quad k = imax(i,j)\]

Различные теории типов по разному определяют \(imax(i,j)\). В теории типов Мартина-Лёфа, это просто наибольший из двух индексов. Исчисление построений добавляет к этому определению одно исключение: \(imax(i, 0) = 0\).

В логике, определение какой-то множества называется непредикативным, если это определение включает квантификацию по определяемому множеству. В исчислении построений, значениями типа \(\mathcal U_0\) являются также типы вида \(∀{\color{red}α}: \mathcal U_0.\; {\color{red}β}\), и потому по аналогии \(\mathcal U_0\) называется непредикативной вселенной типов.

У непредикативности много следствий, разбор которых мы оставим на будущее. Сейчас нам необходимо знать лишь то, что \(\mathcal U_0\) является вселенной высказываний. Типы же остальных математических объектов принадлежат вселенной \(\mathcal U_1\) или выше.

Исчисление построений является основой той теории типов, которую мы будем использовать в будущем. Суммируем всё, что мы рассмотрели выше.

Синтаксис выражений исчисления построений:

\[\begin{split}\begin{aligned} {\color{red}lvl} ::=\ &0\ |\ 1\ |\ 2\ |\ \dots\\ {\color{red}expr} ::=\ &\mathcal{U}_{\color{red} lvl} & &\text{(вселенная)} \\ \mid\quad &∀\, {\color{red}var} : {\color{red}expr}\, .\ {\color{red}expr} & &\text{(тип функций)} \\ \mid\quad &{\color{red}var} & &\text{(переменная)} \\ \mid\quad &{\color{red}expr}\ {\color{red}expr} & &\text{(применение)} \\ \mid\quad &λ\, {\color{red}var} : {\color{red}expr}\, .\ {\color{red}expr} & &\text{(абстракция)} \end{aligned}\end{split}\]

Правило вычисления:

\[(λ\textcolor{red}x: \textcolor{red}τ.\;\textcolor{red}e)\ \textcolor{red}v \longrightarrow {\textcolor{red}e}[{\textcolor{red}x := {\textcolor{red}v}}]\]

Правила типизации:

• Вселенные:

\[\frac{}{Γ ⊢ \mathcal U_i : \mathcal U_{i + 1}}\]

• Предположения:

\[\frac{Γ \vdash {\color{red}τ}:\mathcal U_i}{\Gamma,\, {\color{red}x}:{\color{red}τ} \vdash {\color{red}x}:{\color{red}τ}} \qquad \frac{\Gamma \vdash {\color{red}e}:{\color{red}τ} \qquad Γ \vdash {\color{red}τ}:\mathcal U_i} {\Gamma,\, {\color{red}x}:{\color{red}σ} \vdash {\color{red}e}:{\color{red}τ}}, \qquad {\color{red}x} \mathbin\# Γ\]

• Тип зависимых функций:

\[\frac{ Γ ⊢ {\color{red}σ}: \mathcal U_i \qquad Γ,({\color{red}x}: {\color{red}σ}) ⊢ {\color{red}τ}: \mathcal U_j }{Γ ⊢ (∀{\color{red}x}:{\color{red}σ}.\; {\color{red}τ}): \mathcal U_k},\quad k = imax(i,j)\]

• Абстракция:

\[\frac { Γ,({\color{red}x}:{\color{red}σ}) ⊢ {\color{red}e}:{\color{red}τ} \qquad Γ ⊢ (∀{\color{red}x}:{\color{red}σ}.\;{\color{red}τ}):\mathcal U_i } {Γ ⊢ (λ{\color{red}x}:{\color{red}σ}.\;{\color{red}e}): (∀{\color{red}x}:{\color{red}σ}.\;{\color{red}τ}) }\]

• Применение:

\[\frac { Γ ⊢ {\color{red}f}:(∀{\color{red}x}:{\color{red}σ}.\;{\color{red}τ})\qquad Γ ⊢ {\color{red}v}:{\color{red}σ} } {Γ ⊢ ({\color{red} f\ v}): {\color{red}τ}[{\color{red}x} := {\color{red}v}]}\]

• Вычислительное равенство:

\[\frac { Γ ⊢ \textcolor{red}e: \textcolor{red}σ\qquad \textcolor{red}σ \equiv \textcolor{red}τ\qquad Γ ⊢ \textcolor{red}τ: \mathcal U_i} {Γ ⊢ \textcolor{red}e:\textcolor{red}τ}\]

Правила типизации стоит запомнить: они важны для понимания всего остального.

В выражениях и определениях, индекс при вселенной зачастую опускают, подразумевая либо конкретную вселенную, либо то, что определение применимо для любой вселенной типов.

Логика, выражаемая исчислением построений, является конструктивной. Однако, ничто не мешает дополнить исчисление правилом, постулирующим принцип двойного отрицания:

\[\frac{}{Γ ⊢ dne: ∀α: \mathcal U_0.\; ¬¬α → α}\]

Подобное правило, однако, ограничивает вычисление выражений, так как функция \(dne\) не может быть редуцирована.

Индуктивные типы

Математика начинается с натуральных чисел. Самый простой способ записать число это поставить столько отметок, сколько это число:

\[\begin{split}\begin{aligned} &0 & &\ \\ &1 & &| \\ &2 & &|| \\ &\cdots \end{aligned}\end{split}\]

В переводе на функции:

\[\begin{split}\begin{aligned} &0 & &zero \\ &1 & &succ\ zero \\ &2 & &succ\ (succ\ zero) \\ &\cdots \end{aligned}\end{split}\]

Константа \(zero : ℕ\) представляет собой нуль, когда же функция \(succ: ℕ → ℕ\) сопоставляет каждому натуральному числу непосредственно следующее за ним число. Будем называть \(zero\) и \(succ\) конструкторами натуральных чисел. Оставим вопрос об определении типа \(ℕ\) и значений \(zero\) и \(succ\) на потом, считая их данными.

С натуральными числами связан один из базовых математических принципов — принцип математической индукции. Он утверждает следующее. Пусть \(M\) это некоторое свойство натурального числа, и пусть верны следующие высказывания:

• База индукции: \(M\ 0\)

• Шаг индукции: для любого \(n : ℕ\), из \(M\ n\) следует \(M\ (succ\ n)\)

Тогда свойство \(M\) выполняется для любого натурального числа \(n\).

Почему это так? Обычно, индукцию поясняют следующим процессом. Мы знаем, что \(M\ 0\) истинно. Это влечёт за собой (индуцирует) истинность \(M\ 1\), которая в свою очередь влечёт за собой истинность \(M\ 2\), и так далее.

Таким образом свойство \(M\) доказывается для всех натуральных чисел: какое бы число \(n\) мы не взяли, когда-нибудь процесс индукции дойдёт и до \(M\ n\).

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

Возьмём произвольное число, скажем, \(3\). Для этого числа можно построить конечное доказательство \(M\ 3\), действуя следующим образом:

1. Так как для любого \(n\), из \(M\ n\) следует \(M\ (succ\ n)\), чтобы доказать \(M\ (succ\ (succ\ (succ\ zero)))\), достаточно доказать \(M\ (succ\ (succ\ zero))\)

2. Чтобы доказать \(M\ (succ\ (succ\ zero))\), достаточно доказать \(M\ (succ\ zero)\)

3. Чтобы доказать \(M\ (succ\ zero))\), достаточно доказать \(M\ zero\)

4. Но \(M\ zero\) это база индукции

Сведение задачи к меньшей разновидности той же задачи называется рекурсией. Построение доказательства \(M\ n\) является ярким её примером: мы сводим доказательство \(M\ n\), к доказательству \(M\ (n - 1)\), к доказательству \(M\ (n - 2)\) и так далее, пока не дойдём до \(M\ 0\).

Рассмотрим теперь этот процесс как функцию \(rec_ℕ\), которую будем называть рекурсором натуральных чисел. Она имеет тип, повторяющий принцип математической индукции:

\[\begin{split}\begin{aligned} rec_ℕ :\ &(M : ℕ → \mathcal U) → \\ &M\ 0 → (∀n: ℕ.\; M\ n → M\ (succ\ n)) → \\ &∀n: ℕ.\; M\ n \end{aligned}\end{split}\]

Функция \(M\) в типе функции \(rec_ℕ\) называется мотивом индукции. Её результатом не обязательно является высказывание.

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

\[\begin{split}\begin{aligned} (rec_ℕ\ M\ z\ s)\ zero &\equiv z \\ (rec_ℕ\ M\ z\ s)\ (succ\ n) &\equiv s\ n\ ((rec_ℕ\ M\ z\ s)\ n) \end{aligned}\end{split}\]

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

\[a + b := rec_ℕ\ (λn: ℕ.\; ℕ)\ a\ (λn: ℕ.\; λs: ℕ.\; succ\ s)\ b\]

Пусть \(a\) это натуральное число. Вычислим \(a + 2\):

\[\begin{split}\begin{aligned} a + 2 &\equiv rec_ℕ\ (λn: ℕ.\; ℕ)\ a\ (λn: ℕ.\; λs: ℕ.\; succ\ s)\ (succ\ (succ\ zero)) \\ &\equiv succ\ \big(rec_ℕ\ (λn: ℕ.\; ℕ)\ a\ (λn: ℕ.\; λs: ℕ.\; succ\ s)\ (succ\ zero)\big) \\ &\equiv succ\ \big(succ\ (rec_ℕ\ (λn: ℕ.\; ℕ)\ a\ (λn: ℕ.\; λs: ℕ.\; succ\ s)\ zero)\big) \\ &\equiv succ\ (succ\ a) \end{aligned}\end{split}\]

Мы ничего не сказали про тип \(ℕ\), кроме того, что для него существуют конструкторы и рекурсор. Могут ли существовать другие значения типа \(ℕ\)? Оказывается, что нет: используя индукцию, можно доказать, что любое значение типа \(ℕ\) либо равно \(zero\), либо равно \(succ\ n\), где \(n\) это другое значение типа \(ℕ\).

В свою очередь, описание рекурсора можно вывести из одних лишь конструкторов: полагая, что каждое значение типа \(ℕ\) равно равно значению, построенному с помощью применения конструкторов, можно записать соответствующие вычислительные равенства, которые в свою очередь однозначно определяют тип рекурсора.

Учитывая всё это, введём не вполне формальное определение: тип \(α\) называется индуктивным, если для него существует рекурсор над набором конструкторов \(c_1, \dots, c_n\).

Натуральные числа это индуктивный тип с конструкторами \(zero\) и \(succ\). Рассмотрим теперь другие примеры индуктивных типов.

Двоичные деревья

Двоичное дерево это индуктивный тип с конструкторами

\[lf: T \qquad br: T → T → T\]

Конструкторы \(lf\) и \(br\) выражают, соответственно, лист и ветвь дерева.

Значения типа \(T\) можно наглядно изобразить графически. Для примера, нарисуем \(br\ (br\ lf\ (br\ lf\ lf))\ lf\):

Выведем теперь описание рекурсора индуктивного типа \(T\). Он должен удовлетворять следующим равенствам:

\[\begin{split}\begin{aligned} (rec_T\ M\ l\ b)\ lf &\equiv l \\ (rec_T\ M\ l\ b)\ (br\ x\ y) &\equiv b\ x\ y\ ((rec_T\ M\ l\ b)\ x)\ ((rec_T\ M\ l\ b)\ y) \end{aligned}\end{split}\]

И потому имеет следующий тип:

\[\begin{split}\begin{aligned} rec_T :\ &(M: T → \mathcal U) → \\ &M\ lf → (∀x\, y: T.\; M\ x → M\ y → M\ (br\ x\ y)) → \\ &∀t:T.\; M\ t \end{aligned}\end{split}\]

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

\[fol := rec_T\ (λt:T.\; ℕ)\ 1\ (λx\,y: T.\; λl\,r: ℕ.\; l + r)\]

Вычислим количество листьев в \(br\ lf\ (br\ lf\ lf)\):

\[\begin{split}\begin{aligned} fol\ (br\ lf\ (br\ lf\ lf)) &\equiv (fol\ lf) + (fol\ (br\ lf\ lf)) \\ &\equiv 1 + ((fol\ lf) + (fol\ lf)) \\ &\equiv 1 + (1 + 1) \\ &\equiv 3 \end{aligned}\end{split}\]

Деревья бесконечной ширины

Рассмотрим индуктивный тип \(H\) со следующими конструкторами:

\[lf: H\qquad seg: H → H \qquad br: (ℕ → H) → H\]

Если в двоичных деревьях у \(br\) было два поддерева, то у дерева бесконечной ширины ветвь \(br\) сопоставляет каждому натуральному числу отдельное поддерево.

Простейшим примером такого дерева является следующее выражение:

\[br\ (rec_ℕ\ (λn: ℕ)\ lf\ (λn:ℕ.\; λs: H.\; seg\ s))\]

Его можно условно изобразить следующим образом:

Бесконечная ширина дерева, однако, не мешает записать правила вычисления для рекурсора:

\[\begin{split}\begin{aligned} (rec_H\ M\ l\ s\ b)\ lf &\equiv l \\ (rec_H\ M\ l\ s\ b)\ (seg\ x) &\equiv s\ x\ ((rec_H\ M\ l\ s\ b)\ x) \\ (rec_H\ M\ l\ s\ b)\ (br\ f) &\equiv b\ f\ (λn: ℕ.\; (rec_H\ M\ l\ s\ b)\ (f\ n)) \end{aligned}\end{split}\]

И вывести его тип:

\[\begin{split}\begin{aligned} rec_H:\ &(M : H → \mathcal U) → \\ &M\ lf → (∀h: H.\; M\ h → M\ (seg\ h)) → \\ &\big((f: ℕ → H) → ((n : ℕ) → M\ (f\ n)) → M\ (br\ f)\big) → \\ &∀h:H.\; M\ h \end{aligned}\end{split}\]

Поскольку мы не можем вычислить выражение для всех натуральных чисел, мы позволяем функции \(b\) выбрать нужное поддерево.

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

\[\begin{split}\begin{aligned} ldepth := rec_H\ &(λh: H.\; ℕ)\\ &0\ (λs: H.\; λd: ℕ.\; succ\ d)\\ &(λf: ℕ → H.\; λg: ℕ → ℕ.\; succ\ (g\ 0)) \end{aligned}\end{split}\]

Парадоксальный индуктивный тип

Не каждый индуктивный тип имеет право на существование. В качестве примера рассмотрим индуктивный тип \(B\) с единственным конструктором:

\[cu : (B → ⊥) → B\]

По аналогии с деревьями бесконечной ширины, рекурсор \(rec_B\) должен удовлетворять следующему вычислительному равенству:

\[(rec_B\ M\ c)\ (cu\ f) \equiv c\ f\ (λb:B.\; (rec_B\ M\ c)\ (f\ b))\]

И иметь следующий тип:

\[\begin{split}\begin{aligned} rec_B:\ &(M: B → \mathcal U) → \\ &\big((f: B → ⊥) → ((b: B) → M\ (f\ b)) → M\ (cu\ f)\big) → \\ &∀b:B.\; M\ b \end{aligned}\end{split}\]

Можно доказать абсурдность существования значения типа \(B\), построив функцию из \(B\) в \(⊥\):

\[ω := rec_B\ (λb: B.\; ⊥)\ (λf: B → ⊥.\; λo: Β → ⊥.\; o\ (cu\ o))\]

Однако

\[ω\ (cu\ ω) : ⊥\]

Парадокс, очевидно, вызван возможностью построить значение типа \(B\) из функции, предполагающей существование значения типа \(B\).

Списки

Список значений типа \(α\) это индуктивный тип \(List\ α\) со следующими конструкторами:

\[nil\ α : List\ α \qquad cons\ α: α → List\ α → List\ α\]

Это параметризованный индуктивный тип: подставляя различные типы на место \(α\), можно получить различные конкретные индуктивные типы. Функция \(List\) называется конструктором индуктивного типа.

Как и раньше, запишем вычислительные равенства для рекурсора:

\[\begin{split}\begin{aligned} (rec_{List}\ α\ M\ n\ c)\ (nil\ α) &\equiv n \\ (rec_{List}\ α\ M\ n\ c)\ (cons\ α\ x\ xs) &\equiv c\ x\ xs\ ((rec_{List}\ α\ M\ n\ c)\ xs) \end{aligned}\end{split}\]

И выведем его тип:

\[\begin{split}\begin{aligned} rec_{List}:\ &(α: \mathcal U) → (M: List\ α → \mathcal U) → \\ &M\ (nil\ α) → \\ &((x: α) → (xs: List\ α) → M\ xs → M\ (cons\ α\ x\ xs)) → \\ &∀l: List\ α.\; M\ l \end{aligned}\end{split}\]

Примером функции на списках является функция, вычисляющая длину списка:

\[len\ α := rec_{List}\ α\ (λl: List\ α.\; ℕ)\ 0\ (λx: α.\; λxs: List\ α.\; λl: ℕ.\; succ\ l)\]

В качестве упражнения, читатель может вычислить

\[len\ ℕ\ (cons\ ℕ\ 1\ (cons\ ℕ\ 3\ (cons\ ℕ\ 5\ (nil\ ℕ))))\]

Исчисление индуктивных построений

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

По этой причине, исчисление построений дополняют правилами, позволяющими вводить индуктивные типы. Исчисление вместе с этими правилами называется исчислением индуктивных построений.

Мы не будет рассматривать правила исчисления индуктивных построений, так как они технически сложны, и для использования средств доказательства теорем достаточно интуитивного понимания индуктивных типов. Тем не менее, нам необходимо обратить внимание на несколько тонкостей.

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

\[(x : {\color{red}σ_1}) → \dots → T\]

И если \(\color{red}σ_i\) имеет вид

\[(x : {\color{red}τ_1}) → \dots → T\]

То тогда \(T\) не входит ни в одно из \(\color{red}τ_i\).

Другие две тонкости связанны со вселенными типов. Индуктивный тип определяется в конкретной вселенной типов. Если другой тип является параметром, как \(α\) в \(List\ α\), то этот тип должен принадлежать вселенной, которая не выше той, что принадлежит параметризируемый индуктивный тип.

Если индуктивный тип \(T\) имеет тип \(\mathcal U_0\), то используемый рекурсором мотив также должен иметь тип \(\mathcal U_0\). То есть, например, если определён индуктивный тип \(Or\ P\ Q : \mathcal U_0\) с конструкторами

\[inl: P → Or\ P\ Q \qquad inr: Q → Or\ P\ Q\]

То тогда следующее выражение некорректно:

\[rec_{Or}\ P\ Q\ (λo: Or\ P\ Q.\; ℕ)\ (λp:P.\; 0)\ (λp:Q.\; 1)\]

Исключением из этого правила являются индуктивные типы, населённые единственным значением.

Причиной этого ограничения является парадокс Берарди, согласно которому непредикативность, принцип исключённого третьего и возможность различать два свидетельства истинности одного и того же высказывания не могут сосуществовать в одной теории типов.

Мы не рассмотрели ещё одну разновидность индуктивных типов — индуктивные семейства типов. С ними мы познакомимся в следующих главах.