Интуиционистская теория типов - Intuitionistic type theory

Интуиционистская теория типов (также известная как теория конструктивных типов или теория типов Мартина-Лёфа ) - это теория типов и альтернативная основа математики . Интуиционистская теория типов была создана Пером Мартином-Лёфом , шведским математиком и философом , который впервые опубликовал ее в 1972 году. Существует несколько версий теории типов: Мартин-Лёф предложил как интенсиональный, так и экстенсиональный варианты теории и ранние импредикативные версии, доказанная парадоксом Жирара непоследовательность , уступила место предикативным версиям. Однако все версии сохраняют базовую конструкцию конструктивной логики с использованием зависимых типов.

Дизайн

Мартин-Лёф разработал теорию типов на принципах математического конструктивизма . Конструктивизм требует, чтобы любое доказательство существования содержало «свидетеля». Итак, любое доказательство того, что «существует простое число больше 1000», должно идентифицировать конкретное число, которое одновременно является простым и больше 1000. Интуиционистская теория типов достигла этой цели дизайна, усвоив интерпретацию BHK . Интересным следствием является то, что доказательства становятся математическими объектами, которые можно исследовать, сравнивать и манипулировать.

Конструкторы типов в интуиционистской теории типов были построены так, чтобы следовать взаимно однозначному соответствию с логическими связками. Например, логическая связка под названием импликация ( ) соответствует типу функции ( ). Это соответствие называется изоморфизмом Карри – Ховарда . Предыдущие теории типов также следовали этому изоморфизму, но Мартин-Лёф был первым, кто расширил его до логики предикатов , введя зависимые типы . ${\ displaystyle A \ подразумевает B}$${\ displaystyle от A \ до B}$

Теория типов

В интуиционистской теории типов есть 3 конечных типа, которые затем составляются с использованием 5 различных конструкторов типов. В отличие от теорий множеств, теории типов не строятся на логике, подобной логике Фреге . Итак, каждая особенность теории типов выполняет двойную функцию как функция как математики, так и логики.

Если вы не знакомы с теорией типов и знакомы с теорией множеств, краткое изложение: Типы содержат термины так же, как множества содержат элементы. Термины относятся к одному и только одному типу. Такие термины, как и вычисляют («сокращают») до канонических терминов, например 4. Подробнее см. В статье о теории типов .${\ displaystyle 2 + 2}$${\ displaystyle 2 \ cdot 2}$

0 тип, 1 тип и 2 типа

Есть 3 конечных типа: Тип 0 содержит 0 терминов. Тип 1 содержит 1 канонический термин. А 2-й тип содержит 2 канонических термина.

Поскольку тип 0 содержит 0 терминов, он также называется пустым типом . Он используется для обозначения всего, чего не может быть. Это тоже написано и представляет собой нечто недоказуемое. (. То есть, доказательство этого не может существовать) В результате, отрицание определяется как функция к нему: . ${\ displaystyle \ bot}$${\ displaystyle \ neg A: = A \ to \ bot}$

Точно так же тип 1 содержит 1 канонический термин и представляет существование. Его также называют типом агрегата . Он часто представляет собой утверждения, которые можно доказать, и поэтому иногда их можно записать . ${\ displaystyle \ top}$

Наконец, 2-й тип содержит 2 канонических термина. Он представляет собой определенный выбор между двумя ценностями. Он используется для логических значений, но не для предложений. Утверждения считаются 1-м типом, и может быть доказано, что у них никогда не будет доказательства ( тип 0 ), или они могут не быть доказаны в любом случае. ( Закон исключенного среднего не действует для предложений в интуиционистской теории типов.)

Конструктор типа Σ

Σ-типы содержат упорядоченные пары. Как и в случае типичной упорядоченной пары (или 2-кортежа) типов, A Σ-типа можно описать декартово произведение , , из двух других типов, и . Логически такая упорядоченная пара будет содержать доказательство и доказательство , поэтому можно увидеть такой тип, записанный как . ${\ displaystyle A \ times B}$${\ displaystyle A}$${\ displaystyle B}$${\ displaystyle A}$${\ displaystyle B}$${\ Displaystyle A \ клин B}$

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

