Теория типов

«Теория типов» перенаправляется сюда. Архитектурный термин см. в разделе « Форма (архитектура) § Теории» .

В математике и теоретической информатике теория типов представляет собой формальное представление определенной системы типов . Теория типов — это академическое исследование систем типов.

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

• Типизированное λ-исчисление Алонзо Чёрча
• Интуиционистская теория типов Пера Мартина-Лёфа

Большинство компьютеризированных систем корректуры теорию типов используют в своей основе . Распространенным из них является » Тьерри Коканда «Исчисление индуктивных конструкций .

История

Основная статья: История теории типов

Теория типов была создана, чтобы избежать парадокса в математическом уравнении, основанном на наивной теории множеств и формальной логике . Парадокс Рассела (впервые описанный в книге Готлоба Фреге « Основы арифметики ») заключается в том, что без надлежащих аксиом можно определить множество всех множеств, которые не являются членами самих себя; это множество одновременно содержит себя и не содержит себя. Между 1902 и 1908 годами Бертран Рассел предлагал различные решения этой проблемы.

К 1908 году Рассел пришел к разветвленной теории типов вместе с аксиомой сводимости , обе из которых появились в и Рассела , Уайтхеда «Принципах математики» опубликованных в 1910, 1912 и 1913 годах. Эта система позволила избежать противоречий, предложенных в парадоксе Рассела, путем создания иерархию типов с последующим присвоением каждой конкретной математической сущности определенному типу. Сущности данного типа были построены исключительно из подтипов этого типа. тем самым предотвращая определение сущности с использованием самой себя. Это разрешение парадокса Рассела похоже на подходы, используемые в других формальных системах, таких как теория множеств Цермело-Френкеля .

Теория типов особенно популярна в сочетании с Алонзо Чёрча лямбда-исчислением . Одним из примечательных ранних примеров теории типов является просто типизированное лямбда-исчисление Чёрча . Теория типов Чёрча помог формальной системе избежать парадокса Клини-Россера , который затронул исходное нетипизированное лямбда-исчисление. Церковь продемонстрировала что она могла служить основой математики и называлась логикой высшего порядка .

В современной литературе «теория типов» относится к типизированной системе, основанной на лямбда-исчислении. Одной из влиятельных систем является Пера Мартина-Лёфа , интуиционистская теория типов которая была предложена в качестве основы конструктивной математики . Другим примером является Тьерри Кокана , конструктивное исчисление которое используется в качестве основы Коком , Лином и другими помощниками по компьютерному доказательству . Теория типов — активная область исследований, одним из направлений которой является развитие теории гомотопических типов .

Приложения

Математические основы

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

Математики, работающие над теорией категорий, уже сталкивались с трудностями при работе с широко признанной основой теории множеств Цермело-Френкеля . Это привело к появлению таких предложений, как «Элементарная теория категории множеств» Ловера (ETCS). Гомотопическая теория типов продолжает эту линию, используя теорию типов. Исследователи изучают связи между зависимыми типами (особенно тождественным типом) и алгебраической топологией (в частности, гомотопией ).

Помощники по доказательствам

Основная статья: Помощник по доказательствам

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

• LF используется Twelf часто для определения других теорий типов;
• многие теории типов, подпадающие под логику высшего порядка, используются семейством доказывающих устройств HOL и PVS ;
• теория вычислительных типов используется NuPRL ;
• исчисление конструкций и его производные используются Коком , Матитой и Лином ;
• UTT (Единая теория зависимых типов Ло) используется Agda , которая является одновременно языком программирования и помощником по доказательству.

Многие теории типов поддерживаются LEGO и Изабель . Помимо теорий типов, Изабель также поддерживает другие фонды, такие как ZFC . Мицар — пример системы доказательств, которая поддерживает только теорию множеств.

Языки программирования

Любой статический анализ программы , например алгоритмы проверки типов на семантического анализа этапе компилятора , связан с теорией типов. Ярким примером является Agda , язык программирования, который использует UTT (унифицированную теорию зависимых типов Луо) в качестве системы типов.

Язык программирования ML был разработан для манипулирования теориями типов (см. LCF ), и его собственная система типов находилась под их сильным влиянием.

Лингвистика

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

Наиболее распространенная конструкция включает основные типы. $e$ и $t$ для индивидуумов и истинностных значений соответственно и определяет набор типов рекурсивно следующим образом:

• если $a$ и $b$ являются типами, то и $\langle a,b\rangle$;
• ничего, кроме базовых типов, и то, что из них можно сконструировать с помощью предыдущего предложения, является типами.

