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

Question

Я читаю книгу по λ-исчислению «Функциональное программирование через лямбда-исчисление» (Грег Майклсон).В книге автор вводит сокращенную запись для определения функций.Например,

def identity = λx.x

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

Позже, представляя рекурсию, он использует в качестве примера определение функции сложения, например:

def add x y = if iszero y then x else add (succ x) (pred y)

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

Таким образом, мой вопрос заключается в следующем: каковы теоретические или практические причины для наложения этого ограничения на себя?(о необходимости заменить все определенные имена до оценки функции)?Есть ли?

Answer 1

Я постараюсь опубликовать свой собственный ответ, как я его понимаю.

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

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

def something = something

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

Используя Y-комбинатор, мы всегда можем построить решение уравнения x = f (x) = f (f).(x)) = ... = f (f (f (f (x))) = .... для любого f,

, т. е. мы всегда можем переписать самоотносительное определение к определению, котороеоно не включает в себя

Answer 2

Причина в том, что мы хотим придерживаться правил лямбда-исчисления.Разрешение именам терминов обозначать что-либо, кроме немедленной замены, означало бы добавление рекурсивного выражения let к языку, что означало бы, что нам потребуется действительно более выразительная система (больше не лямбда-исчисление).

Вы можете думать об именах как о не более чем синтаксическом сахаре для оригинального лямбда-термина.Y-комбинатор - это именно тот способ, с помощью которого можно ввести рекурсию в систему, в которой она не встроена. Если книга, которую вы сейчас читаете, смущает вас, вам может понадобиться поискать в Интернете некоторые дополнительные ресурсы, объясняющие Y-комбинатор.