ecd*_*dhe 5 recursion functional-programming scala lambda-calculus y-combinator
我想在薄荷细节中理解我们如何设法从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演算以及替换过程的工作方式有了不错的理解.然而,我很难理解我们是如何从正式表达式实现的.
此外,我想知道如何告诉我的函数的参数的类型和数量以及它的返回类型是什么lambda？
首先,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))
请注意，您编写的内容不是Y组合器的实现。“Y组合器”是\xce\xbb-演算中的特定“定点组合器”。术语的“不动点”g就是x这样一个点：
g(x) = x \n“定点组合器”F是一个可用于“产生”定点的术语。也就是说，这样，
g(F(g)) = F(g)\n该项Y = \xce\xbbf.(\xce\xbbx.f (x x)) (\xce\xbbx.f (x x))是服从该等式的众多项之一，即，g(Y(g)) = Y(g)在某种意义上，一项可以化简为另一项。该属性指的是这样的术语，包括Y可用于在微积分中“编码递归”的术语。
关于输入，请注意Y组合器不能在简单输入的 \xce\xbb-calculus 中输入。即使在系统 F 的多态微积分中也不是这样。如果你尝试输入它，你会得到一种“无限深度”的类型。要键入它，您需要在类型级别进行递归。因此，如果您想将例如简单地键入 \xce\xbb-calculus 扩展到您提供的小型函数式编程语言Y作为原语提供的小型函数式编程语言。
不过，您没有使用 \xce\xbb-calculus，并且您的语言已经带有递归功能。所以你写的是 Scala 中定点“组合器”的简单定义。很简单，因为作为一个定点（几乎）可以立即从定义中得出。
\n\nY(f)(x) = f(Y(f))(x)\n对所有人来说都是如此x（并且它是一个纯函数），因此，
Y(f) = f(Y(f))\n这是定点方程。Y关于考虑方程类型的推断Y(f)(x) = f(Y(f))(x)并让
f : A => B\nY : C => D \n因为Y : C => D需要f : A => B输入，
C = A => B\n因为Y f : D是一个输入f : A => B是then
D = A\n并且由于输出Y f : D与f(Y(f)) : B与当时
D = B\n到目前为止我们已经，
\n\nY : (A => A) => A \n由于Y(f)应用于x,Y(f)是一个函数，所以
A = A1 => B1 \n对于某些类型A1和B1因此，
Y : ((A1 => B1) => (A1 => B1)) => A1 => B1\n