Каково было первоначальное намерение для создания лямбда-исчисления?

22

Я читал, что изначально Черч предложил -calculus как часть своей статьи «Постулаты логики» (которая читается плотно). Но Клини доказал свою «систему» ​​непоследовательной, после чего Черч извлек соответствующие вещи для своей работы по «эффективной вычислимости» и отказался от своей предыдущей работы над логикой.λ

Насколько я понимаю, -система и ее обозначения приняли форму как часть чего-то общего с логикой. Чего изначально пытался достичь Церковь, от чего он отказался позже? Каковы были первые причины создания -calculus?λλ

кандидат наук
источник
1
Опечатка в заголовке ...
user11153

Ответы:

26

Он хотел создать формальную систему для основ логики и математики, которая была бы проще, чем теория типов Рассела и теория множеств Цермело.

Основная идея состояла в том, чтобы добавить константу к нетипизированному лямбда-исчислению (или комбинаторной логике) и интерпретировать как выражение " удовлетворяет предикату ", а как выражение " ". С помощью правил, выражающих эти намерения, можно затем интерпретировать -фрагмент интуиционистской логики предикатов и неограниченного понимания, единственная проблема заключается в том, что, согласно парадоксу Карри, каждый выводим.ΞИксZZИксΞИксYИксYИкс

Смотрите стр. 7 из:

Кардоне и Хиндли, История лямбда-исчисления и комбинаторной логики , 2006: http://www.users.waitrose.com/~hindley/SomePapers_PDFs/2006CarHin,HistlamRp.pdf

А также введение в:

Барендрегт, Бандер и Деккерс, Системы илляционной комбинаторной логики, полные для исчисления высказываний и предикатов первого порядка , JSL 58-3 (1993): http://ftp.cs.ru.nl/CompMath.Found/ICL1.ps

Ульрик Бухгольц
источник
8
«Единственная проблема заключается в том, что по парадоксу Карри каждый выводим» :) Может быть полезно напомнить, что такое парадокс Карри: учитывая, что существует термин такой, что для каждого , тогда можно напишите которое является предложением таким, что , что дает то же противоречие, что и парадокс Рассела. В данном случае решающее значение имеет отсутствие завершения, которое мотивировало создание просто набранного -calculus, в котором каждый термин заканчивается. ИксYYMзнак равноM(YM)MY(¬)φφ¬φ λ
Коди
2

Я не уверен, было ли это частью мотивации для создания лямбда-исчисления, но лямбда-исчисление использовалось для решения проблемы Entscheidungs , поставленной Гильбертом в 1928 году. Тьюринг самостоятельно решил проблему Entscheidungs , представив машину Тьюринга.

Из статьи Википедии по проблеме Entscheidungs:

В 1936 году Алонзо Черч и Алан Тьюринг опубликовали независимые статьи [2], в которых показано, что общее решение проблемы Энтшайдунга невозможно, если предположить, что интуитивное понятие «эффективно вычисляемый» охватывается функциями, вычисляемыми машиной Тьюринга (или, что то же самое, выражаемые в лямбда-исчислении).

littleO
источник
1
Это «последствия» создания лямбда-исчисления ранее. Он просто использовал критически важную часть для определения эффективного расчета.
PhD