Войти
В математике, логике и информатике система типов - это формальная система, в которой каждый термин имеет «тип», который определяет его значение и операции, которые могут выполняться с ним. Теория типов - это академическое исследование систем типов.
Некоторые теории типов служат альтернативой теории множеств как основе математики. Два известных таких теорий Алонзо Чёрч «s типизированного λ-исчисление и Мартин-Лёф » s интуиционистской теории типа.
Теория типов была создана, чтобы избежать парадоксов в предыдущих основах, таких как наивная теория множеств, формальная логика и системы перезаписи.
Теория типов тесно связана с вычислительными системами типов, а в некоторых случаях частично совпадает с ними, которые представляют собой функцию языка программирования, используемую для уменьшения количества ошибок и облегчения определенных оптимизаций компилятора.
Между 1902 и 1908 годами Бертран Рассел предложил различные «теории типов» в ответ на его открытие, что версия наивной теории множеств Готтлоба Фреге поражена парадоксом Рассела. К 1908 году Рассел пришел к «разветвленной» теории типов вместе с « аксиомой сводимости », обе из которых занимали видное место в « Математических принципах Уайтхеда» и Рассела, опубликованных между 1910 и 1913 годами. Они попытались разрешить парадокс Рассела, сначала создав иерархию. типов, а затем присвоение каждой конкретной математической (и, возможно, другой) сущности типу. Сущности данного типа создаются исключительно из сущностей тех типов, которые находятся ниже в своей иерархии, что предотвращает присвоение сущности самой себе.
В 1920-х годах Леон Чвистек и Франк П. Рэмси предложили неразветвленную теорию типов, теперь известную как «теория простых типов» или теория простых типов, которая разрушила иерархию типов в более ранней разветвленной теории и как таковая не требовала аксиома сводимости.
Обычно «теория типов» используется, когда эти типы используются в системе перезаписи терминов. Самый известный ранний пример - это просто типизированное лямбда-исчисление Алонзо Чёрча. Теория типов Чёрча помогла формальной системе избежать парадокса Клини – Россера, поразившего исходное нетипизированное лямбда-исчисление. Черч продемонстрировал, что он может служить основой математики, и был назван логикой более высокого порядка.
Некоторые другие теории типа включают Per Martin-LOF «s интуиционистской теории типа, которая была основой используется в некоторых областях конструктивной математики. Тьерри Кокана «сек Исчисление конструкций и ее производные являются основой используется Coq, Постный, и другими. Эта область является областью активных исследований, что демонстрирует теория гомотопического типа.
Современное представление систем типов в контексте теории типов стало систематизированным с помощью концептуальной основы, введенной Хенком Барендрегтом.
В системе теории типов термин противопоставляется типу. Например, 4, 2 + 2 и - все отдельные термины с типом nat для натуральных чисел. Традиционно за термином следует двоеточие и его тип, например 2: nat - это означает, что число 2 относится к типу nat. Помимо этого противостояния и синтаксиса, мало что можно сказать о типах в этой общности, но часто они интерпретируются как своего рода набор (не обязательно наборы) значений, которые может оценивать термин. Термы обычно обозначают через e, а типы - через τ. Форма терминов и типов зависит от конкретной системы типов и уточняется некоторым синтаксисом и дополнительными ограничениями корректности.
Набор текста обычно происходит в некотором контексте или среде, обозначенной символом. Часто среда - это список пар. Эту пару иногда называют заданием. Контекст завершает вышеуказанное противопоставление. Вместе они образуют суждение обозначаемого.
Теории типов имеют явное вычисление и закодированы в правилах переписывания терминов. Они называются правилами преобразования или, если правило работает только в одном направлении, правилом редукции. Например, и являются синтаксически разными терминами, но первое сводится ко второму. Это сокращение написано. Эти правила также устанавливают соответствующую эквивалентность между написанными терминами.
Срок сокращается до. Поскольку не подлежит дальнейшему сокращению, она называется нормальной формой. Различные системы типизированного лямбда-исчисления, включая просто типизированное лямбда-исчисление, систему F Жан-Ива Жирара и исчисление конструкций Тьерри Коквана, являются строго нормализующими. В таких системах успешная проверка типа подразумевает прекращение срока действия.
На основе суждений и эквивалентностей правила вывода типов могут использоваться для описания того, как система типов присваивает тип синтаксическим конструкциям (терминам), как и в естественном выводе. Чтобы быть значимыми, правила преобразования и типов обычно тесно связаны, например, с помощью свойства сокращения предмета, которое может установить часть надежности системы типов.
Система типа естественным образом связана с проблемами решения о проверке типа, typability и тип обитания.
Проблема решения проверки типа (сокращенно):
Разрешимость проверки типов означает, что безопасность типа любого заданного текста программы (исходного кода) может быть проверена.
Проблема решения типизируемости (сокращенно):
Вариант типизируемости - типизируемость. окружение типа (сокращенно), для которого окружение типа является частью ввода. Если данный термин не содержит внешних ссылок (таких как переменные свободных терминов), то типируемость совпадает с типируемостью по отношению к. среда пустого типа.
Типичность тесно связана с выводом типа. В то время как типизация (как проблема решения) касается существования типа для данного термина, вывод типа (как проблема вычисления) требует вычисления фактического типа.
Проблема решения типа обитания (сокращенно):
Парадокс Жирара показывает, что заселение типов сильно связано с согласованностью системы типов с соответствием Карри – Ховарда. Чтобы такая система была здоровой, она должна иметь необитаемые типы.
Противопоставление терминов и типов также может рассматриваться как одно из воплощений и спецификаций. Посредством программного синтеза (вычислительного аналога) размещение типов (см. Ниже) может использоваться для построения (всех или частей) программ из спецификации, представленной в форме информации о типе.
Теория типов тесно связана со многими областями активных исследований. В частности, соответствие Карри – Ховарда обеспечивает глубокий изоморфизм между интуиционистской логикой, типизированным лямбда-исчислением и декартово закрытыми категориями.
Помимо представления о типах как о совокупности значений термина, теория типов предлагает вторую интерпретацию противопоставления термина и типов. Типы можно рассматривать как предложения, а термины как доказательства. В этом способе чтения типизации тип функции рассматривается как импликация, то есть как предложение, которое следует из.
Внутренний язык декартова закрытой категории является просто напечатал лямбда - исчисление. Это представление можно распространить на другие типизированные лямбда-исчисления. Определенные декартовы закрытые категории, топосы, были предложены в качестве общей установки для математики вместо традиционной теории множеств.
Существует много различных теорий множеств и много разных систем теории типов, поэтому все, что следует ниже, является обобщением.
Зависит тип представляет собой тип, который зависит от срока или другого типа. Таким образом, тип, возвращаемый функцией, может зависеть от аргумента функции.
Например, список s длины 4 может быть другого типа, чем список s длины 5. В теории типов с зависимыми типами можно определить функцию, которая принимает параметр «n» и возвращает список содержащий "n" нулей. Вызов функции с 4 приведет к созданию члена с другим типом, чем если бы функция вызывалась с 5.
Другой пример - это тип, состоящий из доказательств того, что член аргумента имеет определенное свойство, такое как член типа, например, данное натуральное число является простым. См. Переписку Карри-Ховарда.
Зависимые типы играют центральную роль в интуиционистской теории типов и в разработке языков функционального программирования, таких как Idris, ATS, Agda и Epigram.
Многие системы теории типов имеют тип, который представляет равенство типов и терминов. Этот тип отличается от конвертируемости и часто обозначается пропозициональным равенством.
В интуиционистской теории типов тип равенства (также называемый типом идентичности) известен как идентичность. Существует тип, когда тип и и оба условия типа. Термин типа интерпретируется как значение, равное.
На практике можно построить тип, но не существует термина этого типа. В интуиционистской теории типов новые термины равенства начинаются с рефлексивности. Если это термин типа, то существует термин типа. Более сложные равенства могут быть созданы путем создания рефлексивного члена и последующего сокращения с одной стороны. Итак, если это термин типа, тогда существует термин типа и, путем сокращения, генерирует термин типа. Таким образом, в этой системе тип равенства означает, что два значения одного и того же типа могут быть преобразованы редукциями.
Наличие типа для равенства важно, потому что им можно манипулировать внутри системы. Обычно нельзя судить, что два члена не равны; вместо этого, как и в интерпретации Браувер-гейтингова-Колмогорова, мы карту, чтобы, где это нижний тип, не имеющие значения. Существует термин с типом, но не с типом.
Теория гомотопических типов отличается от интуиционистской теории типов главным образом тем, что она обращается с типом равенства.
Система теории типов требует использования некоторых основных терминов и типов. Некоторые системы строят их из функций, использующих кодировку Чёрча. В других системах есть индуктивные типы: набор базовых типов и набор конструкторов типов, которые генерируют типы с хорошо управляемыми свойствами. Например, некоторые рекурсивные функции, вызываемые индуктивными типами, гарантированно завершаются.
Коиндуктивные типы - это бесконечные типы данных, созданные с помощью функции, которая генерирует следующий элемент (ы). См. Coinduction и Corecursion.
Индукция-индукция - это функция для объявления индуктивного типа и семейства типов, которое зависит от индуктивного типа.
Индукционная рекурсия позволяет использовать более широкий диапазон хорошо управляемых типов, позволяя определять тип и рекурсивные функции, работающие с ним, одновременно.
Типы были созданы для предотвращения парадоксов, таких как парадокс Рассела. Однако мотивы, которые приводят к этим парадоксам - способность говорить обо всех типах людей - все еще существуют. Итак, у многих теорий типов есть «тип вселенной», который содержит все другие типы (но не сам).
В системах, где вы, возможно, захотите что-то сказать о типах юниверсов, существует иерархия типов юниверсов, каждый из которых содержит тот, который находится ниже в иерархии. Иерархия определяется как бесконечная, но утверждения должны относиться только к конечному числу уровней юниверса.
Универсальные типы типов особенно сложны в теории типов. Первоначальное предложение интуиционистской теории типов страдало от парадокса Жирара.
Многие системы теории типов, такие как просто типизированное лямбда-исчисление, интуиционистская теория типов и исчисление конструкций, также являются языками программирования. То есть говорят, что они имеют «вычислительную составляющую». Вычисление - это сокращение терминов языка с помощью правил перезаписи.
Система теории типов, которая имеет хорошо отлаженный вычислительный компонент, также имеет простую связь с конструктивной математикой через интерпретацию BHK.
Неконструктивная математика в этих системах возможна путем добавления операторов к продолжениям, таких как вызов с текущим продолжением. Однако эти операторы имеют тенденцию нарушать желаемые свойства, такие как каноничность и параметричность.
Существует обширное пересечение и взаимодействие между областями теории типов и систем типов. Системы типов - это функция языка программирования, предназначенная для выявления ошибок. Любой анализ статической программы, такие как тип проверки алгоритмов в семантическом анализе фазе компилятора, имеет связь с теорией типа.
Ярким примером является Agda, язык программирования, который использует UTT (унифицированная теория зависимых типов Луо) для своей системы типов. Язык программирования ML был разработан для управления теориями типов (см. LCF ), и на его собственную систему типов они сильно повлияли.
Первый помощник компьютерного доказательства, названный Automath, использовал теорию типов для кодирования математики на компьютере. Мартин-Лёф специально разработал интуиционистскую теорию типов, чтобы закодировать всю математику, чтобы служить новым основанием для математики. Продолжаются исследования математических основ с использованием теории гомотопического типа.
Математикам, работающим в области теории категорий, уже было трудно работать с широко признанным основанием теории множеств Цермело – Френкеля. Это привело к таким предложениям, как «Элементарная теория категорий множеств Лавера» (ETCS). Теория гомотопических типов продолжается в этом направлении, используя теорию типов. Исследователи изучают связи между зависимыми типами (особенно типом идентичности) и алгебраической топологией (в частности, гомотопией ).
Большая часть текущих исследований теории типов проводится с помощью средств проверки доказательства, интерактивных помощников по доказательству и автоматических средств доказательства теорем. Большинство этих систем используют теорию типов в качестве математической основы для кодирования доказательств, что неудивительно, учитывая тесную связь между теорией типов и языками программирования:
Многие теории типов поддерживаются LEGO и Изабель. Изабель также поддерживает основы помимо теорий типов, такие как ZFC. Мицар - пример системы доказательств, которая поддерживает только теорию множеств.
Теория Тип также широко используется в формальных теориях семантики в естественных языках, особенно Монтегю грамматики и его потомков. В частности, категориальные грамматики и предгрупповые грамматики широко используют конструкторы типов для определения типов слов ( существительное, глагол и т. Д.).
Наиболее распространенная конструкция берет базовые типы и для индивидов и истинностных значений, соответственно, и рекурсивно определяет набор типов следующим образом:
Сложный тип - это тип функций от сущностей типа до сущностей типа. Таким образом, есть типы, подобные тем, которые интерпретируются как элементы набора функций от сущностей до истинностных значений, то есть индикаторные функции наборов сущностей. Выражение типа - это функция от наборов сущностей до истинностных значений, то есть набор наборов (индикаторная функция). Этот последний тип обычно считается типом квантификаторов естественного языка, таких как все или никто ( Montague 1973, Barwise and Cooper 1981).
Грегори Бейтсон ввел теорию логических типов в социальные науки; его представления о двойном связывании и логических уровнях основаны на теории типов Рассела.
Хотя первоначальная мотивация теории категорий была далека от фундаментализма, оказалось, что эти две области имеют глубокую связь. Как пишет Джон Лейн Белл : «Фактически категории сами по себе могут рассматриваться как теории типов определенного типа; один этот факт указывает на то, что теория типов гораздо более тесно связана с теорией категорий, чем с теорией множеств». Вкратце, категорию можно рассматривать как теорию типов, рассматривая ее объекты как типы (или сорта), т.е. «грубо говоря, категорию можно рассматривать как теорию типов, лишенную синтаксиса». Таким образом, следует ряд важных результатов:
Взаимодействие, известное как категориальная логика, с тех пор стало предметом активных исследований; см., например, монографию Джейкобса (1999).
