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

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

Дизайн

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

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

Теория типов

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

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

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 type), или не может быть доказано в любом случае. (The Закон исключенного среднего не относится к предложениям интуиционистской теории типов.)

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

Σ-типы содержат упорядоченные пары. Как и в случае типичных упорядоченных парных (или двухкортежных) типов, Σ-тип может описывать Декартово произведение, ${ 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$

Зависимая типизация позволяет Σ-типам выполнять роль экзистенциальный квантор. Утверждение "существует ${ 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)}$

Когда тип вывода не зависит от входного значения, тип функции часто просто записывается с помощью ${ displaystyle to}$. Таким образом, ${ Displaystyle { mathbb {N}} to { mathbb {R}}}$ это тип функций от натуральных чисел до действительных чисел. Такие Π-типы соответствуют логической импликации. Логическое предложение ${ displaystyle A подразумевает B}$ соответствует типу ${ displaystyle от A до B}$, содержащий функции, которые принимают доказательства-оф-А и возвращают-доказательства-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 подразумевает бот}$. С ${ displaystyle ldots implies 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}$	т это хорошо сформированный термин типа σ в контексте Γ.
${ Displaystyle Гамма vdash сигма экв тау}$	σ и τ являются равными типами в контексте Γ.
${ Displaystyle Gamma vdash т экв { mathbin {:}} sigma}$	т и ты сужденно равны по типу σ в контексте Γ.
${ 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) в качестве базовой модели теории типов. Это было усовершенствовано Хофманном и Дибьером, чтобы Категории с семьей или же Категории с атрибутами основан на более ранней работе Картмелла.^[1]

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

Fam(Набор) это категория семей наборов, в которых объекты являются парами ${ Displaystyle (А, В)}$ "индексного набора" А и функция B: Икс → А, а морфизмы - это пары функций ж : А → А ' и грамм : Икс → ИКС' , так что B ' _° грамм = ж _° B - другими словами, ж карты B_а к B_{грамм(а)}.

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

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

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

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

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

Основное различие заключается в экстенсиональный против содержательный теория типов. В экстенсиональной теории типов дефиниционное (то есть вычислительное) равенство не отличается от пропозиционального равенства, которое требует доказательства. Как следствие, проверка типов становится неразрешимый в теории экстенсиональных типов, потому что программы в теории могут не завершаться. Например, такая теория позволяет дать тип Y-комбинатор, подробный пример этого можно найти в Nordstöm and Petersson Программирование в теории типов Мартина-Лёфа.^[2] Однако это не мешает теории экстенсиональных типов служить основой для практического инструмента, например, NuPRL основан на теории экстенсиональных типов.

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

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

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

Различные формы теории типов были реализованы как формальные системы, лежащие в основе ряда помощники доказательства. Хотя многие из них основаны на идеях Пера Мартина-Лёфа, многие из них содержат дополнительные особенности, аксиомы или другую философскую основу. Например, NuPRL система основана на вычислительная теория типов^[4] и Coq основан на исчисление (ко) индуктивных построений. Зависимые типы также есть в дизайне языки программирования Такие как ATS, Cayenne, Эпиграмма, Агда,^[5] и Идрис.^[6]

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

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

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

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

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

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

Библиополис: в книге «Библиополис» 1984 года обсуждается теория типов.^[10] но он в некоторой степени неограничен и, кажется, не представляет конкретный набор вариантов, поэтому с ним не связана какая-либо конкретная теория типов.

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

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

Примечания

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

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

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

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

внешняя ссылка

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