Сложный тип $\langle a,b\rangle$ — это тип функций из сущностей типа $a$ к сущностям типа $b$. Таким образом, есть такие типы, как $\langle e,t\rangle$ которые интерпретируются как элементы множества функций от сущностей к истинностным значениям, т.е. индикаторные функции множеств сущностей. Выражение типа $\langle \langle e,t\rangle ,t\rangle$ - это функция от наборов сущностей к истинностным значениям, т.е. (индикаторная функция a) набора множеств. Этот последний тип обычно считается типом кванторов естественного языка , например, «все или никто» ( Montague 1973, Barwise and Cooper 1981).

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

Социальные науки

Грегори Бейтсон ввел в социальные науки теорию логических типов; его представления о двойной связке и логических уровнях основаны на теории типов Рассела.

Теория

Теория типов — это математическая логика , то есть совокупность правил вывода , которые приводят к суждениям . В большинстве логик есть суждения, утверждающие: « Предложение $\varphi$ верна» или « Формула $\varphi$ представляет собой корректную формулу ». В теории типов есть суждения, которые определяют типы и присваивают их набору формальных объектов, известных как термины. Термин и его тип часто пишутся вместе как $\mathrm {term} :{\mathsf {type}}$.

Условия

Термин в логике как рекурсивно определяется постоянный символ , переменная или приложение-функция , где термин применяется к другому термину. Постоянные символы могут включать натуральное число. $0$, логическое значение $\mathrm {true}$и такие функции, как функция-преемник $\mathrm {S}$ и условный оператор $\mathrm {if}$. Таким образом, некоторые термины могут быть $0$, $(\mathrm {S} \,0)$, $(\mathrm {S} \,(\mathrm {S} \,0))$, и $(\mathrm {if} \,\mathrm {true} \,0\,(\mathrm {S} \,0))$.

Решения

Большинство теорий типов имеют четыре суждения:

• " $T$ это тип "
• " $t$ это термин типа $T$"
• "Тип $T_{1}$ равно типу $T_{2}$"
• "Условия $t_{1}$ и $t_{2}$ оба типа $T$ равны »

Суждения могут следовать из предположений. Например, можно сказать: «Предполагая, что $x$ это термин типа ${\mathsf {bool}}$ и $y$ это термин типа ${\mathsf {nat}}$, отсюда следует, что $(\mathrm {if} \,x\,y\,y)$ это термин типа ${\mathsf {nat}}$". Такие суждения формально пишутся символом турникета $\vdash$.

$x:{\mathsf {bool}},y:{\mathsf {nat}}\vdash ({\textrm {if}}\,x\,y\,y):{\mathsf {nat}}$

Если нет предположений, то слева от турникета ничего не будет.

$\vdash \mathrm {S} :{\mathsf {nat}}\to {\mathsf {nat}}$

Список предположений слева представляет собой контекст решения. Заглавные греческие буквы, например $\Gamma$ и $\Delta$, являются распространенным выбором для представления некоторых или всех предположений. Таким образом, четыре различных решения обычно записываются следующим образом.

Официальная запись судебных решений	Описание
$\Gamma \vdash T$ Тип	$T$ является типом (при предположениях $\Gamma$).
$\Gamma \vdash t:T$	$t$ это термин типа $T$ (при предположениях $\Gamma$).
$\Gamma \vdash T_{1}=T_{2}$	Тип $T_{1}$ равно типу $T_{2}$ (при предположениях $\Gamma$).
$\Gamma \vdash t_{1}=t_{2}:T$	Условия $t_{1}$ и $t_{2}$ оба типа $T$ и равны (в предположениях $\Gamma$).

В некоторых учебниках используется тройной знак равенства. $\equiv$ подчеркнуть, что это равенство в суждениях и, следовательно, внешнее понятие равенства. Судебные решения предусматривают, что каждый термин имеет тип. Тип будет ограничивать правила, которые можно применять к термину.

Правила вывода

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

$${\begin{array}{c}\Gamma \vdash t:T_{1}\qquad \Delta \vdash T_{1}=T_{2}\\\hline \Gamma ,\Delta \vdash t:T_{2}\end{array}}$$

Правила являются синтаксическими и работают путем переписывания . Метапеременные ​ $\Gamma$, $\Delta$, $t$, $T_{1}$, и $T_{2}$ на самом деле может состоять из сложных терминов и типов, которые содержат множество применений функций, а не только отдельные символы.

Чтобы сгенерировать конкретное суждение в теории типов, должно существовать правило для его генерации, а также правила для генерации всех необходимых входных данных этого правила и так далее. Применяемые правила образуют дерево доказательства , где самые верхние правила не требуют допущений. Одним из примеров правила, не требующего каких-либо входных данных, является правило, определяющее тип постоянного термина. Например, чтобы утверждать, что существует термин $0$ типа ${\mathsf {nat}}$, можно было бы написать следующее.

$${\begin{array}{c}\hline \vdash 0:nat\\\end{array}}$$