${\ displaystyle \ sum _ {п {\ mathbin {:}} {\ mathbb {N}}} \ operatorname {Vec} ({\ mathbb {R}}, n)}$

Используя терминологию теории множеств, это похоже на индексированные непересекающиеся объединения множеств. В случае обычных упорядоченных пар тип второго члена не зависит от значения первого члена. Таким образом записывается тип, описывающий декартово произведение : ${\ Displaystyle {\ mathbb {N}} \ times {\ mathbb {R}}}$

${\ Displaystyle \ сумма _ {п {\ mathbin {:}} {\ mathbb {N}}} {\ mathbb {R}}}$

Здесь важно отметить, что значение первого члена не зависит от типа второго члена . ${\ displaystyle n}$${\ Displaystyle {\ mathbb {R}}}$

Очевидно, что Σ-типы можно использовать для создания более длинных кортежей с зависимым типом, используемых в математике, а также записей или структур, используемых в большинстве языков программирования. Примером 3-кортежа с зависимым типом являются два целых числа и доказательство того, что первое целое число меньше второго целого числа, описываемого типом:

${\ displaystyle \ sum _ {m {\ mathbin {:}} {\ mathbb {Z}}} {\ sum _ {n {\ mathbin {:}} {\ mathbb {Z}}} ((m <n) = {\ text {True}})}}$

Зависимая типизация позволяет Σ-типам выполнять роль квантора существования . Утверждение «существует тип , такой, который доказан» становится типом упорядоченных пар, где первый элемент является значением типа, а второй элемент является доказательством . Обратите внимание, что тип второго элемента (доказательства ) зависит от значения в первой части упорядоченной пары ( ). Его тип будет: ${\ displaystyle n}$${\ Displaystyle {\ mathbb {N}}}$${\ Displaystyle P (п)}$${\ displaystyle n}$${\ Displaystyle {\ mathbb {N}}}$${\ Displaystyle P (п)}$${\ Displaystyle P (п)}$${\ displaystyle n}$

${\ Displaystyle \ сумма _ {п {\ mathbin {:}} {\ mathbb {N}}} P (п)}$

Π конструктор типов

Π-типы содержат функции. Как и типичные типы функций, они состоят из типа ввода и типа вывода. Однако они более мощные, чем типичные типы функций, поскольку тип возвращаемого значения может зависеть от входного значения. Функции в теории типов отличаются от теории множеств. В теории множеств вы ищите значение аргумента в наборе упорядоченных пар. В теории типов аргумент заменяется термином, а затем к термину применяется вычисление («редукция»).

Например, записывается тип функции, которая по натуральному числу возвращает вектор, содержащий действительные числа: ${\ displaystyle n}$${\ displaystyle n}$

${\ displaystyle \ prod _ {п {\ mathbin {:}} {\ mathbb {N}}} \ operatorname {Vec} ({\ mathbb {R}}, n)}$

Когда тип вывода не зависит от входного значения, тип функции часто просто записывается с расширением . Таким образом, это тип функций от натуральных чисел к действительным числам. Такие Π-типы соответствуют логической импликации. Логическое предложение соответствует типу , содержащему функции, которые принимают доказательства A и возвращают доказательства B. Этот тип можно было бы более последовательно записать как: ${\ displaystyle \ to}$${\ displaystyle {\ mathbb {N}} \ to {\ mathbb {R}}}$${\ displaystyle A \ подразумевает B}$${\ displaystyle от A \ до B}$

${\ displaystyle \ prod _ {a {\ mathbin {:}} A} B}$

