На странице Википедии для комбинаторов с фиксированной точкой написан довольно загадочный текст
Y комбинатор является примером того, что делает лямбда-исчисление непоследовательным. Поэтому к этому следует относиться с подозрением. Однако комбинатор Y можно считать безопасным, если он определен только в математической логике.
Я вступил в какой-то шпионский роман? Что в мире подразумевается под утверждениями о том, что калькуляция является «противоречивой» и что ее следует «рассматривать с подозрением» ?
Ответы:
Оно вдохновлено реальными событиями, но то, как оно заявлено, едва узнаваемо и «следует воспринимать с подозрением» - нонсенс.
Последовательность имеет точное значение в логике: непротиворечивая теория - это теория, в которой не все утверждения могут быть доказаны. В классической логике, это равносильно отсутствию противоречия, то есть теория противоречиваесли и только если есть заявление такоечто теория доказываеткак А и его отрицание ¬ A .A A ¬A
Так что же это значит в отношении лямбда-исчисления? Ничего такого. Лямбда-исчисление - это система переписывания, а не логическая теория.
Можно посмотреть лямбда-исчисление по отношению к логике. Рассматривайте переменные как представление гипотезы в доказательстве, лямбда-абстракции как доказательства в рамках определенной гипотезы (представленной переменной), а применение - как соединение условного доказательства и доказательства гипотезы. Тогда бета-правило соответствует упрощению доказательства, применяя modus ponens , фундаментальный принцип логики.
Это, однако, работает только в том случае, если условное доказательство сочетается с доказательством правильной гипотезы. Если у вас есть условное доказательство, предполагающее и у вас также есть доказательство n = 2 , вы не можете объединить их вместе. Если вы хотите, чтобы эта интерпретация лямбда-исчисления работала, вам нужно добавить ограничение, чтобы к условным доказательствам применялись только доказательства правильной гипотезы. Это называется системой типов , а ограничение - это правило ввода, которое гласит, что когда вы передаете аргумент функции, тип аргумента должен соответствовать типу параметра функции.n=3 n=2
Соответствие Карри-Говарда является параллелью между типизированными исчислениями и системами доказательств.
Типизированное исчисление, имеющее комбинатор с фиксированной точкой, такое как позволяет создать термин любого типа (попробуйте оценить Y ( λ x . X ) ), поэтому, если вы берете логическую интерпретацию через соответствие Карри-Ховарда, вы получаете противоречивую теорию , См. Противоречит ли Y комбинатор соответствию Карри-Говарда? Больше подробностей.Y Y(λx.x)
Это не имеет смысла для чистого лямбда-исчисления, то есть для лямбда-исчисления без типов.
Во многих типизированных исчислениях невозможно определить комбинатор с фиксированной точкой. Эти типизированные исчисления полезны с точки зрения их логической интерпретации, но не являются основой для языка программирования, полного по Тьюрингу. В некоторых типизированных исчислениях можно определить комбинатор с фиксированной точкой. Эти типизированные исчисления полезны в качестве основы для языка программирования, полного по Тьюрингу, но не в отношении их логической интерпретации.
В заключение:
источник
true
иfalse
, и предложения были вещи , которые имели Булевозначный выход. (и рассматривались только предложения по области вещей , где он делает выход A логическое значение).Я хотел бы добавить один к тому, что сказал @Giles.
Переписка Карри-Говард делает параллель между -терминами (точнее, типа из λ -терминов) и система доказательства.λ λ
Например, имеет тип a → ( b → a ) (где a → b означает «функция от a до b »), что соответствует логическому утверждению aλx.λy.x a→(b→a) a→b a b . Функция λ x . λ y . x y имеет тип ( a → b ) → ( a → b ) , соответствующий ( aa⟹(b⟹a) λx.λy.xy (a→b)→(a→b) . Мы можем преобразовать любой тип лямбда-исчисления в логическую тавтологию, в некотором смысле путем «сопоставления с образцом» в функциях.(a⟹b)⟹(a⟹b)
Проблема возникает, когда мы рассматриваем Y комбинатор, определенный как . Проблема возникает потому, что мы ожидаем, что Y-комбинатор, как комбинатор с «фиксированной точкой», будет иметь тип ( a → a ) → a (потому что он переводит функцию из типа в тот же тип и находит фиксированную точку для та функция, которая имеет этот тип). Преобразование это до логических доходностей заявления (λf.(λx.f(xx))(λx.f(xx)) (a→a)→a . Это противоречие(a⟹a)⟹a
Принятие в системе типов приводит к несовместимости системы типов. Это означает, что мы можем либо(a→a)→a
источник
fix
. Вы можете просто утверждают , что существует константа для каждого типа A . Это уже даст вам несовместимую систему в том, что касается CH, поскольку это будет означать, что каждый тип населён f i x ( λ x . X ) . Вы могли бы дополнительно добавить δ- правила, чтобы заставить f i x вычислять, и это превратило бы, скажем, STLC с натуральными числами в систему, полную по Тьюрингу, но вам не нужно добавлять эти вычислительные правила, и система все равно будет противоречивы.