История теории типов

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

Он был связан с формальной математикой со времен Principia Mathematica и до сегодняшних помощников по доказательству .

1900–1927

Происхождение теории типов Рассела

В письме Готлобу Фреге (1902) Бертран Рассел объявил о своем открытии парадокса в «Begriffsschrift» Фреге . Фреге быстро отреагировал, признав наличие проблемы и предложив решение в ходе технического обсуждения « уровней ». Цитирую Фреге:

Кстати, мне кажется, что выражение « предикат высказывается сам о себе» не точно. Предикат, как правило, является функцией первого уровня, и эта функция требует в качестве аргумента объект и не может иметь себя в качестве аргумента (субъекта). Поэтому я бы предпочел сказать: «Понятие основано на своем собственном расширении».

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

Уиллард Куайн представляет исторический обзор происхождения теории типов и «разветвленной» теории типов: после рассмотрения вопроса об отказе от теории типов (1905 г.) Рассел предложил по очереди три теории:

1. теория зигзага
2. теория ограничения размера,
3. бесклассовая теория (1905–1906), а затем
4. повторное принятие теории типов (1908ff)

Куайн отмечает, что введение Расселом понятия «кажущейся переменной» привело к следующему результату:

различие между «все» и «любой»: «все» выражается связанной («кажущейся») переменной количественной оценки универсальности, которая варьируется по типу, а «любой» выражается свободной («реальной») переменной который схематически относится к любой неопределенной вещи, независимо от ее типа.

Куайн отвергает это понятие «связанной переменной» как « бессмысленное, если не считать определенного аспекта теории типов ».

теория типов 1908 года

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

Первичные объекты или индивиды (т. е. данные вещи, не подлежащие логическому анализу) относят к одному типу (скажем, типу 0 ), свойства индивидов — к типу 1 , свойства свойств индивидов — к типу 2 и т. д.; и не допускаются никакие свойства, которые не попадают ни в один из этих логических типов (например, это выводит свойства «предсказуемые» и «непредсказуемые»… за рамки логики). Более подробное описание будет описывать допустимые типы для других объектов, таких как отношения и классы. Затем, чтобы исключить непредписывающие определения внутри типа, типы выше типа 0 дополнительно разделяются на порядки. Таким образом, для типа 1 свойства, определенные без упоминания какой-либо совокупности, принадлежат порядку 0 , а свойства, определенные с использованием совокупности свойств данного порядка, принадлежат следующему более высокому порядку. ... Но такое разделение на порядки делает невозможным построение привычного анализа, который, как мы видели выше, содержит непредикативные определения. Чтобы избежать такого исхода, Рассел постулировал свою аксиома сводимости , которая утверждает, что для любого свойства, принадлежащего к порядку выше наименьшего, существует соэкстенсивное свойство (т. е. свойство, которым обладают точно такие же объекты) порядка 0. Если считается, что существуют только определяемые свойства, то аксиома означает что каждому импредикативному определению внутри данного типа существует эквивалентное предикативное определение (Kleene 1952:44–45).

Аксиома сводимости и понятие «матрицы»

Но поскольку условия разветвленной теории окажутся (цитируя Куайна) «обременительными», Рассел в своей книге 1908 года «Математическая логика, основанная на теории типов» также предложил бы свою аксиому сводимости . К 1910 году Уайтхед и Рассел в своих Principia Mathematica еще больше дополнили эту аксиому понятием матрицы — полностью экстенсиональной спецификации функции. Из ее матрицы функция может быть получена путем «обобщения» и наоборот, т. е. два процесса обратимы — (i) обобщение матрицы в функцию (с использованием видимых переменных) и (ii) обратный процесс уменьшение типа путем замены аргументов очевидной переменной по курсам значений. С помощью этого метода можно было избежать непредикативности.

Таблицы истинности

В 1921 году Эмиль Пост разработал теорию «функций истинности» и их таблиц истинности, которые заменили понятие кажущихся и реальных переменных. Из его «Введения» (1921): «В то время как полная теория [Уайтхеда и Рассела (1910, 1912, 1913)] требует для формулирования своих предложений реальных и кажущихся переменных, которые представляют как индивидов, так и пропозициональные функции разных видов, и в результате этого возникает необходимость в громоздкой теории типов, эта подтеория использует только реальные переменные, и эти реальные переменные представляют собой лишь один вид сущностей, которые авторы решили назвать элементарными предложениями».

