理解Y-组合器的实现

Question

我想详细了解一下我们是如何从Y-combinator的lambda演算表达式中得到的：

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)

我对函数式编程非常陌生，但我对lambda微积分和替代过程是如何工作的有很好的理解。然而，我很难理解我们是如何从正式表达到实现的。

此外，我还想知道如何告诉函数的类型和参数的number ，以及函数的返回类型(无论是什么lambdaE 211)

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中定点"combinator“的简单定义。直截了当，因为作为一个定点(几乎)跟随(几乎)的定义。

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被部分应用。(看起来，代码作者选择使用lambda来使其更加显式。)

现在，我们如何得出这个代码？维基百科那个Y f = f (Y f)。把它扩展到类似Scala的东西，我们有def Y(f) = f(Y(f))。在lambda演算中，这不是一个定义，它不允许直接递归，但它在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))