Почему важно, чтобы функции были анонимными в лямбда-исчислении?

19

Я смотрел лекцию Джима Вейриха « Приключения в функциональном программировании ». В этой лекции он вводит понятие Y-комбинаторов, которое, по существу, находит неподвижную точку для функций более высокого порядка.

Один из мотивов, как он упоминает, состоит в том, чтобы иметь возможность выражать рекурсивные функции с использованием лямбда-исчисления, так что теория Чёрча (все, что эффективно вычисляется, может быть вычислено с использованием лямбда-исчисления) остается.

Проблема в том, что функция не может вызывать себя просто так, потому что лямбда-исчисление не допускает именованных функций, т. Е.

N(Икс,Y)знак равноИкс+Y

не может носить имя ' ', оно должно быть определено анонимно:N

(Икс,Y)Икс+Y

Почему для лямбда-исчисления важно иметь функции, которые не названы? Какой принцип нарушается, если есть именованные функции? Или я просто неправильно понял видео Джима?

Рохан Прабху
источник
4
Это не звучит важно вообще. Вы можете назначить переменной а затем вы дали имя функции. n(x,t)x+yN
Ювал Фильмус
@YuvalFilmus да, вы можете привязать имя к функции. Я думаю, что настоящий вопрос здесь, загадка, заключается в том, почему (в лямбда-исчислении) функция не может вызывать саму себя с таким именем? Зачем нам нужна техника типа оператора Y для выполнения рекурсивных функций? Я надеюсь, что мой ответ ниже поможет.
Jerry101
1
@ Jerry101 Историческая причина отсутствия самоприменения заключается в том, что калькуляция была задуманна как основа математики, а способность к самоприложению сразу же делает такую ​​основу непоследовательной. Таким образом, эта кажущаяся неспособность (которую мы знаем теперь можно обойти) является конструктивной особенностью λ- калькуляции. λλ
Мартин Бергер
@MartinBerger, пожалуйста, скажи больше. Непонятна по причине в моем ответе? Или по другой причине?
Jerry101
1
@ Jerry101 Непоследовательно в том смысле, что вы можете доказать 0 = 1 в таком фундаменте математики. После Клини и Россер показали несостоятельность чистого, нетипизированного -исчисления, то просто-типизированные λ -исчисления было разработано в качестве альтернативы , которая не позволяет нам определить фикс-точечные combintors , такие как Y . Но если вы добавляете рекурсию к λ- вычислению с простым типом, она снова становится противоречивой, потому что каждый тип населяется не заканчивающейся программой. λλYλ
Мартин Бергер

Ответы:

24

Основная теорема, касающаяся этого вопроса, принадлежит британскому математику конца 16 века по имени Уильям Шекспир . Его самая известная статья на эту тему под названием « Ромео и Джульетта » была опубликована в 1597 году, хотя исследовательская работа была проведена несколькими годами ранее, но вдохновила таких предшественников, как Артур Брук и Уильям Пейнтер.

Его основной результат, изложенный в акте II. Сцена II , это знаменитая теорема :

Что в имени? то, что мы называем розой под
любым другим именем, будет пахнуть сладко;

Эта теорема может быть интуитивно понята как «имена не способствуют значению».

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

Как было отмечено Шекспира, имена могут быть изменены без изменения значения, операция , которая позже назвали конверсияα от Алонзо церкви и его последователей. Как следствие, не обязательно просто определить, что обозначается именем. В связи с этим возникает множество вопросов, таких как разработка концепции среды, в которой указывается связь между значением и именем, и правила, позволяющие узнать текущую среду, когда вы пытаетесь определить значение, связанное с именем. Некоторое время это сбивало с толку компьютерщиков, создавая технические трудности, такие как печально известная проблема Фунарга, Среды остаются проблемой в некоторых популярных языках программирования, но обычно считается, что физически небезопасно быть более конкретным, почти таким же смертоносным, как пример, разработанный Шекспиром в его статье.

Эта проблема также близка к проблемам, возникающим в теории формального языка , когда алфавиты и формальные системы должны быть определены с точностью до изоморфизма , чтобы подчеркнуть, что символы алфавитов являются абстрактными объектами , независимо от того, как они «материализуются» как элементы из некоторого набора.

Этот главный результат Шекспира показывает также, что наука тогда расходилась с магией и религией, где существо или смысл могли иметь истинное имя .

Вывод из всего этого заключается в том, что для теоретической работы зачастую удобнее не быть обремененным именами, даже если это может быть проще для практической работы и повседневной жизни. Но помните, что не все, кого зовут Мама, это ваша мать.

Примечание :
этот вопрос был рассмотрен недавно американским логиком ХХ века Гертрудой Стейн . Однако ее коллеги-математики все еще размышляют над точными техническими последствиями ее основной теоремы :

Роза это роза это роза это роза.

опубликовано в 1913 году в коротком сообщении под названием «Священная Эмилия».