Примерно в то же время Людвиг Витгенштейн развил аналогичные идеи в своей работе 1922 года «Логико-философский трактат» :

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

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

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

Витгенштейн также предложил метод таблицы истинности. В своих 4.3–5.101 Витгенштейн принимает неограниченную черту Шеффера в качестве своей фундаментальной логической сущности, а затем перечисляет все 16 функций двух переменных ( 5.101 ).

Понятие «матрица как таблица истинности» появляется еще в 1940–1950-х годах в работах Тарского, например, в его указателях 1946 года «Матрица, см.: Таблица истинности».

Сомнения Рассела

Рассел в своем «Введении в математическую философию» 1920 года посвящает целую главу «Аксиоме бесконечности и логическим типам», в которой излагает свои опасения: «Теперь теория типов решительно не принадлежит к завершенной и определенной части нашего предмета: большая часть эта теория все еще находится в зачаточном состоянии, запутана и неясна. Но необходимость некоторого учения о типах менее сомнительна, чем точная форма, которую должно принять это учение, и в связи с аксиомой бесконечности особенно легко увидеть необходимость некоторого такого учения; доктрина».

Рассел отказывается от аксиомы сводимости : во втором издании Principia Mathematica (1927) он признает аргумент Витгенштейна. В начале своего Введения он заявляет, что «не может быть сомнения... что нет необходимости проводить различие между действительными и кажущимися переменными...». Теперь он полностью поддерживает понятие матрицы и заявляет: « Функция может появляться в матрице только через ее значения » (но возражает в сноске: «Она заменяет (не совсем адекватно) аксиому сводимости» ). Кроме того, он вводит новое (сокращенное, обобщенное) понятие «матрицы», то есть «логической матрицы... такой, которая не содержит констант. Таким образом, p | q является логической матрицей». Таким образом, Рассел фактически отказался от аксиомы сводимости. но в своих последних абзацах он заявляет, что из «наших нынешних примитивных предложений» он не может вывести «дедекиндовы отношения и вполне упорядоченные отношения», и отмечает, что если существует новая аксиома, заменяющая аксиому сводимости, «ее еще предстоит открыть».

Теория простых типов

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

Полученная в результате ограниченная логика называется теорией простых типов. или, что более распространено, простая теория типов. Подробные формулировки простой теории типов были опубликованы в конце 1920-х - начале 1930-х годов.Р. Карнап, Ф. Рэмси, У.В.О. Куайн и А. Тарский. В 1940 году Алонсо Чёрч (пере) сформулировал его как просто типизированное лямбда-исчисление . и исследовано Гёделем в 1944 году. Обзор этих событий можно найти у Коллинза (2012).

1940-е – настоящее время

Гёдель 1944 г.

Курт Гёдель в своей « Математической логике Рассела» 1944 года дал в сноске следующее определение «теории простых типов»:

Под теорией простых типов я подразумеваю учение, согласно которому объекты мышления (или, в другой интерпретации, символические выражения) делятся на типы, а именно: индивиды, свойства индивидов, отношения между индивидами, свойства таких отношений, и т. д. (с аналогичной иерархией расширений), и что предложения вида: « а обладает свойством ф », « b находится в отношении R к с » и т. д. бессмысленны, если a, b, c, R, φ не относятся к типам, подходящим друг к другу. Смешанные типы (например, классы, содержащие индивидуумы и классы в качестве элементов), а также, следовательно, трансфинитные типы (например, класс всех классов конечных типов) исключаются. То, что теории простых типов достаточно для того, чтобы избежать эпистемологических парадоксов, показывает более тщательный их анализ. (Ср. Рэмси 1926 и Тарский 1935 , стр. 399).».