Тип проживания

Основная статья: Тип проживания

Обычно желаемый вывод доказательства в теории типов — это вывод о обитаемости типов . Решение задачи типа проживания (сокращенно $\exists t.\Gamma \vdash t:\tau ?$) является:

Учитывая контекст $\Gamma$ и тип $\tau$, решить, существует ли термин $t$ которому можно присвоить тип $\tau$ в среде типа $\Gamma$.

Парадокс Жирара показывает, что обитаемость типов тесно связана с согласованностью системы типов с соответствием Карри-Ховарда. Чтобы быть здоровой, такая система должна иметь необитаемые типы.

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

• создать суждение ( известное как контекст ) в данном случае
• добавить предположение в контекст ( ослабление контекста )
• переставить предположения
• использовать предположение для создания переменной
• определить рефлексивность , симметрию и транзитивность для равенства суждений
• определить замену для применения лямбда-членов
• перечислить все взаимодействия равенства, такие как замена
• определить иерархию юниверсов типов
• утверждать существование новых типов

Кроме того, для каждого типа «по правилам» существует 4 разных типа правил.

• Правила «формирования типа» говорят, как создать тип.
• Правила «введения термина» определяют канонические термины и функции конструктора, такие как «пара» и «S».
• Правила «исключения терминов» определяют другие функции, такие как «первая», «вторая» и «R».
• Правила «вычислений» определяют, как выполняются вычисления с помощью функций, зависящих от типа.

За примерами правил заинтересованный читатель может обратиться к Приложению A.2 книги «Теория гомотопических типов» : или прочтите «Интуиционистскую теорию типов» Мартина-Лёфа.

Связь с фундаментами

Логическая структура теории типов имеет сходство с интуиционистской или конструктивной логикой. Формально теорию типов часто называют реализацией Брауэра-Хейтинга-Колмогорова . интерпретации интуиционистской логики Кроме того, можно установить связь с теорией категорий и компьютерными программами .

Интуиционистская логика

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

Согласно этой интуиционистской интерпретации, существуют общие типы, которые действуют как логические операторы:

Имя логики	Логическая запись	Обозначение типа	Тип Имя
Истинный	$\top$	$\top$	Тип устройства
ЛОЖЬ	$\bot$	$\bot$	Пустой тип
Импликация	$A\to B$	$A\to B$	Функция
Нет	$\neg A$	$A\to \bot$	Функция для очистки типа
И	$A\land B$	$A\times B$	Тип продукта
Или	$A\lor B$	$A+B$	Тип суммы
Для всех	$\forall a\in A,P(a)$	$\Pi a:A.P(a)$	Зависимый продукт
Существует	$\exists a\in A,P(a)$	$\Sigma a:A.P(a)$	Зависимая сумма

Поскольку закон исключенного третьего не выполняется, не существует термина типа. $\Pi a.A+(A\to \bot )$. Аналогично, двойное отрицание не выполняется, поэтому не существует термина типа $\Pi A.((A\to \bot )\to \bot )\to A$.

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

Конструктивная математика

Пер Мартин-Лёф предложил свою интуиционистскую теорию типов в качестве основы конструктивной математики . Конструктивная математика требует при доказательстве «существования существования $x$ с недвижимостью $P(x)$", необходимо построить конкретный $x$ и доказательство наличия у него собственности $P$. В теории типов существование осуществляется с использованием зависимого типа продукта, и его доказательство требует термина этого типа.

Примером неконструктивного доказательства является доказательство от противного . Первый шаг предполагает, что $x$ не существует и опровергая его от противного. Вывод из этого шага таков: «Это не тот случай, когда $x$ не существует". Последний шаг - путем двойного отрицания заключить, что $x$ существует. Конструктивная математика не позволяет на последнем этапе устранения двойного отрицания прийти к выводу, что $x$ существует.

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

-

Соответствие Карри-Ховарда — это наблюдаемое сходство между логикой и языками программирования. Импликация в логике: «А $\to$ B» напоминает функцию от типа «A» до типа «B». Для разнообразной логики правила аналогичны выражениям в типах языка программирования. Сходство идет еще дальше, поскольку приложения правил напоминают программы на языках программирования. Таким образом, переписку часто резюмируют как «доказательства как программы».

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

Вывод типа

Основная статья: Вывод типа

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

Области исследований

Теория категорий

Основная статья: Теория категорий

Хотя первоначальная мотивация теории категорий была далека от фундаментализма, оказалось, что эти две области имеют глубокие связи. Как пишет Джон Лейн Белл : «Фактически категории сами по себе могут рассматриваться как теории типов определенного типа; один этот факт указывает на то, что теория типов гораздо более тесно связана с теорией категорий, чем с теорией множеств». Короче говоря, категорию можно рассматривать как теорию типов, рассматривая ее объекты как типы (или сорта), т.е. «Грубо говоря, категорию можно рассматривать как теорию типов, лишенную ее синтаксиса». Таким образом, достигается ряд важных результатов:

