Ветвление непредсказуемой теории типов

Большинство теорий типов, которые мне известны, являются предикативными, под которыми я подразумеваю, что

Void : Prop
Void = (x : Prop) -> x

не является типизированным в большинстве доказательств теорем, поскольку этот тип пи принадлежит той же вселенной, что Propи не тот случай Prop : Prop. Это делает их предикативными и не позволяет использовать предикативные определения, подобные приведенным выше. Тем не менее, очень много «языков классной доски», таких как System F или CoC, фактически являются непредсказуемыми. Фактически, эта непредсказуемость жизненно важна для определения большинства конструкций, не включенных примитивно в язык.

Мой вопрос: почему человек хочет отказаться от непредсказуемости, учитывая его силу в определении логических конструкций? Я слышал, как пара людей заметили, что непредсказуемость приводит к ошибкам в «вычислениях» или «индукции», но мне трудно найти конкретное объяснение.

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

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

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

Приблизительно в 1971 году Мартин-Лёф представил зависимую теорию типов, в которой Type : Typeсправедлив и этот принцип, и дальнейшая аксиома . Эта система оказалась непоследовательной по тонким причинам: наивный парадокс Рассела не может быть воспроизведен (прямым способом), но, тем не менее, умная кодировка позволяет найти противоречие. Это вызвало кризис веры, подобный кризису Рассела, в результате чего появилась теория предикативного типа с вселенными, которые мы знаем и любим.

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

Несколько моментов:

1. Какое это имеет отношение к интуиционистской математике? Ответ не очень. На рубеже XX века математики, как правило, связывали использование циркулярных / импредикативных принципов с неконструктивным рассуждением (интуиция заключается в том, что импредикативное рассуждение предполагает уже существующую математическую вселенную, как и использование исключенного среднего). Тем не менее, есть совершенно интуиционистская непредикативных теория (как IZF ). Люди, интересующиеся интуиционизмом, по-прежнему склонны интересоваться предикативизмом по какой-то причине (конечно, я виноват в этом).

2. Что вы можете сделать в предикативной математике? Как указывает Мартин в своем ответе, Герман Вейль (не путать с Андре Вейлем) начал программу, которая пыталась исследовать выразительную силу предикативных систем, взяв за отправную точку то, что предикативные системы имели выразительную силу между арифметикой Пеано и Вторым Порядком. Арифметика , которая в значительной степени согласуется с тем, что по большинству стандартов она является непредсказуемой (и сравнима с Системой F на стороне теории типов). Позднее эту программу назвали «обратной математикой», поскольку она пыталась классифицировать силу известных математических теорем в терминах аксиом, необходимых для их доказательства (обратный подход к обычному подходу). страница википедии дает хороший обзор; Программа была довольно успешной, так как большую часть математики XIX века можно легко разместить в очень слабых системах. До сих пор остается открытым вопрос, может ли эта программа масштабироваться до более поздних результатов, скажем, в теории более высоких категорий (подозрение заключается в том, что ответ «да, с большими усилиями»).

Одним из измерений является вывод типа. Например, вывод типа System F не является разрешимым, но некоторые его предикативные фрагменты имеют разрешимый (частичный) вывод типа.

Другое измерение - последовательность как логика. Уважаемые мыслители исторически испытывали тошноту из-за того, что у них есть непредсказуемые основы математики. В конце концов, это форма круговых рассуждений. Я думаю, что Х. Вейль, возможно, был первым или одним из первых, кто попытался реконструировать как можно больше математики предиктивным способом ... просто чтобы быть в безопасности. Мы узнали, что цикличность импредикативности не является проблематичной в классической математике в том смысле, что из «ручных» импредикативных определений никогда не возникало никаких противоречий. Со временем мы научились доверять им. Обратите внимание, что это (отсутствие парадокса) является эмпирическимнаблюдение! Тем не менее, большая часть развития теории доказательств с ее странными порядковыми конструкциями преследует конечную цель - построить всю математику «снизу», то есть без нечетких определений. Эта программа не завершена. В последние годы интерес к предикативным основам математики сместился от забот о парадоксе к вычислительному содержанию доказательств, которые интересны по разным причинам. Оказывается, что непредсказуемые определения затрудняют извлечение вычислительного контента. Еще один аспект беспокойства о последовательности исходит от традиции Карри-Говарда. Первоначальная теория типов Мартина-Лёфа была непредсказуемой ... и необоснованной. После этого шока он предложил только предикативные системы, но в сочетании с индуктивными типами данных, чтобы восстановить большую часть силы непредсказуемости.

Теории типов склонны к предиктивности в основном по социально-техническим причинам.

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

Однако обратите внимание, что в стандартной (например, ZFC) теории множеств эти операции не могут быть определены как объекты . В теории множеств не существует такого понятия, как «функция тождества», потому что функция - это отношение между набором доменов и набором доменов, и если единственная функция может быть функцией тождества, то вы можете использовать ее для построения набора. из всех комплектов. (Именно так Джон Рейнольдс показал, что полиморфизм в стиле System-F не ​​имеет теоретико-множественных моделей.)

$X$$S$$P$$X$$P$$X$

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