Введение
Альтернативное основание математики
Интуиционистская теория типов (также известная как конструктивная теория типов или теория типов Мартина Лёфа, последняя сокращается как MLTT) — это теория типов и альтернативное основание математики. Интуиционистская теория типов была создана шведским математиком и философом Пером Мартином Лёфом, который впервые опубликовал её в 1972 году. Существует несколько версий теории типов: Мартин Лёф предложил как интенсиональные, так и экстенсиональные варианты теории, а ранние импредикативные версии, оказавшиеся противоречивыми из-за парадокса Жирара, уступили место предикативным версиям. Однако все версии сохраняют базовую структуру конструктивной логики, использующей зависимые типы.
Intuitionistic type theory (also known as constructive type theory, or Martin Löf type theory, the latter abbreviated as MLTT) is a type theory and an alternative foundation of mathematics. Intuitionistic type theory was created by Per Martin Löf, a Swedish mathematician and philosopher, who first published it in 1972. There are multiple versions of the type theory: Martin Löf proposed both intensional and extensional variants of the theory and early impredicative versions, shown to be inconsistent by Girard's paradox, gave way to predicative versions. However, all versions keep the core design of constructive logic using dependent types.
Дизайн
Мартин Лёф разработал теорию типов, основываясь на принципах математического конструктивизма. Конструктивизм требует, чтобы любое доказательство существования содержало "свидетельство". Таким образом, любое доказательство утверждения "существует простое число больше 1000" должно указывать конкретное число, которое является одновременно простым и больше 1000. Интуиционистская теория типов достигла этой цели, интернализовав BHK-интерпретацию. Интересным следствием является то, что доказательства становятся математическими объектами, которые можно исследовать, сравнивать и преобразовывать. Конструкторы типов интуиционистской теории типов были разработаны для установления соответствия один к одному с логическими связками. Например, логическая связка, называемая импликацией, соответствует типу функции. Это соответствие называется изоморфизмом Карри — Ховарда. Предыдущие теории типов также следовали этому изоморфизму, но Мартин Лёф первым расширил его на логику предикатов, введя зависимые типы.
Теория типов
Интуиционистская теория типов имеет три конечных типа, которые затем составляются с использованием пяти различных конструкторов типов. В отличие от теорий множеств, теории типов не опираются на логику, подобную логике Фреге. Поэтому каждая особенность теории типов выполняет двойную роль, являясь особенностью как математики, так и логики. Если вы не знакомы с теорией типов, но знакомы с теорией множеств, краткое резюме таково: типы содержат термы, подобно тому как множества содержат элементы. Термы принадлежат ровно одному типу. Термы, такие как и , вычисляются ("приводятся") к каноническим термам, например, 4. Подробнее см. статью о теории типов.
0 тип, 1 тип и 2 тип
Существует три конечных типа: тип 0 содержит 0 термов. Тип 1 содержит 1 канонический терм. А тип 2 содержит 2 канонических терма. Поскольку тип 0 содержит 0 термов, он также называется пустым типом. Он используется для представления всего, что не может существовать. Он также записывается как ⊥ и представляет собой всё недоказуемое. (То есть, доказательства этого не может существовать.) В результате, отрицание определяется как функция в этот тип: ¬A ≡ A → ⊥. Аналогично, тип 1 содержит 1 канонический терм и представляет существование. Он также называется единичным типом. Часто он представляет собой утверждения, которые могут быть доказаны, и поэтому иногда записывается как ⊤. Наконец, тип 2 содержит 2 канонических терма. Он представляет собой однозначный выбор между двумя значениями. Он используется для булевых значений, но не для утверждений. Утверждения, вместо этого, представляются конкретными типами. Например, истинное утверждение может быть представлено типом 1, а ложное утверждение – типом 0. Однако мы не можем утверждать, что это единственные утверждения, то есть закон исключённого третьего не выполняется для утверждений в интуиционистской теории типов.
Likewise, the 1 type contains 1 canonical term and represents existence. It also is called the unit type. It often represents propositions that can be proven and is, therefore, sometimes written
Finally, the 2 type contains 2 canonical terms. It represents a definite choice between two values. It is used for Boolean values but not propositions. Propositions are instead represented by particular types. For instance, a true proposition can be represented by the 1 type, while a false proposition can be represented by the 0 type. But we cannot assert that these are the only propositions, i. e. the law of excluded middle does not hold for propositions in intuitionistic type theory.
Конструктор типа Σ
Типы Σ содержат упорядоченные пары. Как и в случае с типичными типами упорядоченных пар (или 2-кортежами), тип Σ может описывать декартово произведение двух других типов, , и логически такая упорядоченная пара будет содержать доказательство и доказательство , поэтому такой тип можно записать как. Типы Σ более мощные, чем типичные типы упорядоченных пар, благодаря зависимому типизированию. В упорядоченной паре тип второго элемента может зависеть от значения первого элемента. Например, первый элемент пары может быть натуральным числом, а тип второго элемента может быть последовательностью вещественных чисел длиной, равной первому элементу. Такой тип будет записан:
Σ types are more powerful than typical ordered pair types because of dependent typing. In the ordered pair, the type of the second term can depend on the value of the first term. For example, the first term of the pair might be a natural number and the second term's type might be a sequence of reals of length equal to the first term. Such a type would be written:
Используя терминологию теории множеств, это похоже на индексированное дизъюнктное объединение множеств. В случае обычных упорядоченных пар тип второго элемента не зависит от значения первого элемента. Таким образом, тип, описывающий декартово произведение , записывается:
Важно отметить, что значение первого элемента, , не влияет на тип второго элемента. Типы Σ могут использоваться для построения более длинных зависимо типизированных кортежей, используемых в математике, и записей или структур, используемых в большинстве языков программирования. Примером зависимо типизированного 3-кортежа являются два целых числа и доказательство того, что первое целое число меньше второго целого числа, описанное типом:
Σ types can be used to build up longer dependently typed tuples used in mathematics and the records or structs used in most programming languages. An example of a dependently typed 3 tuple is two integers and a proof that the first integer is smaller than the second integer, described by the type:
Зависимое типизирование позволяет типам Σ выполнять роль экзистенциального квантора. Утверждение "существует элемент типа , такой что доказано" становится типом упорядоченных пар, где первый элемент является значением типа , а второй элемент является доказательством . Обратите внимание, что тип второго элемента (доказательств) зависит от значения в первой части упорядоченной пары. Его тип будет:
= конструктор типа
= типы создаются из двух термов. Имея два терма, такие как α и β, можно создать новый тип α = β. Термы этого нового типа представляют собой доказательства того, что пара термов приводится к одному и тому же каноническому терму. Таким образом, поскольку оба терма α и β вычисляются в канонический терм γ, то будет существовать терм типа α = β. В интуиционистской теории типов существует единственный способ введения = типов, а именно посредством рефлексивности:
Возможно создать = типы, такие как α = β, где термы не приводятся к одному и тому же каноническому терму, но вы не сможете создать термы этого нового типа. Фактически, если бы вы могли создать терм для α = β, вы могли бы создать терм для β = α. Подстановка этого в функцию породит функцию типа (α = β) → (β = α). Поскольку в интуиционистской теории типов отрицание определяется как ¬A ≡ A → ⊥, у вас получится ⊥ или, наконец, false. Равенство доказательств – это область активных исследований в теории доказательств, которая привела к развитию теории гомотопии типов и других теорий типов.
Equality of proofs is an area of active research in proof theory and has led to the development of homotopy type theory and other type theories.
Индуктивные типы
Индуктивные типы позволяют создавать сложные, самореферентные типы. Например, связанный список натуральных чисел – это либо пустой список, либо пара, состоящая из натурального числа и другого связанного списка. Индуктивные типы могут использоваться для определения неограниченных математических структур, таких как деревья, графы и т.д. Фактически, тип натуральных чисел может быть определен как индуктивный тип, будучи либо нулем, либо следующим за другим натуральным числом. Индуктивные типы определяют новые константы, такие как ноль и функция следования. Поскольку ноль не имеет определения и не может быть вычислен посредством подстановки, такие термы, как ноль и следование от нуля, становятся каноническими термами натуральных чисел. Доказательства для индуктивных типов возможны с помощью индукции. Каждый новый индуктивный тип поставляется со своим собственным индуктивным правилом. Чтобы доказать предикат для всех натуральных чисел, используется следующее правило:
and become the canonical terms of the natural numbers. Proofs on inductive types are made possible by induction. Each new inductive type comes with its own inductive rule. To prove a predicate for every natural number, you use the following rule:
В интуиционистской теории типов индуктивные типы определяются через W-типы, тип хорошо обоснованных деревьев. Последующие работы в теории типов привели к созданию коиндуктивных типов, индукционной рекурсии и индукционной индукции для работы с типами, обладающими более сложными формами самореференциальности. Более высокие индуктивные типы позволяют определять равенство между термами.
Типы Вселенной
Типы вселенных позволяют строить доказательства для всех типов, созданных с помощью других конструкторов типов. Любой терм в типе вселенной может быть сопоставлен типу, созданному с помощью любой комбинации и индуктивного конструктора типа. Однако, чтобы избежать парадоксов, в типе вселенной нет терма, который сопоставляется с для любого . Для построения доказательств обо всех "малых типов" и необходимо использовать , который содержит терм для , но не для себя. Аналогично, для . Существует предикативная иерархия вселенных, поэтому для квантификации доказательства над любыми фиксированными константами вселенных можно использовать . Типы вселенных – это сложная особенность теории типов. Изначальная теория типов Мартина Лёфа была изменена с учетом парадокса Жирара. Последующие исследования охватывали такие темы, как "супервселенные", "вселенные Махло" и импредикативные вселенные.
To write proofs about all "the small types" and , you must use , which does contain a term for , but not for itself Similarly, for There is a predicative hierarchy of universes, so to quantify a proof over any fixed constant universes, you can use
Universe types are a tricky feature of type theories. Martin Löf's original type theory had to be changed to account for Girard's paradox. Later research covered topics such as "super universes", "Mahlo universes", and impredicative universes.
Экстенсионный и интенсионный
Основное различие заключается в экстенсиональной и интенсиональной теории типов. В экстенсиональной теории типов определение (т.е. вычислительное) равенство не различается с пропозициональным равенством, которое требует доказательства. Как следствие, проверка типов становится неразрешимой в экстенсиональной теории типов, поскольку программы в этой теории могут не завершаться. Например, такая теория позволяет присвоить тип комбинатору Y; подробный пример этого можно найти в книге Нордстрёма и Петерссона «Программирование в теории типов Мартина Лёфа». Однако это не препятствует использованию экстенсиональной теории типов в качестве основы для практических инструментов; например, Nuprl основан на экстенсиональной теории типов. В отличие от этого, в интенсиональной теории типов проверка типов разрешима, но представление стандартных математических концепций несколько более громоздко, поскольку интенсиональное рассуждение требует использования сетоидов или подобных конструкций. Многие распространенные математические объекты сложно использовать или невозможно представить без них, например, целые, рациональные и действительные числа. Целые и рациональные числа можно представить без сетоидов, но работа с таким представлением затруднена. Числа Коши действительных чисел не могут быть представлены без них. Теория гомотопии направлена на решение этой проблемы. Она позволяет определять высшие индуктивные типы, которые определяют не только конструкторы первого порядка (значения или точки), но и конструкторы высшего порядка, то есть равенства между элементами (пути), равенства между равенствами (гомотопии) и так далее до бесконечности.
Реализация теории типов
Различные формы теории типов были реализованы как формальные системы, лежащие в основе ряда систем доказательства теорем. Хотя многие из них основаны на идеях Пер Мартина Лёфа, многие из них дополнили их новыми возможностями, большим количеством аксиом или иной философской основой. Например, система Nuprl основана на вычислительной теории типов, а Coq — на исчислении (ко)индуктивных конструкций. Зависимые типы также применяются при разработке языков программирования, таких как ATS, Cayenne, Epigram, Agda и Idris.
Теории типов Мартина-Лёфа
Пер Мартин Лёф создал несколько теорий типов, которые были опубликованы в разное время, некоторые из них значительно позже, чем когда препринты с их описанием стали доступны специалистам (в частности, Жан-Иву Жирару и Джованни Самбину). Приведенный ниже список представляет собой попытку перечислить все теории, которые были описаны в печатной форме, и очертить ключевые особенности, которые их различают. Все эти теории имели зависимые произведения, зависимые суммы, дизъюнктные объединения, конечные типы и натуральные числа. Во всех теориях использовались одни и те же правила редукции, которые не включали η-редукцию ни для зависимых произведений, ни для зависимых сумм, за исключением MLTT79, где η-редукция для зависимых произведений была добавлена. MLTT71 была первой теорией типов, созданной Пером Мартином Лёфом. Она появилась в виде препринта в 1971 году. В ней была одна вселенная, но эта вселенная имела собственное имя, то есть это была теория типов, как её сегодня называют, с "Типом в Типе". Жан-Ив Жирар показал, что эта система была противоречивой, и препринт так и не был опубликован. MLTT72 была представлена в препринте 1972 года, который впоследствии был опубликован. Эта теория имела одну вселенную V и не содержала типов идентичности (= типов). Вселенная была "предикативной" в том смысле, что зависимое произведение семейства объектов из V по объекту, не входящему в V, например, самому V, не предполагалось входящим в V. Вселенная была в духе Principia Mathematica Рассела, то есть записывалось непосредственно "T∈V" и "t∈T" (Мартин Лёф использует знак "∈" вместо современного ":") без дополнительного конструктора, такого как "El". MLTT73 была первым определением теории типов, опубликованным Пером Мартином Лёфом (она была представлена на Логическом коллоквиуме '73 и опубликована в 1975 году). В ней присутствуют типы идентичности, которые он описывает как "высказывания", но поскольку реального различия между высказываниями и остальными типами не вводится, их значение неясно. Там есть то, что впоследствии получило название J-элиминатора, но пока без названия (см. стр. 94–95). В этой теории существует бесконечная последовательность вселенных V0, …, Vn. Вселенные предикативны, в духе Рассела и некумулятивны. Фактически, в следствии 3.10 на стр. 115 говорится, что если A∈Vm и B∈Vn таковы, что A и B конвертируемы, то m = n. Это означает, например, что было бы сложно сформулировать аксиому унивалентности в этой теории — в каждом из Vi есть сократимые типы, но неясно, как объявить их равными, поскольку нет типов идентичности, связывающих Vi и Vj для i ≠ j. MLTT79 была представлена в 1979 году и опубликована в 1982 году. В этой работе Мартин Лёф ввёл четыре основных типа суждений для теории зависимых типов, которые впоследствии стали фундаментальными в изучении метатеории таких систем. Он также ввёл контексты как отдельную концепцию (см. стр. 161). Присутствуют типы идентичности с J-элиминатором (который уже появился в MLTT73, но там не имел этого названия), а также правило, делающее теорию "экстенсиональной" (с. 169). Есть W-типы. Существует бесконечная последовательность предикативных вселенных, которые являются кумулятивными. Библиополис: в книге "Библиополис" 1984 года обсуждается теория типов, но она несколько открыта и, по-видимому, не представляет собой определённого набора выборов, поэтому с ней не связана какая-либо конкретная теория типов.
MLTT79 was presented in 1979 and published in 1982. In this paper, Martin Löf introduced the four basic types of judgement for the dependent type theory that has since become fundamental in the study of the meta theory of such systems. He also introduced contexts as a separate concept in it (see p. 161). There are identity types with the J eliminator (which already appeared in MLTT73 but did not have this name there) but also with the rule that makes the theory "extensional" (p. 169). There are W types. There is an infinite sequence of predicative universes that are cumulative. Bibliopolis: there is a discussion of a type theory in the Bibliopolis book from 1984, but it is somewhat open ended and does not seem to represent a particular set of choices and so there is no specific type theory associated with it.