Теория типов

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

Некоторые теории типов служат альтернативой теории множеств как основе математики . Два известных таких теорий Алонзо Чёрч «s типизированного λ-исчисление и Мартин-Лёф » s интуиционистской теории типа .

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

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

История

Между 1902 и 1908 годами Бертран Рассел предложил различные «теории типов» в ответ на его открытие, что версия наивной теории множеств Готтлоба Фреге поражена парадоксом Рассела . К 1908 году Рассел пришел к «разветвленной» теории типов вместе с « аксиомой сводимости », обе из которых занимали видное место в « Principia Mathematica» Уайтхеда и Рассела.опубликовано между 1910 и 1913 годами. Они попытались разрешить парадокс Рассела, сначала создав иерархию типов, а затем назначив каждый конкретный математический (и, возможно, другой) объект типу. Сущности данного типа создаются исключительно из сущностей тех типов, которые находятся ниже в своей иерархии, что предотвращает присвоение сущности самой себе.

В 1920-х годах Леон Чвистек и Фрэнк П. Рэмси предложили неразветвленную теорию типов, теперь известную как «теория простых типов» или теория простых типов , которая разрушила иерархию типов в более ранней разветвленной теории и как таковая не требовала аксиома сводимости.

Обычно «теория типов» используется, когда эти типы используются в системе перезаписи терминов . Самый известный ранний пример - это просто типизированное лямбда-исчисление Алонзо Чёрча . Теория типов Чёрча ^[1] помогла формальной системе избежать парадокса Клини – Россера , поразившего исходное нетипизированное лямбда-исчисление. Черч продемонстрировал, что он может служить основой математики, и был назван логикой более высокого порядка .

Некоторые другие теории типа включают Per Martin-LOF «s интуиционистской теории типа , которая была основой используется в некоторых областях конструктивной математики . Тьерри Кокана «сек Исчисление конструкций и ее производные являются основой используется Coq , Постный , и другими. Эта область является областью активных исследований, что демонстрирует теория гомотопического типа .

Основные понятия

Современное представление систем типов в контексте теории типов стало систематизированным с помощью концептуальной основы, введенной Хенком Барендрегтом . ^[2]

Тип, срок, значение

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

Среда ввода, назначение типа, оценка типа

Набор текста обычно происходит в некотором контексте или среде, обозначенной символом${\ displaystyle \ Gamma}$. Часто окружение представляет собой список пар${\ Displaystyle е: \ тау}$. Эту пару иногда называют заданием . Контекст завершает вышеуказанное противопоставление. Вместе они образуют суждение, обозначенное${\ displaystyle \ Gamma \ vdash e: \ tau}$.

Правила перезаписи, конвертация, редукция

Теории типов имеют явное вычисление и закодированы в правилах переписывания терминов. Они называются правилами преобразования или, если правило работает только в одном направлении, правилом редукции . Например,${\ displaystyle 2 + 2}$ и ${\ displaystyle 4}$синтаксически разные термины, но первое сводится ко второму. Это сокращение написано${\ displaystyle 2 + 2 \ twoheadrightarrow 4}$. Эти правила также устанавливают соответствующие эквивалентности между терминами, написанными${\ Displaystyle 2 + 2 \ Equiv 4}$.

Срок ${\ displaystyle 2 + 1}$ сводится к ${\ displaystyle 3}$. С${\ displaystyle 3}$не подлежит дальнейшему сокращению, это называется нормальной формой . Различные системы типизированного лямбда-исчисления, включая просто типизированное лямбда-исчисление , систему F Жан-Ива Жирара и исчисление конструкций Тьерри Коквана, являются строго нормализующими . В таких системах успешная проверка типа подразумевает прекращение срока действия.

Правила типа

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

Проблемы с решением

Система типа естественным образом связана с проблемами решения о проверке типа , typability и тип обитания . ^[3]

Проверка типа

Проблема решения проверки типов (сокращенно${\ displaystyle \ Gamma \ vdash e: \ tau?}$) является:

