加利化

喺數學同電腦科學入面，加利化（粵拼：gaa1 lei6 faa3，亦稱加里化；英：currying，加利化咗=curried）就係將一個多輸入值函數變做一串單輸入值函數。譬如，加利化咗一個收三個輸入值嘅函數 $f$就會整到三個函數：

${\begin{aligned}x=f(a,b,c)&{\text{ 就 變：}}\\h=g(a)\\i=h(b)\\x=i(c)\\{\text{或 者 一 列 噉 call:}}\\x=g(a)(b)(c)\end{aligned}}$

抽象啲嚟講，一個函數收兩個輸入值（一個嚟自 $X$ ，一個嚟自 $Y$ ）而出個喺 $Z$ 嘅，呢個函數加利化咗之後，佢就會變第二個函數，而呢個函數會收一個嚟自 $X$ 嘅輸入值而出一個由 $Y$ 射到 $Z$ 嘅函數。加利化𪐀局部應用褦，但係兩個係唔同概念嚟嘅。

加利化理論同應用上嚟講都有用。喺啲函數程式同其他程式語言入面，佢係攞嚟自動噉處理點將啲輸入值遞落去啲函數同例外。喺理論電腦科學，加利化可以攞嚟研究點將啲多輸入值函數化為淨係收單輸入值嘅簡單模型。最一般而概念上緊密嘅應用範疇就係喺啲閉包幺半範疇，嗰度就可以將褦埋證明同程式嘅Curry-Howard對應廣泛噉應用喺好多其他嘅結構，譬如量子力學、cobordisms同埋弦理論（string theory）。加利化係由Gottlob Frege引入嘅，後嚟再俾Moses Schönfinkel發展，跟住又俾哈士𠵇·加利發展。

Uncurrying係加利化嘅對偶變換，係用嚟去函數化嘅一種方法。簡單嚟講就係將一個入一個輸入值、出一個函數 $g$ 嘅函數 $f$ 化成一個入 $f$ 同 $g$ 嘅輸入值 $f'$ ，而 $f'$ 嘅輸出值就等同用完 $f$ 再用 $g$ 而得出嘅輸出值。噉樣嘅過程係可以重複嘅。

動機

加利化提供咗一個途徑嚟到將一個接受幾個輸入值嘅函數應用喺啲淨係收一個輸入值嘅架構度。例如，有啲分析技巧淨係可以喺收一個輸入值嘅先至用到，但係實用嘅函數通常都會收多個一個函數。Frege呢就話揾到單輸入值呢個個案嘅答案就已經夠，因為一個收幾個輸入值嘅函數可以畀人轉換成一串單輸入值函數。呢個轉換呢而家就叫做加利化嘞。全部喺數學分析或者電腦程式編寫「正常」嘅函數冚𠾴唥都係可以加利化嘅。但係，有啲範疇係唔可以加利化到嘅；最廣泛嘅可加利化範疇就係閉包幺半範疇嘞。

有啲程式語言係幾乎無時無刻都會用加利化咗嘅函數嚟達到多個輸入值；顯著嘅例子有ML同Haskell，兩者都淨係會用單輸入值函數。攞一串單輸入值函數嚟代多輸入值函數呢個性質係由λ運算遺傳落嚟嘅。

加利化係𪐀局部應用褦嘅，但係兩者唔係完全一樣嘅。實際嚟講，閉包呢啲編程技巧就可以喺一個可以同個加利化咗嘅函數一齊行嘅環境入面遮住啲輸入值，嚟達到局部應用，嚟做加利化嘅一種。

例子

假設有個收兩個實數（$\mathbb {R}$）同出一個實數嘅函數 $f:\mathbb {R} \times \mathbb {R} \to \mathbb {R}$，定義佢做 $f(x,y)=x+y^{2}$。加利化呢就會將$f$化為一個函數 $h$，$h$ 呢會收一個實數嘅函數 $h$，同埋出一個喺 $\mathbb {R} ^{\mathbb {R} }$ 嘅函數。用符號嚟講就係 $h:\mathbb {R} \to \mathbb {R} ^{\mathbb {R} }$，其中嘅 $\mathbb {R} ^{\mathbb {R} }$ 係所有收一個實數出一個實數嘅函數嘅集合。跟住，再為每個實數 $x$ 定義一個函數 $h_{x}:\mathbb {R} \to \mathbb {R}$ 做 $h_{x}(y)=x+y^{2}$，然之後定義 $h:\mathbb {R} \to \mathbb {R} ^{\mathbb {R} }$ 做$h(x)=h_{x}$。舉個例子，$h(2)$就係由 $y$ 射到 $2+y^{2}$ 嘅函數，即係 $h(2)(y)=h_{2}(y)=2+y^{2}$。整體嚟講，我哋可以睇到

$h(x)(y)=x+y^{2}=f(x,y)$

從而令到原本嘅$f$同埋加利化咗嘅${\displaystyle }$係含有同樣嘅資訊。喺呢個情況，我哋亦都可以寫

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

呢個記法用喺其他嘅多輸入值函數都得。如果 $f$ 係一個收三個輸入值嘅函數 $f(x,y,z)$ 嚟嘅話，噉加利化咗嘅 $h$ 就會符合以下嘅公式：

$f(x,y,z)=h(x)(y)(z)$

歷史