• декартовы замкнутые категории соответствуют типизированному λ-исчислению ( Ламбек , 1970);
• C-моноиды (категории с произведениями и экспонентами и одним нетерминальным объектом) соответствуют нетипизированному λ-исчислению (наблюденному независимо Ламбеком и Даной Скотт около 1980 года);
• локально декартовы замкнутые категории соответствуют теориям типа Мартина-Лёфа (Seely, 1984).

С тех пор взаимодействие, известное как категориальная логика , стало предметом активных исследований; см., например, монографию Джейкобса (1999).

Теория

Гомотопическая теория типов пытается объединить теорию типов и теорию категорий. Основное внимание уделяется равенствам, особенно равенствам между типами. Теория гомотопических типов отличается от интуиционистской теории типов главным образом тем, что в ней рассматривается тип равенства. В 2016 году была предложена теория кубического типа , представляющая собой теорию гомотопического типа с нормализацией.

Определения

Термины и типы

Атомарные термины

Самые основные типы называются атомами, а термин, тип которого является атомом, известен как атомарный терм. Общие атомарные термины, включенные в теории типов, представляют собой натуральные числа , часто обозначаемые типом ${\mathsf {nat}}$, значения логической логики ( $\mathrm {true}$/ $\mathrm {false}$), обозначенный типом ${\mathsf {bool}}$и формальные переменные , тип которых может различаться. Например, следующее может быть атомарными терминами.

• $42:{\mathsf {nat}}$
• $\mathrm {true} :{\mathsf {bool}}$
• $x:{\mathsf {nat}}$
• $y:{\mathsf {bool}}$

Функциональные термины

Помимо атомарных терминов, большинство современных теорий типов также допускают функции . Типы функций обозначаются стрелкой и определяются индуктивно : Если $\sigma$ и $\tau$ являются типами, то обозначение $\sigma \to \tau$ — это тип функции, которая принимает параметр типа $\sigma$ и возвращает термин типа $\tau$. Типы этой формы известны как простые типы .

Некоторые термины могут быть объявлены напрямую как имеющие простой тип, например следующий термин: $\mathrm {add}$, который принимает два последовательных натуральных числа и возвращает одно натуральное число.

$\mathrm {add} :{\mathsf {nat}}\to ({\mathsf {nat}}\to {\mathsf {nat}})$

Строго говоря, простой тип допускает только один вход и один выход, поэтому более точное прочтение вышеуказанного типа заключается в следующем: $\mathrm {add}$ — это функция, которая принимает натуральное число и возвращает функцию вида ${\mathsf {nat}}\to {\mathsf {nat}}$. В скобках поясняется, что $\mathrm {add}$ не имеет типа $({\mathsf {nat}}\to {\mathsf {nat}})\to {\mathsf {nat}}$, которая будет функцией, которая принимает функцию натуральных чисел и возвращает натуральное число. Соглашение заключается в том, что стрелка является правоассоциативной , поэтому круглые скобки можно опустить. $\mathrm {add}$тип.

Лямбда-термины

Новые функциональные термины могут быть созданы с использованием лямбда-выражений и называются лямбда-термами. Эти термины также определяются индуктивно: лямбда-терм имеет вид $(\lambda v.t)$, где $v$ является формальной переменной и $t$ это термин, и его тип обозначен $\sigma \to \tau$, где $\sigma$ это тип $v$, и $\tau$ это тип $t$. Следующий лямбда-терм представляет функцию, которая удваивает входное натуральное число.

$(\lambda x.\mathrm {add} \,x\,x):{\mathsf {nat}}\to {\mathsf {nat}}$

Переменная $x$ и (неявно из типа лямбда-терма) должен иметь тип ${\mathsf {nat}}$. Термин $\mathrm {add} \,x\,x$ имеет тип ${\mathsf {nat}}$, что можно увидеть, дважды применив правило вывода приложения функции. Таким образом, лямбда-терм имеет тип ${\mathsf {nat}}\to {\mathsf {nat}}$, что означает, что это функция, принимающая натуральное число в качестве аргумента и возвращающая натуральное число.

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

Правила вывода

Применение функции

Сила теорий типов заключается в определении того, как термины могут быть объединены посредством правил вывода . Теории типов, в которых есть функции, также имеют правило вывода применения функций : если $t$ это термин типа $\sigma \to \tau$, и $s$ это термин типа $\sigma$, то применение $t$ к $s$, часто пишут $(t\,s)$, имеет тип $\tau$. Например, если известны обозначения типов $0:{\textsf {nat}}$, $1:{\textsf {nat}}$, и $2:{\textsf {nat}}$ следующие обозначения типов . можно вывести , то из применения функции