Учитывая типовое окружение ${\ displaystyle \ Gamma}$, термин ${\ displaystyle e}$, а тип ${\ Displaystyle \ тау}$, решите, является ли срок ${\ displaystyle e}$ можно присвоить тип ${\ Displaystyle \ тау}$ в типовой среде ${\ displaystyle \ Gamma}$.

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

Типичность

Решение проблемы типизации (сокращенно:${\ Displaystyle \ существует \ Gamma, \ tau. \ Gamma \ vdash e: \ tau?}$) является:

Учитывая срок ${\ displaystyle e}$, решите, существует ли среда типа ${\ displaystyle \ Gamma}$ и тип ${\ Displaystyle \ тау}$ так что срок ${\ displaystyle e}$ можно присвоить тип ${\ Displaystyle \ тау}$ в типовой среде ${\ displaystyle \ Gamma}$.

Вариант типизируемости - типизируемость. среда типа (сокращенно${\ Displaystyle \ существует \ tau. \ Gamma \ vdash e: \ tau?}$), для которого окружение типов является частью входных данных. Если данный термин не содержит внешних ссылок (таких как переменные свободного термина), то типируемость совпадает с типируемостью по отношению к. среда пустого типа.

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

Тип обитания

Проблема решения типа заселения (сокращенно${\ Displaystyle \ существует е. \ Гамма \ vdash е: \ тау?}$) является:

Учитывая типовое окружение ${\ displaystyle \ Gamma}$ и тип ${\ Displaystyle \ тау}$, решите, существует ли термин ${\ displaystyle e}$ которому можно присвоить тип ${\ Displaystyle \ тау}$ в типовой среде ${\ displaystyle \ Gamma}$.

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

Противопоставление терминов и типов также может рассматриваться как одно из воплощений и спецификаций . Посредством программного синтеза (вычислительного аналога) размещение типов (см. Ниже) может использоваться для построения (всех или частей) программ из спецификации, представленной в форме информации о типе. ^[4]

Интерпретации теории типов

Теория типов тесно связана со многими областями активных исследований. В частности, соответствие Карри – Ховарда обеспечивает глубокий изоморфизм между интуиционистской логикой, типизированным лямбда-исчислением и декартово закрытыми категориями.

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

Помимо представления о типах как о совокупности значений термина, теория типов предлагает вторую интерпретацию противопоставления термина и типов. Типы можно рассматривать как предложения, а термины как доказательства . В этом способе чтения набора тип функции${\ displaystyle \ alpha \ rightarrow \ beta}$рассматривается как импликация , т. е. как утверждение, что${\ displaystyle \ beta}$ следует из ${\ displaystyle \ alpha}$.

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

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

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

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

• Теория множеств построена на логике. Для этого требуется отдельная система, такая как логика предикатов . В теории типов такие понятия, как «и» и «или», могут быть закодированы как типы в самой теории типов.
• В теории множеств элемент не ограничен одним множеством. В теории типов термины (как правило) принадлежат только к одному типу. (Там, где будет использоваться подмножество, теория типов имеет тенденцию использовать функцию предиката, которая возвращает истину, если термин входит в подмножество, и возвращает ложь, если значение нет. Объединение двух типов может быть определено как новый тип, называемый суммой типа , который содержит новые термины.)
• Теория множеств обычно кодирует числа как множества. (0 - это пустое множество, 1 - это набор, содержащий пустое множество, и т. Д. См. Теоретико-множественное определение натуральных чисел .) Теория типов может кодировать числа как функции с использованием кодировки Чёрча или, что более естественно, как индуктивные типы . Индуктивные типы создают новые константы для функции-преемника и нуля, очень напоминающие аксиомы Пеано .
• Теория типов имеет простую связь с конструктивной математикой через интерпретацию BHK . Это может быть связано с логикой изоморфизмом Карри – Ховарда . А некоторые теории типов тесно связаны с теорией категорий .

Дополнительные функции

Зависимые типы

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

Например, список ${\ Displaystyle \ mathrm {нат}}$s длины 4 может быть другого типа, чем список ${\ Displaystyle \ mathrm {нат}}$s длины 5. В теории типов с зависимыми типами можно определить функцию, которая принимает параметр «n» и возвращает список, содержащий «n» нулей. Вызов функции с 4 приведет к созданию члена с другим типом, чем если бы функция вызывалась с 5.