英文「Currying」呢個稱呼係由Christopher Strachey喺1967年起嘅，個稱呼係源於哈士𠵇·加利呢個邏輯學家嘅名。以前都有提倡過要跟Moses Schönfinkel嘅名去叫「Schönfinkelisation」。喺數學呢個範疇入面，「Currying」呢個原則係嚟自Frege喺1893年做嘅嘢。

定義

用以下俗而簡嘅定義呢，就會容易理解加利化㗎喇，之後可以再將個定義套用喺唔同嘅領域入面。首先，喺講定義之前，我哋要定咗一啲記法先。$X\to Y$呢個記法係講緊所有由 $X$ 射到 $Y$ 嘅函數。如果 $f$ 係一個噉嘅函數嚟嘅話，噉我哋就可以記低 $f$。將 $X\times Y$攞嚟做 $X$ 同 $Y$嘅順序對，即係兩者嘅笛卡兒積。喺度呢，$X$ 同 $Y$ 可以係集合、類、或者其他其他款式嘅物件嚟嘅，下面會再探討。

畀一個函數

$f\colon (X\times Y)\to Z$,

加利化 就會整一個新嘅函數

$h\colon X\to (Y\to Z)$.

佢係會收個嚟自 $X$ 嘅數值同出一個由$Y$ 射去 $Z$ 嘅一個函數，係定義做

$h(x)(y)=f(x,y)$

其中嘅$x$ 同 $y$ 分別係嚟自 $X$ 同 $Y$。

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

Uncurrying 就係加利化嘅相反變換，係可以用佢嘅右伴隨函數 $\operatorname {apply} .$嚟容易噉瞭解。

集合論

喺集合論入面， $Y^{X}$ 係攞嚟記低由$X$集合射到$Y$集合嘅函數集合。噉加利化呢，就係由 $B\times C$ 射到 $A$ 嘅函數集合 $A^{B\times C}$ 同埋由 $B$ 射到由$C$射到$A$嘅函數集合嘅函數集合之間嘅自然對射。用符號就係

$A^{B\times C}\cong (A^{C})^{B}$

當然，正正就係呢個自然對射先至合理化咗用次方嘅記法嚟寫函數嘅組合。就好似唔同加利化嘅例子噉，上面嘅公式就形容一對伴隨函子：For每個定咗嘅集合$C$嚟講，$B\mapsto B\times C$函子就係$A\mapsto A^{C}$函子嘅左伴隨函子。

喺集合範疇入面，$Y^{X}$呢個物件係叫做冪對象。

函數空間

函數空間嘅理論有包泛函分析同Homotopy論，主要研究拓撲空間之間嘅連續函數。

集合曬所有由 $X$ 射到 $Y$嘅函數而得出嘅集合呢就可以記做$Hom(X,Y)$同叫做Hom函子。呢度呢，$curry$ 就係以下嘅對射：

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

而去加利化就係相反嘅映射。如果我哋攞緊緻開拓撲畀 $Y^{X}$ 呢個由 $X$ 射到 $Y$ 連續函數嘅集合，而空間 $Y$ 係局部緊緻Hausdorff嘅話，噉

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

就係一個同相寫像（homeomorphism）嚟嘅，話之你$X$、$Y$同$Y^{X}$係咪 緊生成嘅，雖然重有其他case 。

噉樣呢就會衍生咗一個推論出嚟：一個函數係連續若且唯若相應嘅加利化函數係連續。另外，平時喺呢個情況叫開「評價」嘅應用映射就會係連續嘅（注意：嚴緊嚟講，「eval」係一個喺電腦科學入面唔𪐀耕嘅概念嚟嘅）。即係如果$Y^{X}$係緊緻開而$Y$係局部緊緻Hausdorff嘅話，噉

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

就會係連續㗎喇。呢兩個結果對要建立同倫嚟講係中心嘅，即係當 $I$ 係 $X$ 嘅單位間隔，令到 $Z^{I\times Y}\cong (Z^{Y})^{I}$ 可以一係俾人視為兩個由 $Y$ 射到 $Z$ 嘅函數之間嘅同倫，一係俾人視為喺 $Z^{Y}$ 嘅一條道路。

邏輯

根據Curry-Howard對應，加利化同去加利化嘅存在係等同 $(A\land B)\to C\Leftrightarrow A\to (B\to C)$ 呢個邏輯定理，因為多元組（積類型）係對應邏輯入面嘅邏輯與（conjunction），而函數類型係對應意味（implication）。

$Q^{P}$ 呢個冪對象喺Heyting代數嘅範疇入面同相會寫成 $P\to Q$呢個實質條件。分配Heyting代數係布林代數，而 $\neg P\lor Q$ 就係個冪對象，所以冪對象就係實質條件。

同局部函數應用嘅

内文：局部應用

睇埋

• Tensor-hom 伴隨函子
• 惰性求值
• 閉包 (電腦科學)
• smn定理
• 閉包幺半範疇

參考

• Schönfinkel, Moses (1924). "Über die Bausteine der mathematischen Logik". Math. Ann. 92 (3–4): 305–316. doi:10.1007/BF01448013. S2CID 118507515.
• Heim, Irene; Kratzer, Angelika (1998). Semantics in a Generative Grammar. Malden: Blackwall Publishers. ISBN 0-631-19712-5.

出面網頁

• 響砵崙圖案集叢嘅Currying Schonfinkelling
• Currying != Generalized Partial Application! - 喺 Lambda-the-Ultimate.org 嘅貼文