Zurra

Currying (del inglés curry , a veces - curry ) - la transformación de una función de muchos argumentos en un conjunto de funciones, cada una de las cuales es una función de un argumento. La posibilidad de tal transformación se observó por primera vez en los escritos de Gottlob Frege , estudiado sistemáticamente por Moses Scheinfinkel en la década de 1920, y llamado así por Haskell Curry , el desarrollador de la lógica combinatoria , en la que la reducción a funciones de un argumento es fundamental.

Definición

Para una función de dos argumentos , el operador curry realiza una conversión : toma un argumento de tipo y devuelve una función de tipo . Intuitivamente, currar una función le permite corregir algunos de sus argumentos mientras devuelve la función de los argumentos restantes. Por lo tanto, es una función de tipo . $h\dos puntos (A\veces B)\a C$ $\lambda$ ${\ estilo de visualización \ Lambda (h) \ dos puntos A \ a (B \ a C)}$ $A$ ${\ estilo de visualización (B \ a C)}$ $\lambda$ $(A\veces B\a C)\a (A\a (B\a C))$

Decurrying ( eng. uncurring ) se introduce como una transformación inversa, restaurando el argumento curry: para una función, el operador decurringrealiza la transformación; el tipo de operador decurry es. $k\dos puntos A\a (B\a C)$ $\epsilon$ $\epsilon (k)\dos puntos A\veces B\a C$ $(A\a (B\a C))\a (A\veces B\a C)$

En la práctica, curry le permite considerar una función que no recibió todos los argumentos provistos. El operador curry está integrado en algunos lenguajes de programación para permitir que se curryen funciones de varios lugares, siendo los ejemplos más comunes de tales lenguajes ML y Haskell . Todos los idiomas que admiten cierres le permiten escribir funciones curry.

Punto de vista matemático

En ciencias de la computación teórica , currying proporciona una forma de examinar funciones de múltiples argumentos dentro de sistemas teóricos muy simples como el cálculo lambda . En la teoría de conjuntos, curry es una correspondencia entre conjuntos y . En la teoría de categorías, curry proviene de la propiedad universal de la exponencial ; en la situación de una categoría cerrada cartesiana , esto conduce a la siguiente correspondencia. Hay una biyección entre conjuntos de morfismos de un producto binario y morfismos en un exponencial que es natural con respecto a y con respecto a . Esta declaración es equivalente al hecho de que el funtor producto y el funtor Hom son funtores adjuntos. $C^{A\veces B}$ ${\ estilo de visualización \ izquierda (C ^ {B} \ derecha) ^ {A}}$ $f\dos puntos (X\times Y)\to Z$ $g\dos puntos X\a Z^{Y}$ $X$ $Z$

Esta es una propiedad clave de una categoría cerrada cartesiana o, más generalmente, una categoría monoidal cerrada . El primero es bastante suficiente para la lógica clásica, pero el segundo es una base teórica conveniente para la computación cuántica . La diferencia es que el producto cartesiano solo contiene información sobre un par de dos objetos, mientras que el producto tensorial utilizado en la definición de una categoría monoide es adecuado para describir estados entrelazados [1] .

Desde el punto de vista de la correspondencia de Curry-Howard , la existencia de funciones de curry (tipo habitabilidad y de curry (tipo habitabilidad ) equivale a un enunciado lógico ( tipo de producto corresponde a conjunción , y tipo funcional a implicación ). Funciones curry y decurring son continuas según Scott . $((A\veces B)\a C)\a (A\a (B\a C)$ $(A\a (B\a C)\a ((A\veces B)\a C)$ $((A\land B)\Rightarrow C)\Leftrightarrow (A\Rightarrow (B\Rightarrow C))$ $A\veces B$ $De la A, a la B$

Currying desde el punto de vista de la programación

Currying es ampliamente utilizado en lenguajes de programación , principalmente aquellos que soportan el paradigma de programación funcional . En algunos lenguajes, las funciones se procesan de forma predeterminada, es decir, las funciones de varios lugares se implementan como funciones de un solo lugar de órdenes superiores , y la aplicación de argumentos a ellas es una secuencia de aplicaciones parciales .

Los lenguajes de programación con funciones de primera clase generalmente definen operaciones curry(traducir una función de firma de vista A, B -> Cen una función de firma A -> B -> C) y uncurry(realizar la transformación inversa: asignar una función de firma de vista a una función de A -> B -> Cdos lugares del formulario A, B -> C). En estos casos, la conexión con la operación de aplicación parcial es transparente papply: curry papply = curry.

Notas

↑ Juan c. Baez y Mike Stay, " Physics, Topology, Logic and Computation: A Rosetta Stone Archivado el 15 de mayo de 2013 en Wayback Machine ", (2009) ArXiv 0903.0340 Archivado el 20 de julio de 2014 en Wayback Machine en New Structures for Physics , ed. Bob Coecke, Lecture Notes in Physics vol. 813 , Springer, Berlín, 2011, pág. 95-174.

Literatura

Benjamín Pierce. Tipos en lenguajes de programación / Per. del inglés: G. Bronnikov, A. Ott. - Dobrosvet , 2011. - S. 76. - 656 p. — ISBN 978-5-7913-0082-9 .
Teoría de tipos // Homotopía Teoría de tipos: Fundamentos univalentes de las matemáticas . - Princeton : Instituto de Estudios Avanzados , 2013. - 603 p.