从“函数”的角度来看,y组合子是一个计算机科学的概念。大多数程序员根本不了解组合子,如果他们听说过的话。
什么是y组合子? 组合符是如何工作的? 它们有什么用? 它们在过程语言中有用吗?
从“函数”的角度来看,y组合子是一个计算机科学的概念。大多数程序员根本不了解组合子,如果他们听说过的话。
什么是y组合子? 组合符是如何工作的? 它们有什么用? 它们在过程语言中有用吗?
当前回答
匿名的递归
定点组合子是一种根据定义满足等价的高阶函数固定
forall f. fix f = f (fix f)
固定f表示定点方程x的解
x = f x
自然数的阶乘可以用
fact 0 = 1
fact n = n * fact (n - 1)
在一般/μ-递归函数上使用固定的、任意的构造证明可以在没有匿名自指性的情况下导出。
fact n = (fix fact') n
在哪里
fact' rec n = if n == 0
then 1
else n * rec (n - 1)
这样
fact 3
= (fix fact') 3
= fact' (fix fact') 3
= if 3 == 0 then 1 else 3 * (fix fact') (3 - 1)
= 3 * (fix fact') 2
= 3 * fact' (fix fact') 2
= 3 * if 2 == 0 then 1 else 2 * (fix fact') (2 - 1)
= 3 * 2 * (fix fact') 1
= 3 * 2 * fact' (fix fact') 1
= 3 * 2 * if 1 == 0 then 1 else 1 * (fix fact') (1 - 1)
= 3 * 2 * 1 * (fix fact') 0
= 3 * 2 * 1 * fact' (fix fact') 0
= 3 * 2 * 1 * if 0 == 0 then 1 else 0 * (fix fact') (0 - 1)
= 3 * 2 * 1 * 1
= 6
这个形式证明
fact 3 = 6
系统地使用定点组合子等价来重写
fix fact' -> fact' (fix fact')
微积分
无类型lambda演算形式主义包含在上下文无关的语法中
E ::= v Variable
| λ v. E Abstraction
| E E Application
v在变量范围内,和约简规则一起
(λ x. B) E -> B[x := E] Beta
λ x. E x -> E if x doesn’t occur free in E Eta
Beta约简用表达式(“参数”)e替换抽象(“函数”)体B中变量x的所有自由出现。Eta约简消除了冗余抽象。它有时在形式主义中被省略。不适用约简规则的不可约表达式是正常形式或规范形式。
λ x y. E
是简写
λ x. λ y. E
(抽象multiarity),
E F G
是简写
(E F) G
(应用程序left-associativity),
λ x. x
and
λ y. y
alpha-equivalent。
抽象和应用是lambda演算中仅有的两个“语言原语”,但它们允许对任意复杂的数据和操作进行编码。
教会数字是一种自然数的编码,类似于花生公理化自然数。
0 = λ f x. x No application
1 = λ f x. f x One application
2 = λ f x. f (f x) Twofold
3 = λ f x. f (f (f x)) Threefold
. . .
SUCC = λ n f x. f (n f x) Successor
ADD = λ n m f x. n f (m f x) Addition
MULT = λ n m f x. n (m f) x Multiplication
. . .
一个正式的证明
1 + 2 = 3
使用beta约简重写规则:
ADD 1 2
= (λ n m f x. n f (m f x)) (λ g y. g y) (λ h z. h (h z))
= (λ m f x. (λ g y. g y) f (m f x)) (λ h z. h (h z))
= (λ m f x. (λ y. f y) (m f x)) (λ h z. h (h z))
= (λ m f x. f (m f x)) (λ h z. h (h z))
= λ f x. f ((λ h z. h (h z)) f x)
= λ f x. f ((λ z. f (f z)) x)
= λ f x. f (f (f x)) Normal form
= 3
组合子
在lambda微积分中,组合子是不包含自由变量的抽象。最简单的,I,单位组合子
λ x. x
同构的恒等函数
id x = x
这样的组合子是像SKI系统这样的组合子计算器的基本操作符。
S = λ x y z. x z (y z)
K = λ x y. x
I = λ x. x
减少不是强归一化;并不是所有的可约化表达式,“重解”,在约简下收敛到正常形式。一个简单的例子是ω ω组合子的发散应用
λ x. x x
本身:
(λ x. x x) (λ y. y y)
= (λ y. y y) (λ y. y y)
. . .
= _|_ Bottom
减少最左边的子表达式(“头”)是优先的。应用顺序在替换前规范化参数,常规顺序则不然。这两种策略类似于渴望求值(例如C)和懒惰求值(例如Haskell)。
K (I a) (ω ω)
= (λ k l. k) ((λ i. i) a) ((λ x. x x) (λ y. y y))
在热切应用阶beta缩减下发散
= (λ k l. k) a ((λ x. x x) (λ y. y y))
= (λ l. a) ((λ x. x x) (λ y. y y))
= (λ l. a) ((λ y. y y) (λ y. y y))
. . .
= _|_
因为在严格的语义上
forall f. f _|_ = _|_
但在惰性法阶约简下是收敛的
= (λ l. ((λ i. i) a)) ((λ x. x x) (λ y. y y))
= (λ l. a) ((λ x. x x) (λ y. y y))
= a
如果一个表达式具有正规形式,则用正规阶beta缩减法可以找到它。
Y
Y定点组合子的基本性质
λ f. (λ x. f (x x)) (λ x. f (x x))
是由
Y g
= (λ f. (λ x. f (x x)) (λ x. f (x x))) g
= (λ x. g (x x)) (λ x. g (x x)) = Y g
= g ((λ x. g (x x)) (λ x. g (x x))) = g (Y g)
= g (g ((λ x. g (x x)) (λ x. g (x x)))) = g (g (Y g))
. . . . . .
等效
Y g = g (Y g)
同构于
fix f = f (fix f)
无类型lambda演算可以在一般/μ递归函数上编码任意构造证明。
FACT = λ n. Y FACT' n
FACT' = λ rec n. if n == 0 then 1 else n * rec (n - 1)
FACT 3
= (λ n. Y FACT' n) 3
= Y FACT' 3
= FACT' (Y FACT') 3
= if 3 == 0 then 1 else 3 * (Y FACT') (3 - 1)
= 3 * (Y FACT') (3 - 1)
= 3 * FACT' (Y FACT') 2
= 3 * if 2 == 0 then 1 else 2 * (Y FACT') (2 - 1)
= 3 * 2 * (Y FACT') 1
= 3 * 2 * FACT' (Y FACT') 1
= 3 * 2 * if 1 == 0 then 1 else 1 * (Y FACT') (1 - 1)
= 3 * 2 * 1 * (Y FACT') 0
= 3 * 2 * 1 * FACT' (Y FACT') 0
= 3 * 2 * 1 * if 0 == 0 then 1 else 0 * (Y FACT') (0 - 1)
= 3 * 2 * 1 * 1
= 6
(乘法延迟,汇流)
对于丘奇无类型lambda演算,除了Y之外,已经证明存在一个递归可枚举的无穷个定点组合子。
X = λ f. (λ x. x x) (λ x. f (x x))
Y' = (λ x y. x y x) (λ y x. y (x y x))
Z = λ f. (λ x. f (λ v. x x v)) (λ x. f (λ v. x x v))
Θ = (λ x y. y (x x y)) (λ x y. y (x x y))
. . .
法阶beta约简使未扩展的无类型lambda演算成为一个图灵完全重写系统。
在Haskell中,可以优雅地实现定点组合子
fix :: forall t. (t -> t) -> t
fix f = f (fix f)
Haskell的惰性在所有子表达式都被求值之前归一到有限。
primes :: Integral t => [t]
primes = sieve [2 ..]
where
sieve = fix (\ rec (p : ns) ->
p : rec [n | n <- ns
, n `rem` p /= 0])
大卫·特纳:丘奇的论文和函数式编程 阿朗佐·丘奇:初等数论的一个不可解问题 微积分 Church-Rosser定理
其他回答
不动点组合子(或不动点运算符)是一种高阶函数,用于计算其他函数的一个不动点。此操作与编程语言理论相关,因为它允许以重写规则的形式实现递归,而不需要语言的运行时引擎的显式支持。(src维基百科)
上面的大多数答案描述了y组合子是什么,但没有描述它的用途。
用不动点组合子来证明lambda演算是图灵完备的。这是计算理论中一个非常重要的结果,为函数式编程提供了理论基础。
学习不动点组合子也帮助我真正理解了函数式编程。但我从未发现它们在实际编程中有任何用处。
如果你准备好长篇大论,Mike Vanier有一个很好的解释。长话短说,它允许您在一种不一定支持递归的语言中实现递归。
下面是Y-Combinator和Factorial函数的JavaScript实现(来自Douglas Crockford的文章,可在http://javascript.crockford.com/little.html上找到)。
function Y(le) {
return (function (f) {
return f(f);
}(function (f) {
return le(function (x) {
return f(f)(x);
});
}));
}
var factorial = Y(function (fac) {
return function (n) {
return n <= 2 ? n : n * fac(n - 1);
};
});
var number120 = factorial(5);
以下是对尼古拉斯·曼库索(Nicholas Mancuso)在回答中提到的文章(完全值得一读)中提到的原始问题的回答,以及其他答案:
什么是y组合子?
y组合子是一个“函数”(或高阶函数——一个作用于其他函数的函数),它接受一个参数,这是一个非递归的函数,并返回该函数的一个递归版本。
有点递归=),但更深入的定义:
一个组合子-就是一个没有自由变量的lambda表达式。 自由变量-是一个变量,不是一个约束变量。 绑定变量—包含在lambda表达式体中的变量,该变量名作为其参数之一。
另一种思考方式是,combinator是这样一个lambda表达式,在其中,你可以在任何地方用它的定义替换一个组合子的名称,并且一切都仍然有效(如果combinator在lambda体中包含对自身的引用,你将进入一个无限循环)。
y组合子是一个定点组合子。
函数的不动点是函数定义域中映射到函数自身的一个元素。 也就是说,如果f(c) = c, c是函数f(x)的一个不动点 这意味着f(f(…f(c)…))= fn(c) = c
组合符是如何工作的?
下面的例子假设强+动态类型:
惰性(正规阶)y组合子: 此定义适用于具有lazy(也称为deferred, call-by-need)求值的语言——该求值策略将表达式的求值延迟到需要它的值时。
Y = λf.(λx.f(x x)) (λx.f(x x)) = λf.(λx.(x x)) (λx.f(x x))
这意味着,对于给定的函数f(它是非递归函数),可以通过计算λx得到对应的递归函数。F (x x)然后把这个表达式应用到自身上。
严格(应用阶)y组合子: 这个定义适用于具有严格求值策略(也包括热切求值和贪婪求值策略)的语言,在这种策略中,表达式一旦绑定到变量就会被求值。
Y = λf.(λx.f(λy.((x x) y))) (λx.f(λy.((x x) y))) = λf.(λx.(x x)) (λx.f(λy.((x x) y)))
它本质上和lazy一样,只是有一个额外的λ包装器来延迟lambda的体计算。我问了另一个问题,和这个话题有点相关。
它们有什么用?
借用Chris Ammerman的回答:Y-combinator泛化递归,抽象其实现,从而将其与函数的实际工作分离。
尽管Y-combinator有一些实际应用,但它主要是一个理论概念,理解它将扩展你的整体视野,并有可能提高你的分析和开发技能。
它们在过程语言中有用吗?
正如Mike Vanier所说:在许多静态类型的语言中都可以定义Y组合子,但是(至少在我看到的例子中)这样的定义通常需要一些不明显的类型技巧,因为Y组合子本身没有直接的静态类型。这超出了本文的范围,所以我不再进一步提及
正如Chris Ammerman所提到的:大多数过程式语言都有静态类型。
所以这个问题的答案是,不是真的。