Π-типы также используются в логике для универсальной количественной оценки . Оператор «для каждого типа , доказан» становится функцией от типа доказательств . Таким образом, для данного значения функция генерирует доказательство, которое справедливо для этого значения. Тип будет ${\ displaystyle n}$${\ Displaystyle {\ mathbb {N}}}$${\ Displaystyle P (п)}$${\ displaystyle n}$${\ Displaystyle {\ mathbb {N}}}$${\ Displaystyle P (п)}$${\ displaystyle n}$${\ Displaystyle P ()}$

${\ Displaystyle \ prod _ {п {\ mathbin {:}} {\ mathbb {N}}} P (п)}$

= конструктор типа

= -типы создаются из двух терминов. Имея два термина, например и , вы можете создать новый тип . Члены этого нового типа представляют собой доказательства того, что пара сводится к одному и тому же каноническому члену. Таким образом, поскольку оба и вычисляют канонический член , будет термин типа . В интуиционистской теории типов существует единственный способ составить термины = -типы - рефлексивность : ${\ displaystyle 2 + 2}$${\ displaystyle 2 \ cdot 2}$${\ Displaystyle 2 + 2 = 2 \ cdot 2}$${\ displaystyle 2 + 2}$${\ displaystyle 2 \ cdot 2}$${\ displaystyle 4}$${\ Displaystyle 2 + 2 = 2 \ cdot 2}$

${\ displaystyle \ operatorname {refl} {\ mathbin {:}} \ prod _ {a {\ mathbin {:}} A} (a = a).}$

Можно создать = -типы, например, в которых термины не сводятся к одному и тому же каноническому термину, но вы не сможете создавать термины этого нового типа. Фактически, если бы вы могли создать термин , вы могли бы создать термин . Помещение этого в функцию сгенерирует функцию типа . Так как интуиционистская тип теории определяет отрицание, вы бы или, наконец, . ${\ displaystyle 1 = 2}$${\ displaystyle 1 = 2}$${\ displaystyle \ bot}$${\ displaystyle 1 = 2 \ to \ bot}$${\ displaystyle \ ldots \ to \ bot}$${\ Displaystyle \ neg (1 = 2)}$${\ displaystyle 1 \ neq 2}$

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

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

Индуктивные типы позволяют создавать сложные самореферентные типы. Например, связанный список натуральных чисел является либо пустым списком, либо парой натурального числа и другого связанного списка. Индуктивные типы могут использоваться для определения неограниченных математических структур, таких как деревья, графы и т. Д. Фактически, тип натуральных чисел может быть определен как индуктивный тип, являющийся либо преемником другого натурального числа. ${\ displaystyle 0}$

Индуктивные типы определяют новые константы, такие как ноль и функция-преемник . Поскольку не имеет определения и не может быть оценено с помощью подстановки, такие термины, как и, становятся каноническими терминами натуральных чисел. ${\ displaystyle 0 {\ mathbin {:}} {\ mathbb {N}}}$${\ Displaystyle S {\ mathbin {:}} {\ mathbb {N}} \ to {\ mathbb {N}}}$${\ displaystyle S}$${\ displaystyle S0}$${\ displaystyle SSS0}$

Доказательства индуктивных типов стали возможными благодаря индукции . Каждый новый тип индукции имеет собственное правило индукции. Чтобы доказать предикат для каждого натурального числа, вы используете следующее правило: ${\ Displaystyle P ()}$

${\ displaystyle {\ operatorname {{\ mathbb {N}} -elim}} \, {\ mathbin {:}} P (0) \, \ to \ left (\ prod _ {n {\ mathbin {:}} {\ mathbb {N}}} P (n) \ to P (S (n)) \ right) \ to \ prod _ {n {\ mathbin {:}} {\ mathbb {N}}} P (n) }$

Индуктивные типы в интуиционистской теории типов определяются в терминах W-типов, типа хорошо обоснованных деревьев. Более поздние работы в области теории типов привели к появлению коиндуктивных типов, индукции-рекурсии и индукции-индукции для работы с типами с более неясными видами самореферентности. Высшие индуктивные типы позволяют определять равенство между терминами.