• $(\mathrm {add} \,1):{\textsf {nat}}\to {\textsf {nat}}$
• $((\mathrm {add} \,2)\,0):{\textsf {nat}}$
• $((\mathrm {add} \,1)((\mathrm {add} \,2)\,0)):{\textsf {nat}}$

Круглые скобки указывают порядок действий ; однако по соглашению приложение функции остается ассоциативным , поэтому при необходимости круглые скобки можно опустить. В случае трех приведенных выше примеров все круглые скобки в первых двух можно опустить, а третий можно упростить до $\mathrm {add} \,1\,(\mathrm {add} \,2\,0):{\textsf {nat}}$.

Сокращения

Теории типов, допускающие использование лямбда-членов, также включают правила вывода, известные как $\beta$-сокращение и $\eta$-снижение. Они обобщают понятие применения функции на лямбда-термины. Символически они пишутся

• $(\lambda v.t)\,s\rightarrow t[v\colon =s]$ ( $\beta$-снижение).
• $(\lambda v.t\,v)\rightarrow t$, если $v$ не является свободной переменной в $t$ ( $\eta$-снижение).

Первое сокращение описывает, как оценить лямбда-терм: если лямбда-выражение $(\lambda v.t)$ применяется к термину $s$, заменяется каждое вхождение $v$ в $t$ с $s$. Второе сокращение делает явной связь между лямбда-выражениями и типами функций: if $(\lambda v.t\,v)$ это лямбда-терм, то должно быть так $t$ является функциональным термином, поскольку он применяется к $v$. Следовательно, лямбда-выражение эквивалентно просто $t$, поскольку оба принимают один аргумент и применяют $t$ к этому.

Например, следующий термин может быть $\beta$-уменьшенный.

$(\lambda x.\mathrm {add} \,x\,x)\,2\rightarrow \mathrm {add} \,2\,2$

В теориях типов, которые также устанавливают понятия равенства типов и термов, существуют соответствующие правила вывода $\beta$-равенство и $\eta$-равенство.

Общие термины и типы

Пустой тип

не Пустой тип имеет терминов. Тип обычно пишется $\bot$ или $\mathbb {0}$. Одно из применений пустого типа — доказательство существования типа . Если для типа $a$, то последовательно вывести функцию типа $a\to \bot$, затем $a$ необитаем , то есть не имеет условий.

Тип юнита

Тип единицы имеет ровно 1 канонический термин. Тип написан $\top$ или $\mathbb {1}$ и записывается единственный канонический термин $\ast$. Тип объекта также используется в доказательствах типа проживания. Если для типа $a$, то последовательно вывести функцию типа $\top \to a$, затем $a$ является обитаемым , то есть должно иметь один или несколько членов.

Логический тип

Булев тип имеет ровно два канонических термина. Тип обычно пишется ${\textsf {bool}}$ или $\mathbb {B}$ или $\mathbb {2}$. Канонические термины обычно $\mathrm {true}$ и $\mathrm {false}$.

Натуральные числа

Натуральные числа обычно реализуются в стиле арифметики Пеано . Есть канонический термин $0:{\mathsf {nat}}$ за ноль. Канонические значения больше нуля используют повторяющиеся применения функции -преемника. $\mathrm {S} :{\mathsf {nat}}\to {\mathsf {nat}}$.

Зависимая типизация

Некоторые теории типов допускают, что типы сложных терминов, таких как функции или списки, зависят от типов их аргументов. Например, теория типов может иметь зависимый тип ${\mathsf {list}}\,a$, что должно соответствовать спискам терминов, где каждый термин должен иметь тип $a$. В этом случае, ${\mathsf {list}}$ имеет тип $U\to U$, где $U$ обозначает вселенную всех типов в теории.

Некоторые теории также допускают, что типы зависят от терминов, а не от типов. Например, теория может иметь тип ${\mathsf {vector}}\,n$, где $n$ это термин типа ${\mathsf {nat}}$ кодирование длины вектора . Это обеспечивает большую специфичность и безопасность типов : функции с ограничениями длины вектора или требованиями соответствия длины, такие как скалярное произведение , могут кодировать это требование как часть типа.

Существуют фундаментальные проблемы, которые могут возникнуть из-за зависимых типов, если теория не уделяет должного внимания тому, какие зависимости разрешены, например, парадокс Жирара . Логик Хенк Барендегт представил лямбда-куб как основу для изучения различных ограничений и уровней зависимой типизации.

Тип продукта

