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

44

На странице Википедии для комбинаторов с фиксированной точкой написан довольно загадочный текст

Y комбинатор является примером того, что делает лямбда-исчисление непоследовательным. Поэтому к этому следует относиться с подозрением. Однако комбинатор Y можно считать безопасным, если он определен только в математической логике.

Я вступил в какой-то шпионский роман? Что в мире подразумевается под утверждениями о том, что калькуляция является «противоречивой» и что ее следует «рассматривать с подозрением» ?λ

Бен И.
источник
3
FWIW, этот абзац был в статье в Википедии с января 2014 года, когда он был представлен в этой массовой переписке почти всей статьи .
Илмари

Ответы:

51

Оно вдохновлено реальными событиями, но то, как оно заявлено, едва узнаваемо и «следует воспринимать с подозрением» - нонсенс.

Последовательность имеет точное значение в логике: непротиворечивая теория - это теория, в которой не все утверждения могут быть доказаны. В классической логике, это равносильно отсутствию противоречия, то есть теория противоречиваесли и только если есть заявление такоечто теория доказываеткак А и его отрицание ¬ A .AA¬A

Так что же это значит в отношении лямбда-исчисления? Ничего такого. Лямбда-исчисление - это система переписывания, а не логическая теория.

Можно посмотреть лямбда-исчисление по отношению к логике. Рассматривайте переменные как представление гипотезы в доказательстве, лямбда-абстракции как доказательства в рамках определенной гипотезы (представленной переменной), а применение - как соединение условного доказательства и доказательства гипотезы. Тогда бета-правило соответствует упрощению доказательства, применяя modus ponens , фундаментальный принцип логики.

Это, однако, работает только в том случае, если условное доказательство сочетается с доказательством правильной гипотезы. Если у вас есть условное доказательство, предполагающее и у вас также есть доказательство n = 2 , вы не можете объединить их вместе. Если вы хотите, чтобы эта интерпретация лямбда-исчисления работала, вам нужно добавить ограничение, чтобы к условным доказательствам применялись только доказательства правильной гипотезы. Это называется системой типов , а ограничение - это правило ввода, которое гласит, что когда вы передаете аргумент функции, тип аргумента должен соответствовать типу параметра функции.n=3n=2

Соответствие Карри-Говарда является параллелью между типизированными исчислениями и системами доказательств.

  • типы соответствуют логическим утверждениям;
  • сроки соответствуют доказательствам;
  • обитаемые типы (т. е. типы, в которых есть термин этого типа) соответствуют истинным утверждениям (т. е. таким утверждениям, что существует доказательство этого утверждения);
  • оценка программы (т. е. правила, такие как бета) соответствуют преобразованиям доказательств (которые лучше преобразовали правильные доказательства в правильные доказательства).

Типизированное исчисление, имеющее комбинатор с фиксированной точкой, такое как позволяет создать термин любого типа (попробуйте оценить Y ( λ x . X ) ), поэтому, если вы берете логическую интерпретацию через соответствие Карри-Ховарда, вы получаете противоречивую теорию , См. Противоречит ли Y комбинатор соответствию Карри-Говарда? Больше подробностей.YY(λx.x)

Это не имеет смысла для чистого лямбда-исчисления, то есть для лямбда-исчисления без типов.

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

В заключение:

  • Лямбда-исчисление не является «противоречивым», эта концепция не применяется.
  • Типизированный лямбда - исчисление , что присваивает тип для каждого члена лямбды противоречив. Некоторые типизированные лямбда-исчисления похожи на это, другие делают некоторые термины нетипичными и последовательными.
  • Типизированные лямбда-исчисления не являются единственным смыслом для лямбда-исчисления, и даже противоречивые типизированные лямбда-исчисления являются очень полезными инструментами - просто чтобы не доказать что-либо.