Типы вселенной

Типы юниверса позволяют записывать доказательства для всех типов, созданных с помощью других конструкторов типов. Каждый термин в типе юниверса может быть сопоставлен с типом, созданным с помощью любой комбинации конструктора индуктивного типа. Однако, чтобы избежать парадоксов, нет термина в который сопоставляется . ${\ displaystyle {\ mathcal {U}} _ {0}}$${\ Displaystyle 0,1,2, \ Sigma, \ Pi, =,}$${\ displaystyle {\ mathcal {U}} _ {0}}$${\ displaystyle {\ mathcal {U}} _ {0}}$

Чтобы написать доказательства обо всех «малых типах» и , вы должны использовать , который содержит термин для , но не для самого себя . Аналогично для . Существует предикативная иерархия вселенных, поэтому для количественной оценки доказательства по любым фиксированным постоянным вселенным можно использовать . ${\ displaystyle {\ mathcal {U}} _ {0}}$${\ displaystyle {\ mathcal {U}} _ {1}}$${\ displaystyle {\ mathcal {U}} _ {0}}$${\ displaystyle {\ mathcal {U}} _ {1}}$${\ displaystyle {\ mathcal {U}} _ {2}}$${\ displaystyle k}$${\ displaystyle {\ mathcal {U}} _ {k + 1}}$

Типы вселенной - сложная особенность теорий типов. Первоначальную теорию типов Мартина-Лёфа пришлось изменить, чтобы учесть парадокс Жирара . Более поздние исследования охватывали такие темы, как «сверхвселенные», «много вселенных» и непредикативные вселенные.

Суждения

Формальное определение интуиционистской теории типов написано с использованием суждений. Например, в утверждении «если это тип, а это тип, то есть тип», есть суждения о том, что «это тип», «и», и «если ... то ...». Выражение не суждение; это определяемый тип. ${\ displaystyle A}$${\ displaystyle B}$${\ displaystyle \ textstyle \ sum _ {a: A} B}$${\ displaystyle \ textstyle \ sum _ {a: A} B}$

Этот второй уровень теории типов может сбивать с толку, особенно когда речь идет о равенстве. Существует суждение о равенстве сроков, которое можно было бы сказать . Это утверждение, что два термина сводятся к одному и тому же каноническому термину. Существует также суждение о равенстве типов, скажем так , что означает, что каждый элемент является элементом типа и наоборот. На уровне типа, есть тип , и он содержит термины , если есть доказательство того, что и сводятся к тому же значению. (Очевидно, что термины этого типа генерируются с использованием суждения о равенстве терминов.) Наконец, существует уровень равенства на английском языке, потому что мы используем слово «четыре» и символ « » для обозначения канонического термина . Подобные синонимы Мартин-Лёф назвал «по определению равными». ${\ Displaystyle 4 = 2 + 2}$${\ displaystyle A = B}$${\ displaystyle A}$${\ displaystyle B}$${\ Displaystyle 4 = 2 + 2}$${\ displaystyle 4}$${\ displaystyle 2 + 2}$${\ displaystyle 4}$${\ displaystyle SSSS0}$

Описание судебных решений, приведенное ниже, основано на обсуждениях, проведенных Нордстремом, Петерсоном и Смитом.

Формальная теория работает с типами и объектами .

Тип объявлен:

• ${\ Displaystyle A \ {\ mathsf {Тип}}}$

Объект существует и относится к типу, если:

• ${\ displaystyle a {\ mathbin {:}} A}$

Объекты могут быть равными

• ${\ displaystyle a = b}$

и типы могут быть равными

• ${\ displaystyle A = B}$

Объявляется тип, зависящий от объекта другого типа.

• ${\ Displaystyle (х {\ mathbin {:}} А) В}$

и удален заменой

• ${\ Displaystyle В [х / а]}$, заменяя переменную объектом в .${\ displaystyle x}$${\ displaystyle a}$${\ displaystyle B}$