Тип продукта зависит от двух типов, и его условия обычно записываются в виде упорядоченных пар. $(s,t)$ или с символом $\times$. Пара $(s,t)$ имеет тип продукта $\sigma \times \tau$, где $\sigma$ это тип $s$ и $\tau$ это тип $t$. Тип продукта обычно определяется с помощью функций-элиминаторов. $\mathrm {first} :(\Pi \,\sigma \,\tau .\sigma \times \tau \to \sigma )$ и $\mathrm {second} :(\Pi \,\sigma \,\tau .\sigma \times \tau \to \tau )$.

• $\mathrm {first} \,(s,t)$ возвращает $s$, и
• $\mathrm {second} \,(s,t)$ возвращает $t$.

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

Тип суммы

Тип суммы зависит от двух типов и обычно обозначается символом $+$ или $\sqcup$. В языках программирования типы сумм могут называться тегированными объединениями . Тип $\sigma \sqcup \tau$ обычно определяется с помощью конструкторов $\mathrm {left} :\sigma \to (\sigma \sqcup \tau )$ и $\mathrm {right} :\tau \to (\sigma \sqcup \tau )$, которые являются инъективными , и исключающую функцию $\mathrm {match} :(\Pi \,\rho .(\sigma \to \rho )\to (\tau \to \rho )\to (\sigma \sqcup \tau )\to \rho )$ такой, что

• $\mathrm {match} \,f\,g\,(\mathrm {left} \,x)$ возвращает $f\,x$, и
• $\mathrm {match} \,f\,g\,(\mathrm {right} \,y)$ возвращает $g\,y$.

Тип суммы используется для понятий логической дизъюнкции и объединения .

произведения

Два общих типа зависимостей , зависимый продукт и зависимый тип суммы, позволяют теории кодировать интуиционистскую логику БХК , действуя как эквиваленты универсальной и экзистенциальной количественной оценки ; это формализовано перепиской Карри-Говарда . Поскольку они также связаны с произведениями и суммами в теории множеств , их часто пишут символами $\Pi$ и $\Sigma$, соответственно. Зависимые типы произведения и суммы обычно встречаются в типах функций и часто включаются в языки программирования.

Например, рассмотрим функцию $\mathrm {append}$, который принимает ${\mathsf {list}}\,a$ и термин типа $a$и возвращает список с элементом в конце. Аннотация типа такой функции будет такой: $\mathrm {append} :(\Pi \,a.{\mathsf {list}}\,a\to a\to {\mathsf {list}}\,a)$, что можно прочитать как «для любого типа $a$, пройти в ${\mathsf {list}}\,a$ и $a$и верните ${\mathsf {list}}\,a$".

Типы сумм рассматриваются в виде зависимых пар , где второй тип зависит от значения первого члена. Это естественным образом возникает в информатике, где функции могут возвращать различные типы выходных данных на основе входных данных. Например, логический тип обычно определяется с помощью функции-элиминатора. $\mathrm {if}$, который принимает три аргумента и ведет себя следующим образом.

• $\mathrm {if} \,\mathrm {true} \,x\,y$ возвращает $x$, и
• $\mathrm {if} \,\mathrm {false} \,x\,y$ возвращает $y$.

Тип возвращаемого значения этой функции зависит от ее ${\mathsf {bool}}$ вход. Если теория типов допускает зависимые типы, то можно определить функцию $\mathrm {TF} \colon {\mathsf {bool}}\to U\to U\to U$ такой, что

• $\mathrm {TF} \,\mathrm {true} \,\sigma \,\tau$ возвращает $\sigma$, и
• $\mathrm {TF} \,\mathrm {false} \,\sigma \,\tau$ возвращает $\tau$.

Тип $\mathrm {if}$ тогда можно записать как $(\Pi \,\sigma \,\tau .{\mathsf {bool}}\to \sigma \to \tau \to (\Sigma \,x:{\textsf {bool}}.\mathrm {TF} \,x\,\sigma \,\tau ))$.

Тип удостоверения

Следуя понятию соответствия Карри-Ховарда, тип идентичности — это тип, введенный для отражения пропозициональной эквивалентности , в отличие от оценочной (синтаксической) эквивалентности , которую уже обеспечивает теория типов.

Тип идентичности требует двух терминов одного типа и обозначается символом $=$. Например, если $x+1$ и $1+x$ являются терминами, то $x+1=1+x$ это возможный тип. Канонические термины создаются с помощью функции рефлексивности, $\mathrm {refl}$. На срок $t$, звонок $\mathrm {refl} \,t$ возвращает канонический термин, обитающий в типе $t=t$.

Сложность равенства в теории типов делает ее активной темой исследований; гомотопическая теория типов — примечательная область исследований, которая в основном занимается вопросами равенства в теории типов.

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

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

Некоторые помощники по доказательству , такие как Coq и Lean , основаны на исчислении индуктивных конструкций, которое представляет собой исчисление конструкций индуктивного типа.

