En matemáticas y ciencias de la computación , el curry es la técnica de convertir una función que toma múltiples argumentos en una secuencia de funciones que cada una toma un solo argumento. Por ejemplo, currar una función que toma tres argumentos crea tres funciones:
O de forma más abstracta, una función que toma dos argumentos, uno de y uno de y produce salidas en currying se traduce en una función que toma un solo argumento de y produce como funciones de salida de a El curry está relacionado, pero no es lo mismo, con la aplicación parcial .
El curry es útil tanto en entornos prácticos como teóricos. En los lenguajes de programación funcional , y muchos otros, proporciona una forma de administrar automáticamente cómo se pasan los argumentos a las funciones y excepciones. En informática teórica , proporciona una forma de estudiar funciones con múltiples argumentos en modelos teóricos más simples que proporcionan solo un argumento. El escenario más general para la noción estricta de curry y no curry es en las categorías monoidales cerradas , que sustenta una vasta generalización de la correspondencia Curry-Howard de pruebas y programas con una correspondencia con muchas otras estructuras, incluida la mecánica cuántica, los cobordismos y la teoría de cuerdas. . [1] Fue introducido por Gottlob Frege , [2] [3] desarrollado por Moses Schönfinkel , [3] [4] [5] [6] y desarrollado por Haskell Curry . [7] [8]
No curry es la transformación dual en curry, y puede verse como una forma de desfuncionalización . Se necesita una función cuyo valor de retorno es otra función , y produce una nueva función que toma como parámetros los argumentos para ambos y , y devuelve, como resultado, la aplicación de y posteriormente, , a esos argumentos. El proceso se puede iterar.
Motivación
Currying proporciona una forma de trabajar con funciones que toman múltiples argumentos y usarlos en marcos donde las funciones pueden tomar solo un argumento. Por ejemplo, algunas técnicas analíticas solo se pueden aplicar a funciones con un solo argumento. Las funciones prácticas suelen tener más argumentos que este. Frege demostró que era suficiente proporcionar soluciones para el caso de un solo argumento, ya que era posible transformar una función con múltiples argumentos en una cadena de funciones de un solo argumento. Esta transformación es el proceso que ahora se conoce como curado. [9] Todas las funciones "ordinarias" que normalmente se pueden encontrar en el análisis matemático o en la programación de computadoras pueden cursarse. Sin embargo, hay categorías en las que el curry no es posible; las categorías más generales que permiten el curado son las categorías monoidales cerradas .
Algunos lenguajes de programación casi siempre usan funciones curry para lograr múltiples argumentos; ejemplos notables son ML y Haskell , donde en ambos casos todas las funciones tienen exactamente un argumento. Esta propiedad se hereda del cálculo lambda , donde las funciones de múltiples argumentos generalmente se representan en forma de curry.
El curry está relacionado con la aplicación parcial , pero no es lo mismo . En la práctica, la técnica de programación de cierres se puede utilizar para realizar una aplicación parcial y una especie de curry, ocultando argumentos en un entorno que viaja con la función curry.
Ilustración
Supongamos que tenemos una función que toma dos números reales () argumentos y números reales de salida, y se define por . Curry traduce esto en una función que toma un solo argumento real y genera funciones de a . En símbolos,, dónde denota el conjunto de todas las funciones que toman un solo argumento real y producen salidas reales. Por cada número real, define la función por , y luego defina la función por . Entonces, por ejemplo, es la función que envía su argumento real a la salida , o . Vemos que en general
para que la función original y su curry transmitir exactamente la misma información. En esta situación, también escribimos
Esto también funciona para funciones con más de dos argumentos. Si eran una función de tres argumentos , es curry tendría la propiedad
Historia
El nombre "curry", acuñado por Christopher Strachey en 1967 [ cita requerida ] , es una referencia al lógico Haskell Curry . Se ha propuesto el nombre alternativo "Schönfinkelisation" como referencia a Moses Schönfinkel . [10] En el contexto matemático, el principio se remonta a su trabajo en 1893 por Frege .
Definición
El curry se entiende más fácilmente al comenzar con una definición informal, que luego puede moldearse para adaptarse a muchos dominios diferentes. Primero, hay que establecer alguna notación. La notacióndenota todas las funciones de a . Si es tal función, escribimos . Dejardenotar los pares ordenados de los elementos de y respectivamente, es decir, el producto cartesiano de y . Aquí, y pueden ser conjuntos, o pueden ser tipos, o pueden ser otros tipos de objetos, como se explora a continuación.
Dada una función
- ,
currying construye una nueva función
- .
Es decir, toma un argumento de y devuelve una función que mapea a . Está definido por
por de y de . Luego también escribimos
Uncurrying es la transformación inversa, y se entiende más fácilmente en términos de su adjunto derecho, la función
Teoría de conjuntos
En la teoría de conjuntos , la notaciónse utiliza para denotar el conjunto de funciones del conjunto al set . El curry es la biyección natural entre el conjunto de funciones de a , y el set de funciones de al conjunto de funciones de a . En símbolos:
De hecho, es esta biyección natural la que justifica la notación exponencial para el conjunto de funciones. Como es el caso en todos los casos de curry, la fórmula anterior describe un par adjunto de functores : para cada conjunto fijo, el functor se deja adjunto al functor .
En la categoría de conjuntos , el objeto se llama objeto exponencial .
Espacios funcionales
En la teoría de los espacios funcionales , como en el análisis funcional o la teoría de la homotopía , uno está comúnmente interesado en funciones continuas entre espacios topológicos . Uno escribe(el functor Hom ) para el conjunto de todas las funciones de a y usa la notación para denotar el subconjunto de funciones continuas. Aquí,es la biyeccion
mientras que no cursar es el mapa inverso. Si el conjunto de funciones continuas desde a se le da la topología compacta-abierta , y si el espacioes localmente compacto Hausdorff , entonces
es un homeomorfismo . Este también es el caso cuando, y se generan de forma compacta , [11] ( capítulo 5 ) [12] aunque hay más casos. [13] [14]
Un corolario útil es que una función es continua si y solo si su forma al curry es continua. Otro resultado importante es que el mapa de la aplicación , generalmente llamado "evaluación" en este contexto, es continuo (tenga en cuenta que eval es un concepto estrictamente diferente en informática). Es decir,
es continuo cuando es compacto-abierto y Hausdorff localmente compacto. [15] Estos dos resultados son fundamentales para establecer la continuidad de la homotopía , es decir, cuando es el intervalo unitario , así que eso ¿Puede el pensamiento como una homotopía de dos funciones de a , o, de manera equivalente, una única ruta (continua) en .
Topología algebraica
En topología algebraica , el currying sirve como un ejemplo de la dualidad Eckmann-Hilton y, como tal, juega un papel importante en una variedad de entornos diferentes. Por ejemplo, el espacio del bucle es adyacente a las suspensiones reducidas ; esto se escribe comúnmente como
dónde es el conjunto de clases de homotopía de mapas, y es la suspensión de A , yes el espacio de bucle de A . En esencia, la suspensión puede verse como el producto cartesiano de con la unidad de intervalo, módulo una relación de equivalencia para convertir el intervalo en un bucle. La forma al curry luego mapea el espacio al espacio de funciones desde bucles en , es decir, de dentro . [15] Entonceses el functor adjunto que asigna suspensiones a espacios de bucle, y no curry es el dual. [15]
La dualidad entre el cono cartográfico y la fibra cartográfica ( cofibración y fibración ) [11] ( capítulos 6 y 7 ) puede entenderse como una forma de currización, que a su vez conduce a la dualidad de las secuencias Puppe largas exactas y coexactivas .
En álgebra homológica , la relación entre curry y no curry se conoce como adjunción tensor-hom . Aquí, surge un giro interesante: el functor Hom y el functor producto tensorial podrían no elevarse a una secuencia exacta ; esto conduce a la definición del functor Ext y del functor Tor .
Teoría del dominio
En la teoría del orden , es decir, la teoría de celosías de conjuntos parcialmente ordenados ,es una función continua cuando a la red se le da la topología de Scott . [16] Las funciones continuas de Scott se investigaron por primera vez en el intento de proporcionar una semántica para el cálculo lambda (ya que la teoría de conjuntos ordinaria es inadecuada para hacer esto). De manera más general, las funciones continuas de Scott ahora se estudian en la teoría de dominios , que abarca el estudio de la semántica denotacional de los algoritmos informáticos. Tenga en cuenta que la topología de Scott es bastante diferente a muchas topologías comunes que se pueden encontrar en la categoría de espacios topológicos ; la topología de Scott es típicamente más fina y no es sobria .
La noción de continuidad hace su aparición en la teoría de tipos de homotopía , donde, hablando a grandes rasgos, dos programas de ordenador pueden considerarse homotópicos, es decir, calculan los mismos resultados, si se pueden refactorizar "continuamente" de uno a otro.
Cálculos lambda
En informática teórica , el currying proporciona una forma de estudiar funciones con múltiples argumentos en modelos teóricos muy simples, como el cálculo lambda , en el que las funciones solo toman un único argumento. Considere una función tomando dos argumentos y teniendo el tipo , lo que debe entenderse en el sentido de que x debe tener el tipo, y debe tener el tipo, y la función en sí devuelve el tipo . La forma al curry de f se define como
dónde es el abstractor del cálculo lambda. Dado que el curry toma, como entrada, funciones con el tipo, se concluye que el tipo de curry en sí es
El operador → a menudo se considera asociativo a la derecha , por lo que el tipo de función curry a menudo se escribe como . Por el contrario, la aplicación de funciones se considera asociativa por la izquierda , de modo que es equivalente a
- .
Es decir, los paréntesis no son necesarios para eliminar la ambigüedad del orden de la aplicación.
Las funciones curry se pueden utilizar en cualquier lenguaje de programación que admita cierres ; sin embargo, las funciones no actualizadas generalmente se prefieren por razones de eficiencia, ya que la sobrecarga de la aplicación parcial y la creación de cierres se pueden evitar para la mayoría de las llamadas a funciones.
Teoría de tipos
En la teoría de tipos , la idea general de un sistema de tipos en informática se formaliza en un álgebra de tipos específica. Por ejemplo, al escribir, la intención es que y son tipos , mientras que la flechaes un constructor de tipos , específicamente, el tipo de función o tipo de flecha. De manera similar, el producto cartesianode tipos es construido por el constructor de tipo de producto.
El enfoque teórico de tipos se expresa en lenguajes de programación como ML y los lenguajes derivados e inspirados en él: CaML , Haskell y F # .
El enfoque teórico de tipos proporciona un complemento natural al lenguaje de la teoría de categorías , como se analiza a continuación. Esto se debe a que las categorías, y específicamente las categorías monoidales , tienen un lenguaje interno , siendo el cálculo lambda de tipo simple el ejemplo más destacado de dicho lenguaje. Es importante en este contexto, porque se puede construir a partir de un constructor de tipo único, el tipo de flecha. El curry dota a la lengua de un tipo de producto natural. La correspondencia entre objetos en categorías y tipos permite que los lenguajes de programación sean reinterpretados como lógicas (a través de la correspondencia Curry-Howard ) y como otros tipos de sistemas matemáticos, como se explora más adelante.
Lógica
Según la correspondencia Curry-Howard , la existencia de curry y no curry es equivalente al teorema lógico, como tuplas ( tipo de producto ) corresponde a la conjunción en lógica, y el tipo de función corresponde a la implicación.
El objeto exponencial en la categoría de álgebras de Heyting se escribe normalmente como implicación material . Las álgebras distributivas de Heyting son álgebras booleanas , y el objeto exponencial tiene la forma explícita, dejando claro así que el objeto exponencial es realmente una implicación material . [17]
Teoría de categorías
Las nociones anteriores de curry y no curry encuentran su declaración más general y abstracta en la teoría de categorías . El curry es una propiedad universal de un objeto exponencial y da lugar a una adjunción en categorías cerradas cartesianas . Es decir, existe un isomorfismo natural entre los morfismos de un producto binario y los morfismos a un objeto exponencial .
Esto se generaliza a un resultado más amplio en categorías monoidales cerradas : Currying es la afirmación de que el producto tensorial y el Hom interno son functores adjuntos ; es decir, para cada objetohay un isomorfismo natural :
Aquí, Hom denota el Hom-functor (externo) de todos los morfismos en la categoría, mientras quedenota el functor hom interno en la categoría monoidal cerrada. Para la categoría de conjuntos , los dos son iguales. Cuando el producto es el producto cartesiano, entonces el hogar interno se convierte en el objeto exponencial .
El curry puede descomponerse de dos maneras. Una es si una categoría no está cerrada y, por lo tanto, carece de un funtor hom interno (posiblemente porque hay más de una opción para dicho funtor). Otra forma es si no es monoidal y, por lo tanto, carece de producto (es decir, carece de una forma de escribir pares de objetos). Las categorías que tienen productos y homs internos son exactamente las categorías monoidales cerradas.
El establecimiento de categorías cerradas cartesianas es suficiente para la discusión de la lógica clásica ; la configuración más general de categorías monoidales cerradas es adecuada para la computación cuántica . [18]
La diferencia entre estos dos es que el producto de las categorías cartesianas (como la categoría de conjuntos , órdenes parciales completos o álgebras de Heyting ) es simplemente el producto cartesiano ; se interpreta como un par ordenado de elementos (o una lista). El cálculo lambda simplemente mecanografiado es el lenguaje interno de las categorías cerradas cartesianas; y es por esta razón que los pares y las listas son los tipos principales en la teoría de tipos de LISP , esquemas y muchos lenguajes de programación funcional .
Por el contrario, el producto de las categorías monoidales (como el espacio de Hilbert y los espacios vectoriales del análisis funcional ) es el producto tensorial . El lenguaje interno de tales categorías es la lógica lineal , una forma de lógica cuántica ; el sistema de tipo correspondiente es el sistema de tipo lineal . Tales categorías son adecuadas para describir estados cuánticos entrelazados y, de manera más general, permiten una amplia generalización de la correspondencia Curry-Howard con la mecánica cuántica , los coordismos en la topología algebraica y la teoría de cuerdas . [1] El sistema de tipo lineal y la lógica lineal son útiles para describir las primitivas de sincronización , como las cerraduras de exclusión mutua y el funcionamiento de las máquinas expendedoras.
Contraste con la aplicación de función parcial
El currying y la aplicación de funciones parciales a menudo se combinan. [19] Una de las diferencias significativas entre los dos es que una llamada a una función aplicada parcialmente devuelve el resultado de inmediato, no otra función en la cadena de curado; esta distinción se puede ilustrar claramente para funciones cuya aridad es mayor que dos. [20]
Dada una función de tipo , curry produce . Es decir, mientras que una evaluación de la primera función podría representarse como, la evaluación de la función de curry se representaría como , aplicando cada argumento a su vez a una función de un solo argumento devuelta por la invocación anterior. Tenga en cuenta que después de llamar, nos queda una función que toma un solo argumento y devuelve otra función, no una función que toma dos argumentos.
Por el contrario, la aplicación de función parcial se refiere al proceso de fijar una serie de argumentos a una función, produciendo otra función de menor aridad. Dada la definición de arriba, podríamos arreglar (o 'enlazar') el primer argumento, produciendo una función de tipo . La evaluación de esta función podría representarse como. Tenga en cuenta que el resultado de la aplicación de una función parcial en este caso es una función que toma dos argumentos.
Intuitivamente, la aplicación de función parcial dice "si arreglas el primer argumento de la función, obtienes una función de los argumentos restantes". Por ejemplo, si la función div representa la operación de división x / y , entonces div con el parámetro x fijo en 1 (es decir, div 1) es otra función: la misma que la función inv que devuelve el inverso multiplicativo de su argumento, definido por inv ( y ) = 1 / y .
La motivación práctica para la aplicación parcial es que muy a menudo las funciones obtenidas al proporcionar algunos, pero no todos los argumentos a una función, son útiles; por ejemplo, muchos idiomas tienen una función u operador similar a plus_one
. La aplicación parcial facilita la definición de estas funciones, por ejemplo, creando una función que representa el operador de suma con 1 límite como primer argumento.
La aplicación parcial puede verse como la evaluación de una función de curry en un punto fijo, por ejemplo, dado y luego o simplemente dónde primer parámetro de curries f.
Por tanto, la aplicación parcial se reduce a una función de curry en un punto fijo. Además, una función de curry en un punto fijo es (trivialmente), una aplicación parcial. Para mayor evidencia, tenga en cuenta que, dada cualquier función, Una función puede definirse de tal manera que . Por tanto, cualquier aplicación parcial puede reducirse a una sola operación de curry. Como tal, el curry se define más adecuadamente como una operación que, en muchos casos teóricos, a menudo se aplica de forma recursiva, pero que teóricamente es indistinguible (cuando se considera una operación) de una aplicación parcial.
Entonces, una aplicación parcial se puede definir como el resultado objetivo de una sola aplicación del operador curry en algún orden de las entradas de alguna función.
Ver también
- Adjunción tensor-hom
- Evaluación perezosa
- Cierre (informática)
- teorema de s mn
- Categoría monoidal cerrada
Notas
- ^ a b John C. Baez y Mike Stay, " Física, topología, lógica y computación: una piedra de Rosetta ", (2009) ArXiv 0903.0340 en New Structures for Physics , ed. Bob Coecke, Lecture Notes in Physics vol. 813 , Springer, Berlín, 2011, págs. 95-174.
- ^ Gottlob Frege , Grundgesetze der Arithmetik I, Jena: Verlag Hermann Pohle, 1893, §36.
- ↑ a b Willard Van Orman Quine , introducción a "Bausteine der mathischen Logik" de Moses Schönfinkel , págs. 355–357, esp. 355. Traducido por Stefan Bauer-Mengelberg como "Sobre los componentes básicos de la lógica matemática" en Jean van Heijenoort (1967), A Source Book in Mathematical Logic, 1879-1931 . Harvard University Press, págs. 355–66.
- ^ Strachey, Christopher (2000). "Conceptos fundamentales en lenguajes de programación". Computación simbólica y de orden superior . 13 : 11–49. doi : 10.1023 / A: 1010000313106 . S2CID 14124601 .
Existe un dispositivo originado por Schönfinkel, para reducir operadores con varios operandos a la aplicación sucesiva de operadores de un solo operando.
(Notas de conferencias reimpresas de 1967.) - ^ Reynolds, John C. (1972). "Intérpretes de definiciones para lenguajes de programación de orden superior" . Actas de la Conferencia Anual de ACM . 2 (4): 717–740. doi : 10.1145 / 800194.805852 . S2CID 163294 .
En la última línea hemos utilizado un truco llamado Currying (en honor al lógico H. Curry) para resolver el problema de introducir una operación binaria en un lenguaje donde todas las funciones deben aceptar un solo argumento. (El árbitro comenta que aunque "Currying" es más sabroso, "Schönfinkeling" podría ser más exacto).
- ^ Kenneth Slonneger y Barry L. Kurtz. Sintaxis formal y semántica de lenguajes de programación . 1995. p. 144.
- ^ Henk Barendregt, Erik Barendsen, " Introducción al cálculo Lambda ", marzo de 2000, página 8.
- ^ Curry, Haskell; Feys, Robert (1958). Lógica combinatoria . I (2 ed.). Amsterdam, Países Bajos: North-Holland Publishing Company.
- ^ Graham Hutton. "Preguntas frecuentes sobre comp.lang.functional: currying" . nott.ac.uk .
- ^ I. Heim y A. Kratzer (1998). Semántica en gramática generativa . Blackwell.
- ^ a b J.P. May, Un curso conciso en topología algebraica , (1999) Conferencias de matemáticas en Chicago ISBN 0-226-51183-9
- ^ Espacio topológico generado de forma compacta en nLab
- ^ PI Booth y J. Tillotson, " Categorías convenientes y cerradas monoidal, cerradas cartesianas de espacios topológicos ", Pacific Journal of Mathematics , 88 (1980) pp.33-53.
- ^ Categoría conveniente de espacios topológicos en nLab
- ^ a b c Joseph J. Rotman, Introducción a la topología algebraica (1988) Springer-Verlag ISBN 0-387-96678-1 (consulte el Capítulo 11 para obtener una prueba).
- ^ Barendregt, HP (1984). El cálculo Lambda . Holanda Septentrional. ISBN 978-0-444-87508-2. (Ver teoremas 1.2.13, 1.2.14)
- ^ Saunders Mac Lane e Ieke Moerdijk, Gavillas en geometría y lógica (1992) Springer ISBN 0-387-97710-4 ( consulte el capítulo 1, páginas 48-57 )
- ^ Samson Abramsky y Bob Coecke, " Una semántica categórica para protocolos cuánticos ".
- ^ "El blog sin tallar: la aplicación de función parcial no se está currando" . uncarved.com . Archivado desde el original el 23 de octubre de 2016.
- ^ "Programación funcional en 5 minutos" . Diapositivas .
Referencias
- Schönfinkel, Moisés (1924). "Über die Bausteine der mathischen Logik". Matemáticas. Ana. 92 (3–4): 305–316. doi : 10.1007 / BF01448013 . S2CID 118507515 .
- Heim, Irene; Kratzer, Angelika (1998). Semántica en una gramática generativa . Malden: Editores de Blackwall. ISBN 0-631-19712-5.
enlaces externos
- Currying Schonfinkelling en el repositorio de patrones de Portland
- Currying! = Aplicación parcial generalizada! - publicar en Lambda-the-Ultimate.org