# 柯里化

var foo = function(a) {
return function(b) {
return a * a + b * b;
}
}


## 动机

### 示例

${\displaystyle f(x,y)}$

${\displaystyle h_{x}(y)=f(x,y)}$.

${\displaystyle h_{x}=(y\mapsto f(x,y))}$,

${\displaystyle h(x)=(y\mapsto f(x,y))}$

${\displaystyle h=(x\mapsto (y\mapsto f(x,y)))}$

${\displaystyle {\text{curry}}=(f\mapsto h)}$

${\displaystyle {\text{curry}}(f)=h}$

${\displaystyle f=((x,y)\mapsto f(x,y))}$

${\displaystyle f(x,y)={\frac {y}{x}}}$

${\displaystyle g=h_{2}=h(2)=(y\mapsto f(2,y))}$

${\displaystyle g(y)=h_{2}(y)=h(2)(y)=f(2,y)={\frac {y}{2}}}$

${\displaystyle g(3)=h_{2}(3)=h(2)(3)=f(2,3)={\frac {3}{2}}.}$

${\displaystyle f(x,y,z,w)}$

${\displaystyle h_{x}=((y,z,w)\mapsto f(x,y,z,w))}$

${\displaystyle h_{x}(y,z,w)=f(x,y,z,w)}$.

${\displaystyle h=(x\mapsto ((y,z,w)\mapsto f(x,y,z,w)))}$

${\displaystyle x\mapsto (y\mapsto (z\mapsto (w\mapsto f(x,y,z,w))))}$

${\displaystyle x\mapsto y\mapsto z\mapsto w\mapsto f(x,y,z,w)}$

## 定义

${\displaystyle f\colon X\to Y}$ 表示从 ${\displaystyle X}$ 映射到 ${\displaystyle Y}$ 的函数${\displaystyle f}$

${\displaystyle X\to Y}$ 表示从 ${\displaystyle X}$${\displaystyle Y}$ 的所有函数。

${\displaystyle X\times Y}$表示有序对，即笛卡尔乘积。

${\displaystyle {\text{curry}}(f)\colon X\to (Y\to Z)}$

### 函数空间

${\displaystyle {\text{curry}}:{\text{Hom}}(X\times Y,Z)\to {\text{Hom}}(X,{\text{Hom}}(Y,Z)),}$

uncurrying 是反向的映射。如果从 ${\displaystyle X}$${\displaystyle Y}$${\displaystyle Y^{X}}$集合为连续函数 给出了紧致开拓扑紧致开拓扑，而且如果 ${\displaystyle Y}$空间是局部豪斯多夫紧致的，那么 ${\displaystyle {\text{curry}}}$是一个连续函数，也是同胚。尽管可能有更多情况，当 ${\displaystyle X}$${\displaystyle Y}$${\displaystyle Y^{X}}$紧生成的时候，情况都是相同的。

${\displaystyle {\text{curry}}:Z^{X\times Y}\to (Z^{Y})^{X}}$

{\displaystyle {\begin{aligned}&&{\text{eval}}:Y^{X}\times X\to Y\\&&(f,x)\mapsto f(x)\end{aligned}}}

${\displaystyle Y^{X}}$是紧致开放的，而且 ${\displaystyle Y}$局部紧致的豪斯多夫时，那上述式子是连续的。这两个结果对于确立同伦的连续性非常重要，亦即当 ${\displaystyle X}$是单位区间 ${\displaystyle I}$，所以 ${\displaystyle Z^{I\times Y}\cong (Z^{Y})^{I}}$能想成 就是从 ${\displaystyle Y}$${\displaystyle Z}$的两个函数的同伦，或者等价地，是 ${\displaystyle Z^{Y}}$中的单个（连续）路径。

### 逻辑

Curry-Howard下，柯里化和对偶柯里化的存在相当于逻辑定理${\displaystyle (A\land B)\to C\Leftrightarrow A\to (B\to C)}$，因为多元组（型别积, product type）对应于逻辑中的且连接，而函数类型对应于蕴涵

## 历史

“科里化”一词由克里斯托弗·斯特雷奇创造，以逻辑学家哈斯凯尔·加里命名。另外一个名词 "Schönfinkelisation" 则以Moses Schönfinkel命名。在数学历史中，这个原理可以追溯到1893年戈特洛布·弗雷格的工作。