Babou
источник
3
Дополнительное примечание: в последние десятилетия «роза» (в компьютерных науках) в основном была заменена на «foobar» (и его части) в качестве канонического примера имени, которое так же хорошо, как и любое другое. Это предпочтение, по- видимому, было введено американскими железнодорожными инженерами.
FrankW
Тем не менее, канонические имена для часто используемых понятий важны для эффективного общения.
Рафаэль
1
@ Рафаэль Согласен, но я бы отнес это к категории повседневной жизни. И как мы узнаем границы действительно канонического? Тем не менее, я часто испытываю беспокойство, когда вижу, что студенты принимают всю терминологию, обозначения и определения (или даже то, как формулируются некоторые теоремы) для данной Богом неизменной истины. Даже здесь, на SE, студенты задают вопросы, не понимая, что мы можем не знать их обозначения или определения, которые они используют в классе. Магия настоящих имен не умирает легко.
Бабу
10

Я хотел бы высказать мнение, которое отличается от мнений @babou и @YuvalFilmus: для чистого λ- калькулятора жизненно важно иметь анонимные функции. Проблема с наличием только именованных функций заключается в том, что вам нужно заранее знать, сколько имен вам потребуется. Но в чистом λ- калькуляторе у вас нет априорной привязки к числу используемых функций (подумайте о рекурсии), поэтому вы либо используете (1) анонимные функции, либо (2) вы идете по маршруту π- калькулятора и предоставляете свежий комбинатор имен ( ν x . P в π- калькуляторе), который дает неисчерпаемый запас свежих имен во время выполнения.λλπνИкс,пπ

λλλ

LеTезнак равноMяNN(λе,N)Mλ

Мартин Бергер
источник
1
Я думаю, что ОП хотела иметь возможность называть функции, а не запрещать анонимные. Тем не менее, я думаю, что любое требование λ-исчисления, касающееся необходимости анонимных функций, будет также отображаться в таких языках, как Lisp / Scheme или ML. В случае Lisp / Scheme мета-цикличность оценщиков должна позволять создавать новые имена по мере необходимости, хотя я не уверен, что хотел бы этого в формальной системе. Использование неограниченного числа функций не обязательно является проблемой, когда рекурсия позволяет локальное повторное использование уже используемых имен.
Бабу
λλ
Должна ли последняя строка читать (лямбда ф. N) M?
Джо Человек
@JoethePerson Да, хорошо заметили. Исправлена. Благодарю.
Мартин Бергер
4

Я считаю, что идея в том, что имена не нужны. Все, что требует имен, может быть написано как анонимные функции.

Вы можете думать о лямбда-исчислении как о языке ассемблера. Кто-то в лекции по сборке может сказать: «На языке ассемблера нет объектно-ориентированных деревьев наследования». Затем вы могли бы придумать умный способ реализации деревьев наследования, но это не главное. Дело в том, что деревья наследования не требуются на самом базовом уровне программирования физического компьютера.

В лямбда-исчислении дело в том, что имена не требуются для описания алгоритма на самом базовом уровне.

Настоящий Джон Коннор
источник
4

Пока что я получаю удовольствие от 3 ответов, особенно от анализа Шекспира в babou, но они не проливают свет на то, что, по моему мнению, является сутью вопроса.

λ-исчисление связывает имена с функциями всякий раз, когда вы применяете функцию к функции. Проблема не в отсутствии имен.

«Проблема в том, что функция не может вызвать сама себя», ссылаясь на свое имя.

(В чистом Лиспе привязка имени -> функции находится вне области действия внутри тела функции. Чтобы функция вызывала себя по имени, функция должна ссылаться на среду, которая ссылается на функцию. Чистый Лисп не имеет циклические структуры данных. Нечистый Лисп делает это, изменяя среду, на которую ссылается функция.)

Как указал @MartinBerger, историческая причина, по которой λ-исчисление не позволяет функции вызывать себя по имени, была попыткой исключить парадокс Карри, когда он пытался использовать λ-исчисление в качестве основы математики, включая дедуктивную логику. Это не сработало, поскольку такие методы, как Y-комбинатор, допускают рекурсию даже без ссылки на себя.

Из Википедии:

Если мы можем определить функцию r = (λ.x x x ⇒ y)тогда r r = (r r ⇒ y).

Если r rэто правда, то yэто правда. Если r rложно, то r r ⇒ yверно, что является противоречием. Так yчто верно, и, как yи любое утверждение, любое утверждение может быть доказано.

r rявляется не заканчивающимся вычислением. Логическим r rсчитается выражение для значения, которого не существует.

Jerry101
источник
λ,Икс ИксИксИксИксИкс
@RohanPrabhu λ.x x xпереводит на Лисп как (lambda (x) (x x))и на JavaScript как function (x) {return x(x);}. x⇒yзначит x implies y, примерно так же, как (NOT x) OR y. См en.wikipedia.org/wiki/Lambda_calculus
Jerry101
Спасибо за ответ на этот неловкий вопрос новичка!
Рохан Прабху