User:Greeninvisibledreams/加利化

{\displaystyle {\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}}}

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

動機

例子

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

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

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

定義

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

${\displaystyle h\colon X\to (Y\to Z)}$.

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

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

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

集合論

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

函數空間

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

${\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 Q^{P}}$ 呢個冪對象喺Heyting代數嘅範疇入面同相會寫成 ${\displaystyle P\to Q}$呢個實質條件。分配Heyting代數係布林代數，而 ${\displaystyle \neg P\lor Q}$ 就係個冪對象，所以冪對象就係實質條件[15]

外部連結

1. John C. Baez and Mike Stay, "Physics, Topology, Logic and Computation: A Rosetta Stone", (2009) ArXiv 0903.0340 in New Structures for Physics, ed. Bob Coecke, Lecture Notes in Physics vol. 813, Springer, Berlin, 2011, pp. 95-174.
2. Gottlob Frege, Grundgesetze der Arithmetik I, Jena: Verlag Hermann Pohle, 1893, §36.
3. Willard Van Orman Quine, introduction to Moses Schönfinkel's "Bausteine der mathematischen Logik", pp. 355–357, esp. 355. Translated by Stefan Bauer-Mengelberg as "On the building blocks of mathematical logic" in Jean van Heijenoort (1967), A Source Book in Mathematical Logic, 1879–1931. Harvard University Press, pp. 355–66.
4. Strachey, Christopher (2000). "Fundamental Concepts in Programming Languages". Higher-Order and Symbolic Computation. 13: 11–49. doi:10.1023/A:1010000313106. S2CID 14124601. There is a device originated by Schönfinkel, for reducing operators with several operands to the successive application of single operand operators. (Reprinted lecture notes from 1967.)
5. Reynolds, John C. (1972). "Definitional Interpreters for Higher-Order Programming Languages". Proceedings of the ACM Annual Conference. 2 (4): 717–740. doi:10.1145/800194.805852. S2CID 163294. In the last line we have used a trick called Currying (after the logician H. Curry) to solve the problem of introducing a binary operation into a language where all functions must accept a single argument. (The referee comments that although "Currying" is tastier, "Schönfinkeling” might be more accurate.)
6. Kenneth Slonneger and Barry L. Kurtz. Formal Syntax and Semantics of Programming Languages. 1995. p. 144.
7. Henk Barendregt, Erik Barendsen, "Introduction to Lambda Calculus", March 2000, page 8.
8. Curry, Haskell; Feys, Robert (1958). Combinatory logic.第I卷 (第2版). Amsterdam, Netherlands: North-Holland Publishing Company.
9. Graham Hutton. "Frequently Asked Questions for comp.lang.functional: Currying". nott.ac.uk.
10. J.P. May, A Concise Course in Algebraic Topology, (1999) Chicago Lectures in Mathematics ISBN 0-226-51183-9
11. P. I. Booth and J. Tillotson, "Monoidal closed, Cartesian closed and convenient categories of topological spaces", Pacific Journal of Mathematics, 88 (1980) pp.33-53.
12. Joseph J. Rotman, An Introduction to Algebraic Topology (1988) Springer-Verlag ISBN 0-387-96678-1 (See Chapter 11 for proof.)
13. Saunders Mac Lane and Ieke Moerdijk, Sheaves in Geometry and Logic (1992) Springer ISBN 0-387-97710-4 (See Chapter 1, pp.48-57)