柯里化
在计算机科学中,柯里化(),又译为卡瑞化或加里化,是把接受多个参数的函数变换成接受一个单一参数(最初函数的第一个参数)的函数,并且返回接受余下的参数而且返回结果的新函数的技术。这个技术由克里斯托弗·斯特雷奇以逻辑学家哈斯凯尔·加里命名的,尽管它是Moses Schönfinkel和戈特洛布·弗雷格发明的。
在直觉上,柯里化声称「如果你固定某些参数,你将得到接受余下参数的一个函数」。所以对于有两个变量的函数formula_1,如果固定了formula_2,则得到有一个变量的函数formula_3。
在理论计算机科学中,柯里化提供了在简单的理论模型中,比如:只接受一个单一参数的lambda演算中,研究带有多个参数的函数的方式。
函数柯里化的对偶是Uncurrying,一种使用匿名单参数函数来实现多参数函数的方法。例如:
var foo = function(a) {
return function(b) {
return a * a + b * b;
这样调用上述函数:codice_1,或直接codice_2。
动机.
柯里化是一种处理函数中附有多个参数的方法,并在只允许单一参数的框架中使用这些函数。例如,一些分析技术只能用于具有单一参数的函数。现实中的函数往往有更多的参数。弗雷格表明,为单一参数情况提供解决方案已经足够了,因为可以将具有多个参数的函数转换为一个单参数的函数链。这种转变是现在被称为“柯里化”的过程。
在数学分析或计算机编程中,所有可能遇到的“普通”函数都可以被使用。但是,有些类别不可能使用柯里化;确实允许柯里化的最普通的类别是闭合的monoidal类别。一些编程语言几乎总是使用curried函数来实现多个参数;值得注意的例子是 ML 和 Haskell,在这两种情况下,所有函数都只有一个参数。这个属性是从lambda演算继承而来的,其中多参数的函数通常以柯里形式表示。
柯里化与部份求值是相关的,但不完全相同。在实作中,闭包的编程技术可以用来执行部份求值和一种卷曲,通过将参数隐藏在使用柯里化函数的环境中。
部份求值.
柯里化有如倣效接受多个参数的函数评估过程,若以纸笔手工作业,要周密地写出评估过程中的所有步骤。
例如,给定某一函数 formula_4:
要评估 formula_5 时,首先以 formula_6代入 formula_7
因为结果会是函数 formula_8的输出,所以可定义为一个新函数 formula_9 为 formula_10
接下来将 formula_8参数以 formula_12替换,产生了 formula_13
在纸上使用传统符号,上述过程通常是一次代入两个参数 formula_14的值就完成了。
而每个参数其实是依次序替换,在每一步替换的中介函数只能接受单一个参数。
以上范例有点缺陷,虽然应用上类似函数的部份求值。对柯里化的过程来说,但并非完全相同(见下文)。
示例.
柯里化(Currying)是产生一系列连锁函数的一种方法,其中每个函数只有一个参数。借由另一个柯里化之后的新函数,传回其它剩余参数的功能,将原本以多个参数应用的函数“隐藏”起来,如下所述。
给定带有 "x"和"y"两个参数的函数 "f",也就是,
formula_15
然后可以构造一个与原来的 "f" 相关的新函数 "h"x。这个函数的形式只有单一参数 "y",并给定该参数,则 "h"x 返回 "f"("x","y")。也就是,
formula_16.
在这里应该了解 "h"上的下标 "x"是当成隐藏作用的符号设施,或者说把一个参数放在一边,使原函数变成只带一个参数。柯里化(Currying)提供了符号标记上的技巧,将函数因而抽象化。
这个技巧要利用map或函数构造子。符号 formula_17用于表示抽象化的实际行为。
例如以 formula_18 这样子来表示:某个函数将一个参数 "y"映射到结果 "z"。
然后考虑从 "h""x" 记号中删掉下标 "x",就得到了一个 柯里化表示的代表符 "h";
而成为另一个给予 "x" 能把其“值”传回的不同函数 "h"x;它恰好是一个函数构造,其映射过程
可以用 formula_19 语句来表达,或者描述为一个将参数 "y"映射到结果 "z"的函数。也就是,
formula_20,
用不同代表符号(但意义相同)来看,
formula_21
函数 "h" 本身现在可用 "h"x 相似的表示,并写成
formula_22
能够负责并处理对开头"涉及"的函数参数。鉴于上述情况,柯里化的行为可被理解为一函数,给予某些任意的 "f",即涉及相关的 "h"函数可以产生 "h"的所述功能;论及 "f"。也就是,
formula_23
或相当于
formula_24
这说明了柯里化的基本性质:它是参数重新定位的机制,将原函数中的每一个参数绑定到不同的新函数,而返回另一个相关的函数。也就是给定函数 "f"原本传回一个“值”,则柯里化“构造”了一个新函数 "h" 而传回的是涉及 "f"的函数。另一种理解柯里化的不同方式,则意识到它只是一个代数游戏,符号的句法重新排列。人们不会问这些符号的“含义”是什么; 一个人只同意他们的重新排列规则。 要看出这一点,注意原来的函数 "f"本身可能写成
formula_25
与上面的函数 "h"互相比较,可以看出这两种形式都重新排列了括号,以及将逗号转换为箭头。回到前面的例子,
formula_26
然后有,
formula_27
作为上例柯里化的相等物。 添加一个参数到 "g" 然后给出
formula_28
以及
formula_29
剥除参数的方法或许更容易地理解,例如有四个参数的函数:
formula_30
经过上述操作,导出为形式
formula_31
这应用到三元组之上可得到
formula_32.
然后适当地写成柯里化形式
formula_33
一直继续玩著重新安排符号的代数游戏,最终导出了完全的柯里化形式
formula_34
对箭头运算符一般理解是右结合的,所以上面大部份的括号是多余的,在意义不变的情况下可以删除掉。因此,写成了很常见的
formula_35
也就是函数 "f"完全的柯里化形式。
定义.
从非形式的一般定义开始,柯里化是最容易理解的,然后再塑造它以适应许多不同的领域。
首先说明一些符号的标记法。
formula_36 表示从 formula_37 映射到 formula_38 的函数formula_39。
formula_40 表示从 formula_37 到 formula_38 的所有函数。
这里,formula_37 和 formula_38 可以是集合、或者是类型,或者它们可以是其它型别的物件,如下所述。
令 formula_45表示有序对,即笛卡尔乘积。
给定类型为formula_46 的函数formula_39,柯里化即构造或创建一个新的函数:
formula_48
也就是说,formula_49取一个类型为 formula_37的参数,并返回一个类型为 formula_51的函数。Uncurrying则相反。
集合论.
数理领域的集合论中,符号 formula_52用于表示从 formula_37集合映射到 formula_38集合的函数。柯里化是指从 formula_55映射到 formula_56的 formula_57函数,和从 formula_58之中映射,由 formula_59到formula_56的 formula_61函数,这些组合的自然变换。事实上是这种自然变换关系,阐述了出现在集合论中的指数符号。在集合的范畴论中 formula_52被称为指数物件。
函数空间.
在函数空间理论中,如泛函分析或拓扑的同伦,人们通常对拓扑空间之间的连续函数感兴趣。从 formula_37到 formula_38 "所有的"函数集,写成 formula_65(Hom函子)并使用 formula_52 来表示连续函数的子集。在这里的 formula_67是一一对应的
formula_68
而 uncurrying 是反向的映射。如果从 formula_37到 formula_38 的 formula_52集合为连续函数
给出了紧致开拓扑紧致开拓扑,而且如果 formula_38空间是局部豪斯多夫紧致的,那么 formula_67是一个连续函数,也是同胚。尽管可能有更多情况,当 formula_37,formula_38和 formula_52 是紧生成的时候,情况都是相同的。
这结果发展成了指数表示法
formula_77
有时称为指数法则。 而有用的推论是,一个函数若且唯若其柯里化形式是连续时,它才是连续的。另一个重要的结果是应用程序映射(在这种情况通常称为“评估”)是连续的(注意codice_3在计算机科学中的概念与此严格不同)。也就是说,
formula_78
当 formula_52是紧致开放的,而且 formula_38局部紧致的豪斯多夫时,那上述式子是连续的。这两个结果对于确立同伦的连续性非常重要,亦即当 formula_37是单位区间 formula_82,所以 formula_83能想成
就是从 formula_38 到formula_85的两个函数的同伦,或者等价地,是 formula_86中的单个(连续)路径。
域理论.
在序理论对于偏序集合的格,当格是给定的 Scott拓扑时,则 formula_67会是一个连续函数。为了提供 lambda演算的语义学,要先研究 Scott连续函数(因为普通集合理论不适合这样做)。更一般地说,现在研究 Scott连续函数的域理论中,含括了计算机算法的指称语义学。
请注意,Scott拓扑结构与拓扑空间范畴中可能遇到的许多常见拓扑结构完全不同; Scott拓扑通常更为精巧,而不是很严审的。连续性的概念使它出现在同伦类型理论中,粗略地说,两个计算机程序可以被认为是同伦的,如果他们可以“连续”地从一个重构到另一个,即计算得出相同的结果。
型别理论.
在型别理论中,对于计算机科学型别系统的一般概念,被形式化为一个具体的代数类型。例如写为 formula_36时,
意指那个 formula_37和 formula_38是一种类型,而 formula_91 箭头符号代表是类型构造函数,特别是指函数类型或箭头类型。类似地,类型的笛卡尔积是由 formula_92构造函数,而建构出的复合结构类型。
型别理论方法可以用 ML编程语言表达,而受启发衍生出的语言有:CaML,Haskell和F#。
逻辑.
在Curry-Howard下,柯里化和对偶柯里化的存在相当于逻辑定理formula_93,因为多元组(型别积, product type)对应于逻辑中的且连接,而函数类型对应于蕴涵。
历史.
「科里化」一词由克里斯托弗·斯特雷奇创造,以逻辑学家哈斯凯尔·加里命名。另外一个名词 "Schönfinkelisation" 则以Moses Schönfinkel命名。在数学历史中,这个原理可以追溯到1893年戈特洛布·弗雷格的工作。
生成维基百科快照图片,大概需要3-30秒!