Понимание реализации Y-Combinator

Question

Я бы хотел в деталях разобраться, как нам удалось получить от выражения лямбда-исчисления Y-комбинатора:

Y = λf.(λx.f (x x)) (λx.f (x x))

до следующей реализации (в Scala):

def Y[A, B](f: (A => B) => A => B): A => B = (x: A) => f(Y(f))(x)

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

Кроме того, мне бы хотелось узнать, как сказать type и number из аргументов моей функции и типа возврата любого лямбда ?

Answer 1

Обратите внимание, что то, что вы написали, не является реализацией комбинатора Y.«Y комбинатор» является конкретным «комбинатором с фиксированной точкой» в λ-исчислении.«Фиксированная точка» термина g - это просто точка x, такая, что

g(x) = x 

«Комбинатор с фиксированной точкой» F - это термин, который можно использовать для "производить "точки исправления.То есть, так что

g(F(g)) = F(g)

Термин Y = λf.(λx.f (x x)) (λx.f (x x)) является одним из многих, которому подчиняется это уравнение, т.е. он таков, что g(Y(g)) = Y(g) в том смысле, что один термин может быть сведен к другому.Это свойство означает, что такие термины, включая Y, могут использоваться для «кодирования рекурсии» в исчислении.

Относительно ввода отметим, что комбинатор Y не может быть введен в простой тип λ-исчисления.Даже в полиморфном исчислении системы F. Если вы попытаетесь набрать его, вы получите тип «бесконечной глубины».Чтобы набрать его, вам нужна рекурсия на уровне типа.Поэтому, если вы хотите расширить, например, просто набранное λ-исчисление, до небольшого функционального языка программирования, вы предоставляете Y в качестве примитива.

Вы не работаете с λ-исчислением, и ваш язык уже поставляется с рекурсией.Итак, то, что вы написали, является прямым определением «комбинатора» с фиксированной точкой в ​​Scala.Просто, потому что быть фиксированной точкой следует (почти) немедленно из определения.

Y(f)(x) = f(Y(f))(x)

верно для всех x (и это чистая функция), поэтому

Y(f) = f(Y(f))

, которое является уравнением для фиксированных точек.Что касается логического вывода для типа Y, рассмотрим уравнение Y(f)(x) = f(Y(f))(x) и пусть

f : A => B
Y : C => D 

, поскольку Y : C => D принимает f : A => B в качестве входного значения,

C = A => B

поскольку Y f : D является входом f : A => B, то

D = A

, и поскольку выход Y f : D такой же, как у f(Y(f)) : B, то

D = B

до сих пор мыесть,

Y : (A => A) => A 

, поскольку Y(f) применяется к x, Y(f) - функция, поэтому

A = A1 => B1 

для некоторых типов A1 и B1 итаким образом,

Y : ((A1 => B1) => (A1 => B1)) => A1 => B1

Answer 2

Во-первых, код Scala - это длинный путь написания:

def Y[A, B](f: (A => B) => A => B): A => B = f(Y(f))

Здесь f применяется частично.(Похоже, автор кода решил использовать лямбду, чтобы сделать это более явным.)

Теперь, как мы можем прийти к этому коду? Википедия отмечает , что Y f = f (Y f).Расширяя это до чего-то, похожего на Scala, мы имеем def Y(f) = f(Y(f)).Это не сработает как определение в лямбда-исчислении, которое не допускает прямой рекурсии, но работает в Scala.Чтобы сделать это действительным Scala, нам нужно добавить типы.Добавление типа к f приводит к:

def Y(f: (A => B) => A => B) = f(Y(f))

Поскольку A и B свободны, нам нужно сделать их параметры типа:

def Y[A, B](f: (A => B) => A => B) = f(Y(f))

Поскольку это рекурсивнонам нужно добавить тип возврата:

def Y[A, B](f: (A => B) => A => B): A => B = f(Y(f))