Отличия от теории множеств

Наиболее общепринятой основой математики является логика первого порядка с языком и аксиомами теории множеств Цермело-Френкеля с аксиомой выбора , сокращенно ZFC. Теории типов, обладающие достаточной выразимостью, могут также выступать в качестве основы математики. Между этими двумя подходами существует ряд различий.

• В теории множеств есть и правила , и аксиомы , тогда как в теориях типов есть только правила. Теории типов, как правило, не имеют аксиом и определяются своими правилами вывода.
• В классической теории множеств и логике действует закон исключенного третьего . Когда теория типов кодирует понятия «и» и «или» как типы, это приводит к интуиционистской логике и не обязательно имеет закон исключенного третьего.
• В теории множеств элемент не ограничивается одним множеством. Элемент может появляться в подмножествах и объединениях с другими множествами. В теории типов термины (вообще) принадлежат только одному типу. Там, где будет использоваться подмножество, теория типов может использовать функцию предиката или использовать тип продукта с зависимой типизацией, где каждый элемент $x$ сочетается с доказательством того, что свойство подмножества справедливо для $x$. Там, где используется объединение, теория типов использует тип суммы, который содержит новые канонические термины.
• Теория типов имеет встроенное понятие вычислений. Таким образом, «1+1» и «2» — это разные термины в теории типов, но они вычисляют одно и то же значение. Более того, функции определяются вычислительно как лямбда-термы. В теории множеств «1+1=2» означает, что «1+1» — это просто еще один способ обозначения значения «2». Вычисления теории типов действительно требуют сложной концепции равенства.
• Теория множеств кодирует числа как множества . Теория типов может кодировать числа как функции с использованием кодирования Чёрча или, что более естественно, как индуктивные типы , и эта конструкция очень напоминает аксиомы Пеано .
• В теории типов доказательства являются типами, тогда как в теории множеств доказательства являются частью базовой логики первого порядка.

Сторонники теории типов также укажут на ее связь с конструктивной математикой через интерпретацию БХК , ее связь с логикой через изоморфизм Карри-Ховарда и ее связь с теорией категорий .

Свойства теорий типов

Термины обычно относятся к одному типу. Однако существуют теории множеств, которые определяют «подтипирование».

Вычисление происходит путем многократного применения правил. Многие типы теорий являются строго нормализующими , а это означает, что любой порядок применения правил всегда приводит к одному и тому же результату. Однако некоторые из них этого не делают. В нормализующей теории типов правила однонаправленных вычислений называются «правилами редукции», и применение этих правил «уменьшает» этот термин. Если правило не является однонаправленным, оно называется «правилом преобразования».

Некоторые комбинации типов эквивалентны другим комбинациям типов. Когда функции считаются «возведением в степень», комбинации типов можно записать аналогично алгебраическим тождествам. Таким образом, ${\mathbb {0} }+A\cong A$, ${\mathbb {1} }\times A\cong A$, ${\mathbb {1} }+{\mathbb {1} }\cong {\mathbb {2} }$, $A^{B+C}\cong A^{B}\times A^{C}$, $A^{B\times C}\cong (A^{B})^{C}$.

Аксиомы

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

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

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

Некоторые часто встречающиеся аксиомы:

• «Аксиома К» обеспечивает «единственность доказательств идентичности». То есть каждый термин тождественного типа равен рефлексивности.
• «Аксиома универсальности» гласит, что эквивалентность типов — это равенство типов. Исследование этого свойства привело к созданию теории кубического типа , в которой это свойство сохраняется без необходимости аксиомы.
• «Закон исключенного третьего» часто добавляется, чтобы удовлетворить пользователей, которым нужна классическая логика , а не интуиционистская логика.

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

Список

Майор

• Просто типизированное лямбда-исчисление, которое представляет собой логику более высокого порядка.
• интуиционистская теория типов
• система F
• LF часто используется для определения других теорий типов.
• исчисление конструкций и его производные

Незначительный

• Автомат
• Теория типа ST
• UTT (Единая теория зависимых типов Ло)
• некоторые формы комбинаторной логики
• другие определены в лямбда-кубе (также известном как системы чистого типа )
• другие под именем набрали лямбда-исчисление

исследования

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

См. также

• Основы математики
• Логика

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