Другой пример - это тип, состоящий из доказательств того, что термин аргумента имеет определенное свойство, такое как член ${\ Displaystyle \ mathrm {нат}}$ тип, например заданное натуральное число, является простым. См. Переписку Карри-Ховарда .

Зависимые типы играют центральную роль в интуиционистской теории типов и в разработке таких языков функционального программирования, как Idris , ATS , Agda и Epigram .

Типы равенства

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

В интуиционистской теории типов тип равенства (также называемый типом идентичности) известен как ${\ displaystyle I}$для идентичности. Есть тип${\ Displaystyle I \ A \ a \ b}$ когда ${\ displaystyle A}$ это тип и ${\ displaystyle a}$ и ${\ displaystyle b}$ оба термина типа ${\ displaystyle A}$. Срок типа${\ Displaystyle I \ A \ a \ b}$ интерпретируется как означающее, что ${\ displaystyle a}$ равно ${\ displaystyle b}$.

На практике можно построить тип ${\ Displaystyle I \ \ mathrm {нат} \ 3 \ 4}$но такого термина не будет. В интуиционистской теории типов новые термины равенства начинаются с рефлексивности. Если${\ displaystyle 3}$ это термин типа ${\ Displaystyle \ mathrm {нат}}$, то существует терм типа ${\ Displaystyle I \ \ mathrm {нат} \ 3 \ 3}$. Более сложные равенства могут быть созданы путем создания рефлексивного члена и последующего сокращения с одной стороны. Так что если${\ displaystyle 2 + 1}$ это термин типа ${\ Displaystyle \ mathrm {нат}}$, то есть член типа ${\ Displaystyle I \ \ mathrm {нат} \ (2 + 1) \ (2 + 1)}$ и, уменьшив, сгенерируйте член типа ${\ Displaystyle I \ \ mathrm {нат} \ (2 + 1) \ 3}$. Таким образом, в этой системе тип равенства означает, что два значения одного и того же типа могут быть преобразованы редукциями.

Наличие типа для равенства важно, потому что им можно манипулировать внутри системы. Обычно нельзя судить, что два члена не равны; вместо этого, как в интерпретации Брауэра – Гейтинга – Колмогорова , мы отображаем${\ Displaystyle \ neg (а = Ь)}$ к ${\ Displaystyle (а = Ь) \ к \ бот}$, куда ${\ displaystyle \ bot}$это нижний тип , не имеющий значений. Существует термин с типом${\ displaystyle (I \ \ mathrm {nat} \ 3 \ 4) \ to \ bot}$, но не одного типа${\ displaystyle (I \ \ mathrm {nat} \ 3 \ 3) \ to \ bot}$.

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

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

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

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

Индукция-индукция - это функция для объявления индуктивного типа и семейства типов, которое зависит от индуктивного типа.

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

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

Типы были созданы для предотвращения парадоксов, таких как парадокс Рассела . Однако мотивы, которые приводят к этим парадоксам - способность говорить обо всех типах людей - все еще существуют. Итак, у многих теорий типов есть «тип вселенной», который содержит все другие типы (но не сам).

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

Универсальные типы типов особенно сложны в теории типов. Первоначальное предложение интуиционистской теории типов страдало от парадокса Жирара .

Вычислительный компонент

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

Система теории типов, которая имеет хорошо управляемый вычислительный компонент, также имеет простую связь с конструктивной математикой через интерпретацию BHK .

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

Типовые теории

Майор

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

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

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

Активный

• Теория гомотопического типа находится в стадии исследования.

Практическое воздействие

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

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

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

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

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

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

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

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

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

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

Лингвистика

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

Самая обычная конструкция принимает основные типы ${\ displaystyle e}$ и ${\ displaystyle t}$для индивидов и истинностных значений , соответственно, и рекурсивно определяет набор типов следующим образом:

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

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

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

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

Отношение к теории категорий

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

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

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

См. Также

• Тип данных для конкретных типов данных в программировании
• Теория предметной области
• Тип (теория модели)
• Система типов для более практического обсуждения систем типов для языков программирования
• Универсальные основы

Примечания

Ссылки

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

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

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