Объект, который зависит от объекта другого типа, может быть создан двумя способами. Если объект «абстрагирован», то он записывается

• ${\ displaystyle [x] b}$

и удален заменой

• ${\ Displaystyle б [х / а]}$, заменяя переменную объектом в .${\ displaystyle x}$${\ displaystyle a}$${\ displaystyle b}$

Объект, зависящий от объекта, также может быть объявлен как константа как часть рекурсивного типа. Пример рекурсивного типа:

• ${\ Displaystyle 0 {\ mathbin {:}} \ mathbb {N}}$
• ${\ Displaystyle S {\ mathbin {:}} \ mathbb {N} \ to \ mathbb {N}}$

Здесь - постоянный объект, зависящий от объекта. Это не связано с абстракцией. Константы вроде можно удалить, задав равенство. Здесь связь с добавлением определяется с использованием равенства и сопоставления с образцом для обработки рекурсивного аспекта : ${\ displaystyle S}$${\ displaystyle S}$${\ displaystyle S}$

${\ displaystyle {\ begin {align} \ operatorname {add} & {\ mathbin {:}} \ (\ mathbb {N} \ times \ mathbb {N}) \ to \ mathbb {N} \\\ operatorname {add } (0, b) & = b \\\ operatorname {add} (S (a), b) & = S (\ operatorname {add} (a, b))) \ end {выровнено}}}$

${\ displaystyle S}$ манипулируется как непрозрачная константа - у нее нет внутренней структуры для подстановки.

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

${\ Displaystyle \ Gamma \ vdash \ sigma \ {\ mathsf {Тип}}}$	σ - правильно сформированный тип в контексте Γ.
${\ Displaystyle \ Gamma \ vdash т {\ mathbin {:}} \ sigma}$	t - это правильно сформированный терм типа σ в контексте Γ.
${\ Displaystyle \ Гамма \ vdash \ сигма \ экв \ тау}$	σ и τ являются одинаковыми типами в контексте Γ.
${\ Displaystyle \ Гамма \ vdash т \ экв {\ mathbin {:}} \ sigma}$	t и u суть равные члены типа σ в контексте Γ.
${\ Displaystyle \ vdash \ Gamma \ {\ mathsf {Контекст}}}$	Γ - это хорошо сформированный контекст предположений о типизации.

По соглашению существует тип, представляющий все остальные типы. Это называется (или ). Поскольку это тип, его члены являются объектами. Существует зависимый тип, который сопоставляет каждый объект с его соответствующим типом. В большинстве текстов никогда не написано. Из контекста утверждения читатель почти всегда может определить, относится ли он к типу или относится к объекту, который соответствует типу. ${\ displaystyle {\ mathcal {U}}}$${\ displaystyle \ operatorname {Set}}$${\ displaystyle {\ mathcal {U}}}$${\ displaystyle \ operatorname {El}}$${\ displaystyle \ operatorname {El}}$${\ displaystyle A}$${\ displaystyle {\ mathcal {U}}}$

Это полная основа теории. Все остальное выведено.

Для реализации логики каждому предложению дается свой тип. Объекты этих типов представляют различные возможные способы доказательства предложения. Очевидно, что если для предложения нет доказательства, то в типе нет объектов. Такие операторы, как «и» и «или», которые работают с предложениями, вводят новые типы и новые объекты. Так что это тип, который зависит от типа и типа . Объекты в этом зависимом типе определены как существующие для каждой пары объектов в и . Очевидно, что если или не имеет доказательства и является пустым типом, то представляющий новый тип также будет пустым. ${\ displaystyle A \ times B}$${\ displaystyle A}$${\ displaystyle B}$${\ displaystyle A}$${\ displaystyle B}$${\ displaystyle A}$${\ displaystyle B}$${\ displaystyle A \ times B}$

Это можно сделать для других типов (логические, натуральные числа и т. Д.) И их операторов.

Категориальные модели теории типов