• Аартс, К.; Бэкхаус, Р.; Хугендейк, П.; Верманс, Э.; ван дер Вауде, Дж. (декабрь 1992 г.). «Реляционная теория типов данных» . Эйндховенский технологический университет.
• Эндрюс Б., Питер (2002). Введение в математическую логику и теорию типов: к истине через доказательство (2-е изд.). Клювер. ISBN  978-1-4020-0763-7 .
• Джейкобс, Барт (1999). Категориальная логика и теория типов . Исследования по логике и основам математики. Том. 141. Эльзевир. ISBN  978-0-444-50170-7 . Архивировано из оригинала 10 августа 2023 г. Проверено 19 июля 2020 г. Подробно освещает теорию типов, включая полиморфные и зависимые расширения типов. Дает категориальную семантику .
• Карделли, Лука (1996). «Типовые системы» . В Такере, Аллен Б. (ред.). Справочник по информатике и инженерии . ЦРК Пресс. стр. 2208–36. ISBN  9780849329098 . Архивировано из оригинала 10 апреля 2008 г. Проверено 26 июня 2004 г.
• Коллинз, Джордан Э. (2012). История теории типов: развитие после второго издания «Principia Mathematica» . Академическое издательство Ламберта. hdl : 11375/12315 . ISBN  978-3-8473-2963-3 . Содержит исторический обзор развития теории типов с акцентом на упадок теории как основы математики на протяжении четырех десятилетий после публикации второго издания «Principia Mathematica».
• Констебль, Роберт Л. (2012) [2002]. «Наивная вычислительная теория типов» (PDF) . В Швихтенберге, Х.; Штайнбрюгген, Р. (ред.). Доказательство и надежность системы . Наука НАТО, серия II. Том. 62. Спрингер. стр. 213–259. ISBN  9789401004138 . Архивировано (PDF) из оригинала 9 октября 2022 г. Задуман как аналог теории типов Пола Халмоша (1960). Наивной теории множеств
• Коканд, Тьерри (2018) [2006]. «Теория типов» . Стэнфордская энциклопедия философии .
• Томпсон, Саймон (1991). Теория типов и функциональное программирование . Аддисон-Уэсли. ISBN  0-201-41667-0 . Архивировано из оригинала 23 марта 2021 г. Проверено 3 апреля 2006 г.
• Хиндли, Дж. Роджер (2008) [1995]. Базовая теория простых типов . Издательство Кембриджского университета. ISBN  978-0-521-05422-5 . Хорошее введение в простую теорию типов для специалистов по информатике; Однако описанная система не совсем STT Черча. Рецензия на книгу. Архивировано 7 июня 2011 г. в Wayback Machine.
• Камареддин, Файруз Д.; Лаан, Тван; Недерпельт, Роб П. (2004). Современный взгляд на теорию типов: от ее истоков до сегодняшнего дня . Спрингер. ISBN  1-4020-2334-0 .
• Феррейрос, Хосе; Домингес, Хосе Феррейрос (2007). «X. Логика и теория типов в межвоенный период». Лабиринт мысли: история теории множеств и ее роль в современной математике (2-е изд.). Спрингер. ISBN  978-3-7643-8349-7 .
• Лаан, ТДЛ (1997). Эволюция теории типов в логике и математике (PDF) (доктор философии). Эйндховенский технологический университет. дои : 10.6100/IR498552 . ISBN  90-386-0531-5 . Архивировано (PDF) из оригинала 9 октября 2022 г.
• Монтегю, Р. (1973) «Правильное обращение с количественной оценкой в ​​обычном английском языке». В KJJ Hintikka, JME Moravcsik и P. Suppes (ред.), «Подходы к естественному языку» (Synthese Library, 49), Dordrecht: Reidel, 221–242; перепечатано в Portner and Partee (ред.), 2002 г., стр. 17–35. См.: Семантика Монтегю , Стэнфордская энциклопедия философии.

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

Вводный материал

• Теория типов на сайте nLab , где есть статьи на многие темы.
• Статья об интуиционистской теории типов в Стэнфордской энциклопедии философии
• «Лямбда-исчисление с типами» Книга Хенка Барендрегта
• Строительное исчисление / Бумага в стиле учебника по типизированному лямбда-исчислению от Хельмута Брандла
• по интуиционистской теории типов Заметки Пера Мартина-Лёфа
• Мартина-Лёфа «Теория типов» Программирование в книге
• Книга «Теория гомотопических типов» , в которой теория гомотопических типов предлагается в качестве математической основы.

Расширенный материал

• Роберт Л. Констебль (ред.). «Теория вычислительных типов» . Схоларпедия .
• Форум TYPES — модерируемый форум электронной почты, посвященный теории типов в информатике, работающий с 1987 года.
• Книга Nuprl : « Введение в теорию типов » .
• Типы Проектные конспекты лекций летних школ 2005–2008 гг.
  • проводятся В летней школе 2005 года вводные лекции.
• Летняя школа языков программирования штата Орегон , множество лекций и несколько заметок.
  • Лекции лета 2013 г., включая выступления Роберта Харпера на YouTube.
  • Лето 2015 г. Типы, логика, семантика и проверка
• Блог Андрея Бауэра