Противоречит ли Y комбинатор соответствию Карри-Ховарду?

Y комбинатор имеет тип . Согласно соответствию Карри-Говарда, поскольку тип является обитаемым, он должен соответствовать истинной теореме. Однако всегда истинно, поэтому кажется, что тип Y-комбинатора соответствует теореме , что не всегда верно. Как это может быть?$(a \rightarrow a) \rightarrow a$$(a \rightarrow a) \rightarrow a$$a \rightarrow a$$a$

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

Конечно, существуют и другие изоморфизмы, подобные Карри-Говарду; Фил Уодлер, как известно, указал, что двуствольное имя «Карри-Ховард» предсказывает другие двуствольные имена, такие как «Хиндли-Милнер» и «Жирар-Рейнольдс». Было бы смешно, если бы "Martin-Löf" был одним из них, но это не так. Но я отвлекся.

Комбинатор Y не противоречит этому по одной ключевой причине: он не выражается в простом типе лямбда-исчисления.

На самом деле, это был весь смысл. Хаскелл Карри обнаружил комбинатор с фиксированной точкой в ​​нетипизированном лямбда-исчислении и использовал его, чтобы доказать, что нетипизированное лямбда-исчисление не является системой вывода звука.

Интересно, что тип Y соответствует логическому парадоксу, который не так хорошо известен, как следовало бы называть парадоксом Карри. Рассмотрим это предложение:

Если это предложение верно, то Санта-Клаус существует.

Предположим, что предложение было правдой. Тогда, очевидно, Санта-Клаус будет существовать. Но это именно то , что говорит предложение, так что предложение является истинным. Поэтому Дед Мороз существует. QED

Карри-Говард связывает системы типов с системами логического вывода. Среди прочего, это карты:

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

$a \to b$$a$$b$$Y (\lambda x. x) \to Y (\lambda x.M)$

Переписка Карри-Ховарда - это всего лишь переписка. Само по себе это не говорит о том, что некоторые теоремы верны. Это говорит о том, что типизируемость / доказуемость переносится с одной стороны на другую.

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

Карри-Ховард по-прежнему применяется к бесконечным типизированным исчислениям и непоследовательным системам дедукции. Это просто не особенно полезно там.