Он пришел к выводу, что (1) теория простых типов и (2) аксиоматическая теория множеств «позволяют вывести современную математику и в то же время избежать всех известных парадоксов» (Gödel 1944:126); более того, теория простых типов «является системой первых Principia [ Principia Mathematica ] в соответствующей интерпретации... Однако [м]аждые симптомы слишком ясно показывают, что примитивные понятия нуждаются в дальнейшем разъяснении» (Gödel 1944). :126).

Карри-Ховарда, 1934–1969

Соответствие Карри-Ховарда представляет собой интерпретацию доказательств как программ и формул как типов. Идея началась в 1934 году с Хаскелла Карри и завершилась в 1969 году Уильямом Элвином Ховардом . Он связал «вычислительный компонент» многих теорий типов с логическими выводами.

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

АВТОМАТ де Брейна,

Николаас Говерт де Брейн создал теорию типов Automath как математическую основу для системы Automath, которая могла проверять правильность доказательств. Система развивалась и добавляла функции с течением времени по мере развития теории типов.

теория типов Мартина-Лёфа, 1971–1984

Пер Мартин-Лёф нашел теорию типов, которая соответствовала логике предикатов , путем введения зависимых типов , которая стала известна как интуиционистская теория типов или теория типов Мартина-Лёфа.

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

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

Строительное исчисление Коканда и Юэ

Тьерри Коканд и Жерар Юэ создали « Конструктивное исчисление» . теория зависимого типа для функций. В случае с индуктивными типами оно будет называться «Исчислением индуктивных конструкций» и станет основой для Coq и Lean .

куб Барендрегта,

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

личности не уникальны,

До 1994 года многие теоретики типов считали, что все термины одного и того же типа идентичности одинаковы. То есть, чтобы все было рефлексивно. Но Мартин Хофманн и Томас Штрайхер показали, что этого не требуют правила типа идентичности. В своей статье «Модель группоида опровергает уникальность доказательств идентичности» они показали, что условия равенства можно смоделировать как группу, где нулевым элементом была «рефлексивность», сложение — «транзитивность», а отрицание — «симметрия».

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

Источники

• Бертран Рассел (1903), Принципы математики: Том. 1 , Кембридж в Университетском издательстве, Кембридж, Великобритания.
• Бертран Рассел (1920), «Введение в математическую философию» (второе издание), Dover Publishing Inc., Нью-Йорк, штат Нью-Йорк, ISBN   0-486-27724-0 (в частности, главы XIII и XVII).
• Альфред Тарский (1946), «Введение в логику и методологию дедуктивных наук» , переиздано в 1995 году издательством Dover Publications, Inc., Нью-Йорк, штат Нью-Йорк. ISBN   0-486-28462-X
• Жан ван Хейеноорт (1967, 3-е издание 1976 г.), От Фреге до Геделя: справочник по математической логике, 1879–1931 , издательство Гарвардского университета, Кембридж, Массачусетс, ISBN   0-674-32449-8 (пбк)
  • Бертран Рассел (1902), Письмо Фреге с комментариями ван Хейеноорта, страницы 124–125. При этом Рассел объявляет об открытии «парадокса» в творчестве Фреге.
  • Готтлоб Фреге (1902), Письмо Расселу с комментариями ван Хейеноорта, страницы 126–128.
  • Бертран Рассел (1908), Математическая логика, основанная на теории типов , с комментариями Уилларда Куайна , страницы 150–182.
  • Эмиль Пост (1921), «Введение в общую теорию элементарных предложений » с комментарием ван Хейеноорта, страницы 264–283.
• Альфред Норт Уайтхед и Бертран Рассел (1910–1913, 1927 г., 2-е издание переиздано в 1962 г.), Principia Mathematica до * 56 , Кембридж в University Press, Лондон, Великобритания, нет ISBN или номера карточного каталога в США.
• Людвиг Витгенштейн (переиздано в 2009 г.), Основные работы: Избранные философские сочинения , HarperCollins, Нью-Йорк. ISBN   978-0-06-155024-9 . Витгенштейна (1921 г. на английском языке), Tractatus Logico-Philosophicus , страницы 1–82.

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

• У. Фармер, «Семь достоинств простой теории типов», Journal of Applied Logic , Vol. 6, № 3. (сентябрь 2008 г.), стр. 267–286.