scala – 了解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? 解决方法
请注意,您编写的内容不是Y组合子的实现. “Y组合子”是λ-演算中的特定“定点组合子”.术语g的“定点”只是一个点x,
g(x) = x “定点组合器”F是可用于“产生”固定点的术语.就是这样, g(F(g)) = F(g) 术语Y =λf.(λx.f(xx))(λx.f(xx))是服从该等式的许多人之一,即它是g(Y(g))= Y(g)感觉一个术语可以减少到另一个术语.此属性意味着包括Y的这些术语可用于在微积分中“编码递归”. 关于打字注意,Y组合器不能在简单类型的λ演算中输入.甚至在系统F的多态演算中也没有.如果你尝试输入它,你会得到一种“无限深度”.要键入它,您需要在类型级别进行递归.所以如果你想扩展,例如只需将λ-calculus键入一个小函数式编程语言,就可以将Y作为基元. 你不是在使用λ-calculus,而且你的语言已经带有递归.所以你写的是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 (编辑:李大同) 【声明】本站内容均来自网络,其相关言论仅代表作者个人观点,不代表本站立场。若无意侵犯到您的权利,请及时与联系站长删除相关内容! |