Жиль "ТАК - перестань быть злым"
источник
2
Вау, мне многое нужно распаковать здесь. Спасибо за подробное объяснение. Мне понадобится некоторое время, чтобы попытаться все это проглотить.
Бен I.
4
Технически, рассматривая нетипизированный как un i typed, вы можете сделать CH-соответствие между нетипизированным лямбда-исчислением и логикой. Это просто очень, очень скучная (и непоследовательная) логика. Корректоры вроде NuPRL немного мутят воду. Объектный язык NuPRL содержит нетипизированное лямбда-исчисление, и вы можете легко определить Y-комбинатор. NuPRL разделяет вещи немного по-другому, поэтому у него есть система уточнения типов, а не система типов, и упражнение состоит не в том, чтобы создавать хорошо типизированные термины, а в том, что касается производных от типов.
Дерек Элкинс,
Это только я или странно навязывать парадигму «предложения как типы» нетипизированному лямбда-исчислению? Я всегда видел , что люди говорят о логике в нетипизированном лямбда - исчислении путем введения конкретных объектов , чтобы быть логическими значениями trueи false, и предложения были вещи , которые имели Булевозначный выход. (и рассматривались только предложения по области вещей , где он делает выход A логическое значение).
Тривиально (доказывает каждое утверждение) и содержит противоречия два разных свойства. Хотя они являются эквивалентными в классической логике, для паранепротиворечивых логик система может быть непоследовательной и нетривиальной.
Темыр
1
«Несогласованный» для логики, основанной на λ-исчислении, означает «назначает каждый тип какому-либо термину», а не «назначает тип каждому термину» (хотя первое следует из второго); Есть много языков на основе λ-исчисления, которые соответствуют противоречивым логикам, но где не каждый термин λ-исчисления является типичным.
Джонатан Каст
6

Я хотел бы добавить один к тому, что сказал @Giles.

Переписка Карри-Говард делает параллель между -терминами (точнее, типа из λ -терминов) и система доказательства.λλ

Например, имеет тип a ( b a ) (где a b означает «функция от a до b »), что соответствует логическому утверждению aλx.λy.xa(ba)abab . Функция λ x . λ y . x y имеет тип ( a b ) ( a b ) , соответствующий ( aa(ba)λx.λy.xy(ab)(ab) . Мы можем преобразовать любой тип лямбда-исчисления в логическую тавтологию, в некотором смысле путем «сопоставления с образцом» в функциях.(ab)(ab)

Проблема возникает, когда мы рассматриваем Y комбинатор, определенный как . Проблема возникает потому, что мы ожидаем, что Y-комбинатор, как комбинатор с «фиксированной точкой», будет иметь тип ( a a ) a (потому что он переводит функцию из типа в тот же тип и находит фиксированную точку для та функция, которая имеет этот тип). Преобразование это до логических доходностей заявления (λf.(λx.f(xx))(λx.f(xx))(aa)a . Это противоречие(aa)a

(aa)aaa(¬a¬a)(¬a)¬a¬a

Принятие в системе типов приводит к несовместимости системы типов. Это означает, что мы можем либо(aa)a

  • Запретить типы, такие как в системе типов (это дает вам просто набранный λ- калькулятор ), или(aa)aλ
  • Жить с системой типов, несовместимой как система логического вывода.
Неконтекстовое правописание
источник
1
CH связывает типы с предложениями, программы с доказательствами и даже сокращения с преобразованиями доказательств. Это не только о типах. Далее тавтологии соответствуют только обитаемые типы. является (полиморфным) типом лямбда-исчисления, даже если его не населяют термины. Предполагая, что вы имеете в виду такие типы, как a . ( a a ) a , то принятие таких типов совершенно нормально, вопрос в том, есть ли у этого типа обитатель или нет. И наоборот, мы можем добавить примитивные термины в STLC, которые сделают соответствующую логику несовместимой без расширения системы типов.a,b.aba.(aa)a
Дерек Элкинс,
@DerekElkins, что за примитивные термины? Кроме того, если я правильно понимаю, это просто предположить, что (a -> a) -> a всегда заселен, что приводит к несоответствию? Таким образом, нет больше несоответствия с языком программирования, который требует доказательства завершения? Или есть какой-либо другой источник противоречий в нетипизированном или лямбда-исчислении Хиндли-Милнера?
Hibou57
1
@ Hibou57 Примитивные термины, то есть константы, как fix. Вы можете просто утверждают , что существует константа для каждого типа A . Это уже даст вам несовместимую систему в том, что касается CH, поскольку это будет означать, что каждый тип населён f i x ( λ x . X ) . Вы могли бы дополнительно добавить δ- правила, чтобы заставить f i x вычислять, и это превратило бы, скажем, STLC с натуральными числами в систему, полную по Тьюрингу, но вам не нужно добавлять эти вычислительные правила, и система все равно будет противоречивы. fixAAfix(λx.x)δfix
Дерек Элкинс