Используя язык теории категорий , Р.А.Г. Сили ввел понятие локально декартовой замкнутой категории (LCCC) в качестве базовой модели теории типов. Это было усовершенствовано Хофманном и Дибьером до категорий с семействами или категорий с атрибутами на основе более ранней работы Картмелла.

Категория с семействами - это категория C контекстов (в которой объекты являются контекстами, а морфизмы контекста - подстановками) вместе с функтором T  : C ^op → Fam ( Set ).

Fam ( Set ) - это категория семейств множеств, в которой объекты представляют собой пары «индексного множества» A и функции B : X → A , а морфизмы - это пары функций f  : A → A ' и g  : X → X ' , такое что B' _° g = f _° B - другими словами, f отображает B _a в B _{g ( a )} . ${\ Displaystyle (А, В)}$

Функтор T присваивает контексту G набор типов и для каждого набора терминов. Аксиомы для функтора требуют, чтобы они гармонично играли с подстановкой. Замена обычно записываются в виде М или аф , где представляет собой тип , в и является членом в и е представляет собой замену от D до G . Вот и . ${\ Displaystyle Ty (G)}$${\ displaystyle A: Ty (G)}$${\ displaystyle Tm (G, A)}$${\ Displaystyle Ty (G)}$${\ displaystyle Tm (G, A)}$${\ displaystyle Af: Ty (D)}$${\ displaystyle af: Tm (D, Af)}$

Категория C должна содержать конечный объект (пустой контекст) и конечный объект для формы продукта, называемой пониманием или расширением контекста, в котором правый элемент является типом в контексте левого элемента. Если G - контекст, и , то среди контекстов D должен быть объект final с отображениями p  : D → G , q  : Tm ( D, Ap ). ${\ displaystyle A: Ty (G)}$${\ displaystyle (G, A)}$

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

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

Экстенсиональный против интенсионального

Фундаментальное различие между теорией экстенсионального и интенсионального типов. В экстенсиональной теории типов дефиниционное (т. Е. Вычислительное) равенство не отличается от пропозиционального равенства, которое требует доказательства. Как следствие, проверка типов становится неразрешимой в экстенсиональной теории типов, потому что программы в этой теории могут не завершаться. Например, такая теория позволяет придать тип Y-комбинатору , подробный пример этого можно найти в книге Нордстема и Петерсона « Программирование в теории типов Мартина-Лёфа» . Однако это не мешает теории экстенсиональных типов быть основой для практического инструмента, например, NuPRL основан на теории экстенсиональных типов.

В отличие от этого в интенсионального типа теории проверки типа является разрешимым , но представление стандартных математических понятий является несколько более громоздким, так как интенсиональная рассуждения требует использования setoids или аналогичных конструкций. Есть много общих математических объектов, с которыми трудно работать или которые не могут быть представлены без этого, например, целые числа , рациональные числа и действительные числа . Целые и рациональные числа могут быть представлены без сетоидов, но с этим представлением нелегко работать. Без этого нельзя представить действительные числа Коши.

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

Реализации теории типов

Различные формы теории типов были реализованы как формальные системы, лежащие в основе ряда вспомогательных средств доказательства . Хотя многие из них основаны на идеях Пера Мартин-Лёфа, многие из них содержат дополнительные особенности, аксиомы или другую философскую основу. Например, система NuPRL основана на теории вычислительного типа, а Coq - на исчислении (со) индуктивных конструкций . Зависимые типы также используются при разработке таких языков программирования , как ATS , Cayenne , Epigram , Agda и Idris .

Теории типа Мартина-Лёфа

Пер Мартин-Лёф построил несколько теорий типов, которые были опубликованы в разное время, некоторые из них намного позже, чем когда препринты с их описанием стали доступны специалистам (среди прочих Жан-Ив Жирар и Джованни Самбин). В приведенном ниже списке предпринята попытка перечислить все теории, которые были описаны в печатной форме, и очертить ключевые особенности, которые отличают их друг от друга. У всех этих теорий были зависимые произведения, зависимые суммы, непересекающиеся союзы, конечные типы и натуральные числа. Все теории имели одни и те же правила сокращения, которые не включали η-уменьшение ни для зависимых продуктов, ни для зависимых сумм, за исключением MLTT79, где добавлено η-уменьшение для зависимых продуктов.

MLTT71 был первой из теорий типов, созданных Пером Мартин-Лёфом. Он появился в препринте в 1971 году. У него была одна вселенная, но эта вселенная имела название сама по себе, то есть это была теория типов с, как ее сегодня называют, «Тип в типе». Жан-Ив Жирар показал, что эта система была непоследовательной, и препринт так и не был опубликован.

MLTT72 был представлен в препринте 1972 года, который сейчас опубликован. В этой теории была одна вселенная V и не было типов идентичности. Вселенная была «предикативной» в том смысле, что зависимый продукт семейства объектов из V над объектом, который не был в V, таким как, например, сам V, не предполагался находящимся в V. Вселенная была а ля Russell, т. Е. Можно было бы писать напрямую «T∈V» и «t∈T» (Мартин-Лёф использует знак «∈» вместо современного «:») без дополнительного конструктора, такого как «El».

MLTT73 был первым определением теории типов, опубликованным Пером Мартином-Лёфом (оно было представлено на Logic Colloquium 73 и опубликовано в 1975 году). Существуют типы идентичности, которые он называет «пропозициями», но, поскольку реального различия между пропозициями и остальными типами не вводится, значение этого неясно. Есть то, что позже получило название J-элиминатор, но пока без названия (см. Стр. 94–95). В этой теории существует бесконечная последовательность вселенных V ₀ , ..., V _n , .... Вселенные предсказуемы, а-ля Рассел и не суммируются ! Фактически, следствие 3.10 на с. 115 говорит, что если A∈V _m и B∈V _n таковы, что A и B конвертируемы, то m  =  n . Это означает, например, что в этой теории было бы сложно сформулировать однолистность - в каждом из V _i есть стягиваемые типы, но неясно, как объявить их равными, поскольку нет типов идентичности, связывающих V _i и V. _j для i ≠ j .

MLTT79 был представлен в 1979 году и опубликован в 1982 году. В этой статье Мартин-Лёф представил четыре основных типа суждений для теории зависимых типов, которая с тех пор стала фундаментальной в изучении метатеории таких систем. Он также ввел в нее контексты как отдельное понятие (см. С. 161). Существуют типы идентичности с J-элиминатором (который уже появился в MLTT73, но не имел там этого имени), но также с правилом, делающим теорию «экстенсиональной» (стр. 169). Есть W-типы. Существует бесконечная последовательность предикативных вселенных, которые накапливаются .

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

Смотрите также

• Интуиционистская логика
• Типизированное лямбда-исчисление

Заметки

Рекомендации

• Мартин-Лёф, Пер (1984). Интуиционистская теория типов (PDF) . Самбин, Джованни. Неаполь: Библиополь. ISBN 978-8870881059. OCLC  12731401 .

дальнейшее чтение

• Примечания Пера Мартин-Лёфа, записанные Джованни Самбином (1980)
• Нордстрём, Бенгт; Петерссон, Кент; Смит, Ян М. (1990). Программирование в теории типов Мартина-Лёфа . Издательство Оксфордского университета. ISBN 9780198538141.
• Томпсон, Саймон (1991). Теория типов и функциональное программирование . Эддисон-Уэсли. ISBN 0-201-41667-0.
• Гранстрем, Йохан Г. (2011). Трактат по интуиционистской теории типов . Springer. ISBN 978-94-007-1735-0.

Внешние ссылки

• EU Types Project: Tutorials - конспекты лекций и слайды из Летней школы Type 2005
• n-категории - набросок определения - письмо Джона Баэза и Джеймса Долана на Росс-стрит , 29 ноября 1995 г.