En matemáticas y ciencias de la computación en general, un punto fijo de una función es un valor que se asigna a sí mismo por la función. En lógica combinatoria para informática , un combinador de punto fijo (o combinador de punto fijo ) [1] : la página 26 es una función de orden superior que devuelve algún punto fijo de su función de argumento, si existe.
Formalmente, si la función f tiene uno o más puntos fijos, entonces
y por tanto, por aplicación repetida,
Combinador Y
En el cálculo lambda clásico sin tipo , cada función tiene un punto fijo. Una implementación particular de fix es el combinador paradójico Y de Curry , representado por
En la programación funcional , el combinador Y se puede utilizar para definir formalmente funciones recursivas en un lenguaje de programación que no admite la recursividad.
Este combinador se puede utilizar para implementar la paradoja de Curry . El corazón de la paradoja de Curry es que el cálculo lambda sin tipo no es sólido como sistema deductivo, y el combinador Y lo demuestra al permitir que una expresión anónima represente cero, o incluso muchos valores. Esto es inconsistente en lógica matemática.
Aplicado a una función con una variable, el combinador Y generalmente no termina. Se obtienen resultados más interesantes aplicando el combinador Y a funciones de dos o más variables. La segunda variable se puede utilizar como contador o índice. La función resultante se comporta como un ciclo while o for en un lenguaje imperativo.
Usado de esta manera, el combinador Y implementa una recursividad simple. En el cálculo lambda no es posible hacer referencia a la definición de una función en el cuerpo de una función. La recursividad solo se puede lograr pasando una función como parámetro. El combinador Y demuestra este estilo de programación.
Combinador de punto fijo
El combinador Y es una implementación de un combinador de punto fijo en el cálculo lambda. Los combinadores de punto fijo también se pueden definir fácilmente en otros lenguajes funcionales e imperativos. La implementación en el cálculo lambda es más difícil debido a las limitaciones del cálculo lambda.
El combinador de punto fijo se puede utilizar en varias áreas diferentes,
- Matemáticas generales
- Cálculo lambda sin tipo
- Cálculo lambda tipificado
- Programación funcional
- Programación imperativa
Los combinadores de punto fijo se pueden aplicar a una variedad de funciones diferentes, pero normalmente no terminan a menos que haya un parámetro adicional. Cuando la función que se va a fijar se refiere a su parámetro, se invoca otra llamada a la función, por lo que el cálculo nunca se inicia. En cambio, el parámetro adicional se utiliza para activar el inicio del cálculo.
El tipo de punto fijo es el tipo de retorno de la función que se está fijando. Puede ser real o funcional o de cualquier otro tipo.
En el cálculo lambda sin tipo, la función para aplicar el combinador de punto fijo a puede expresarse usando una codificación, como la codificación de Church . En este caso, los términos lambda particulares (que definen funciones) se consideran valores. "Ejecutar" (reducción beta) del combinador de punto fijo en la codificación da un término lambda para el resultado que luego puede interpretarse como un valor de punto fijo.
Alternativamente, una función puede considerarse como un término lambda definido puramente en el cálculo lambda.
Estos diferentes enfoques afectan la forma en que un matemático y un programador pueden considerar un combinador de punto fijo. Un matemático de cálculo lambda puede ver el combinador Y aplicado a una función como una expresión que satisface la ecuación de punto fijo y, por lo tanto, una solución.
Por el contrario, una persona que solo desee aplicar un combinador de punto fijo a alguna tarea de programación general puede verlo solo como un medio para implementar la recursividad.
Valores y dominios
Cada expresión tiene un valor. Esto es cierto en las matemáticas generales y debe ser cierto en el cálculo lambda. Esto significa que en el cálculo lambda, aplicar un combinador de punto fijo a una función le da una expresión cuyo valor es el punto fijo de la función.
Sin embargo, este es un valor en el dominio de cálculo lambda , puede no corresponder a ningún valor en el dominio de la función, por lo que en un sentido práctico no es necesariamente un punto fijo de la función, y solo en el dominio de cálculo lambda es es un punto fijo de la ecuación.
Por ejemplo, considere
La división de números con signo se puede implementar en la codificación de Church, por lo que f puede representarse mediante un término lambda. Esta ecuación no tiene solución en números reales. Pero en el dominio de los números complejos i y -i hay soluciones. Esto demuestra que puede haber soluciones para una ecuación en otro dominio. Sin embargo, el término lambda para la solución de la ecuación anterior es más extraño que eso. El término lambdarepresenta el estado donde x podría ser yo o -i , como un valor. La información que distingue estos dos valores se ha perdido, en el cambio de dominio.
Para el matemático del cálculo lambda, esto es una consecuencia de la definición del cálculo lambda. Para el programador, significa que la reducción beta del término lambda se repetirá para siempre, sin alcanzar nunca una forma normal.
Función versus implementación
El combinador de coma fija puede definirse en matemáticas y luego implementarse en otros lenguajes. Las matemáticas generales definen una función en función de sus propiedades extensionales . [3] Es decir, dos funciones son iguales si realizan el mismo mapeo. El cálculo lambda y los lenguajes de programación consideran la identidad de función como una propiedad intensional . La identidad de una función se basa en su implementación.
Una función (o término) de cálculo lambda es una implementación de una función matemática. En el cálculo lambda hay una serie de combinador (implementaciones) que satisfacen la definición matemática de un combinador de punto fijo.
¿Qué es un "combinador"?
La lógica combinatoria es una teoría de funciones de orden superior . Un combinador es una expresión lambda cerrada , lo que significa que no tiene variables libres. Los combinadores pueden combinarse para dirigir los valores a sus lugares correctos en la expresión sin siquiera nombrarlos como variables.
Uso en programación
Los combinadores de punto fijo se pueden utilizar para implementar la definición recursiva de funciones. Sin embargo, rara vez se utilizan en la programación práctica. [4] Los sistemas de tipos fuertemente normalizados , como el cálculo lambda de tipo simple, no permiten la no terminación y, por lo tanto, a los combinadores de punto fijo a menudo no se les puede asignar un tipo o requieren características del sistema de tipos complejos. Además, los combinadores de punto fijo a menudo son ineficientes en comparación con otras estrategias para implementar la recursividad, ya que requieren más reducciones de funciones y construyen y desarman una tupla para cada grupo de definiciones recursivas entre sí. [1] : página 232
La función factorial
La función factorial proporciona un buen ejemplo de cómo se puede aplicar el combinador de coma fija. El resultado demuestra una recursividad simple, como se implementaría en un solo bucle en un lenguaje imperativo. La definición de números utilizados se explica en la codificación de la Iglesia . La función que se toma a sí misma como parámetro es,
Esto le da a YF n como,
Configuración da,
Esta definición coloca a F en el papel del cuerpo de un bucle a iterar, y es equivalente a la definición matemática de factorial:
Combinadores de punto fijo en cálculo lambda
El combinador Y , descubierto por Haskell B. Curry , se define como:
La reducción beta de esto da,
(por definición de Y ) | ||
(por β-reducción de λf: aplicado Y ag) | ||
(por β-reducción de λx: función izquierda aplicada a función derecha) | ||
(por segunda igualdad) |
Al aplicar repetidamente esta igualdad obtenemos,
Tenga en cuenta que la igualdad anterior debe considerarse como una secuencia de reducciones β de varios pasos de izquierda a derecha. El término lambda no puede, en general, ser β-reducir al término . Se pueden interpretar los signos de igualdad como equivalencias β en lugar de reducciones β de varios pasos para permitir ir en ambas direcciones.
Definición equivalente de un combinador de punto fijo
Este combinador de punto fijo puede definirse como y en,
Una expresión para y puede derivarse usando reglas de la definición de una expresión let . Primero usando la regla,
da,
También usando,
da
Luego, usando la regla de reducción de eta ,
da,
Derivación del combinador Y
El combinador Y de Curry se puede obtener fácilmente a partir de la definición de y . [5] Comenzando con,
Una abstracción lambda no admite la referencia al nombre de la variable en la expresión aplicada, por lo que x debe pasarse como parámetro ax . Podemos pensar en esto como reemplazar x por xx , pero formalmente esto no es correcto. En lugar de definir y por da,
La expresión let puede considerarse como la definición de la función y , donde z es el parámetro. La instanciación z como y en la llamada da,
Y porque el parámetro z siempre pasa la función y .
Usando la regla de reducción de eta ,
da,
Una expresión let puede expresarse como una abstracción lambda usando,
da,
Esta es posiblemente la implementación más simple de un combinador de punto fijo en el cálculo lambda. Sin embargo, una reducción beta da la forma más simétrica del combinador Y de Curry.
Consulte también traducir entre expresiones let y lambda .
Otros combinadores de punto fijo
En el cálculo lambda sin tipo, los combinadores de punto fijo no son especialmente raros. De hecho, hay infinitos de ellos. [6] En 2005, Mayer Goldberg demostró que el conjunto de combinadores de punto fijo del cálculo lambda no tipificado es recursivamente enumerable . [7]
El combinador Y se puede expresar en el cálculo SKI como
El combinador de punto fijo más simple en el cálculo SK, encontrado por John Tromp , es
aunque tenga en cuenta que no está en forma normal, que es más larga. Este combinador corresponde a la expresión lambda
El siguiente combinador de punto fijo es más simple que el combinador Y, y β-se reduce al combinador Y; a veces se cita como el propio combinador Y:
Otro combinador de punto fijo común es el combinador de punto fijo de Turing (llamado así por su descubridor, Alan Turing ): [8] [2] : 132
Su ventaja sobre es eso beta-se reduce a , [nota 3] mientras que y solo beta-reducir a un término común. [nota 2]
también tiene una forma simple de llamada por valor:
El análogo de la recursividad mutua es un combinador de punto fijo polivariado , [9] [10] [11] que puede denotarse Y *.
Combinador estricto de punto fijo
En un lenguaje de programación estricto, el combinador Y se expandirá hasta que la pila se desborde, o nunca se detendrá en caso de optimización de la llamada final. [12] El combinador Z funcionará en lenguajes estrictos (también llamados lenguajes ansiosos, donde se aplica el orden de evaluación aplicativa). El combinador Z tiene el siguiente argumento definido explícitamente, evitando la expansión de Z g en el lado derecho de la definición: [13]
y en el cálculo lambda es una expansión eta del combinador Y :
Combinadores de punto fijo no estándar
En el cálculo lambda sin tipo, hay términos que tienen el mismo árbol de Böhm que un combinador de punto fijo, es decir, tienen la misma extensión infinita λx.x (x (x ...)). Estos se denominan combinadores de punto fijo no estándar . Cualquier combinador de punto fijo también es uno no estándar, pero no todos los combinadores de punto fijo no estándar son combinadores de punto fijo porque algunos de ellos no satisfacen la ecuación que define los "estándar". Estos extraños combinadores se denominan combinadores de punto fijo estrictamente no estándar ; un ejemplo es el siguiente combinador;
dónde,
El conjunto de combinadores de punto fijo no estándar no se puede enumerar de forma recursiva. [7]
Implementación en otros idiomas
Tenga en cuenta que el combinador Y es una implementación particular de un combinador de punto fijo en el cálculo lambda. Su estructura está determinada por las limitaciones del cálculo lambda. No es necesario ni útil utilizar esta estructura para implementar el combinador de punto fijo en otros idiomas.
A continuación se dan ejemplos simples de combinadores de punto fijo implementados en algunos paradigmas de programación .
Implementación funcional perezosa
En un lenguaje que admite la evaluación perezosa , como en Haskell , es posible definir un combinador de punto fijo utilizando la ecuación definitoria del combinador de punto fijo que se denomina convencionalmente fix
. Dado que Haskell tiene tipos de datos perezosos, este combinador también se puede usar para definir puntos fijos de constructores de datos (y no solo para implementar funciones recursivas). La definición se da aquí, seguida de algunos ejemplos de uso. En Hackage, la muestra original es: [14]
arreglar , arreglar ' :: ( a -> a ) -> a arreglar f = dejar x = f x en x - Lambda eliminado. Intercambio. - Definición original en Data.Function. - alternativa: arreglar ' f = f ( arreglar' f ) - Lambda levantado. No compartir.fix ( \ x -> 9 ) - esto se evalúa como 9fix ( \ x -> 3 : x ) - evalúa a la lista infinita perezosa [3,3,3, ...]fact = fix fac - evalúa a la función factorial donde fac f 0 = 1 fac f x = x * f ( x - 1 )hecho 5 - se evalúa como 120
Implementación funcional estricta
En un lenguaje funcional estricto, el argumento af se expande de antemano, produciendo una secuencia de llamadas infinita,
- .
Esto se puede resolver definiendo el arreglo con un parámetro adicional.
deje que rec fije f x = f ( fije f ) x (* observe la x extra; aquí fije f = \ x-> f (fije f) x *)let factabs fact = function (* factabs tiene un nivel extra de abstracción lambda *) 0 -> 1 | x -> x * hecho ( x - 1 )let _ = ( arreglar factabs ) 5 (* se evalúa como "120" *)
Implementación imperativa del lenguaje
Este ejemplo es una implementación ligeramente interpretativa de un combinador de punto fijo. Se utiliza una clase para contener la función de reparación , denominada fixer . La función a arreglar está contenida en una clase que hereda de fixer. La función arreglar accede a la función que se va a fijar como una función virtual. En cuanto a la definición funcional estricta, fix recibe explícitamente un parámetro adicional x , lo que significa que no se necesita una evaluación diferida.
plantilla < typename R , typename D > class fixer { public : R fix ( D x ) { return f ( x ); } privado : virtual R f ( D ) = 0 ; }; hecho de clase : reparador público < largo , largo > { virtual largo f ( largo x ) { if ( x == 0 ) { return 1 ; } return x * fix ( x -1 ); } }; resultado largo = hecho (). arreglar ( 5 );
En un lenguaje imperativo-funcional, como Lisp , Scheme o Racket , Landin (1963) [ se necesita cita completa ] sugiere el uso de una asignación de variable para crear un combinador de punto fijo:
( definir Y! ( lambda ( f-maker ) (( lambda ( f ) ( set! f ( f-maker ( lambda ( x ) ( f x )))) ;; sentencia de asignación f ) 'NONE )))
Usando un cálculo lambda con axiomas para declaraciones de asignación, se puede demostrar que Y! satisface la misma ley de coma fija que el combinador Y llamada por valor: [15] [16]
Mecanografía
En el cálculo lambda polimórfico ( Sistema F ), un combinador polimórfico de punto fijo tiene tipo [ cita requerida ] ;
- ∀a. (A → a) → a
donde a es una variable de tipo . Es decir, fix toma una función, que asigna a → ay la usa para devolver un valor de tipo a.
En el cálculo lambda simplemente tipado extendido con tipos recursivos , se pueden escribir operadores de punto fijo, pero el tipo de un operador de punto fijo "útil" (uno cuya aplicación siempre regresa) puede estar restringido.
En el cálculo lambda simplemente tipado , al combinador de punto fijo Y no se le puede asignar un tipo [17] porque en algún momento se ocuparía del subtérmino de autoaplicación por la regla de aplicación:
dónde tiene el tipo infinito . De hecho, no se puede escribir ningún combinador de punto fijo; en esos sistemas, cualquier soporte para la recursividad debe agregarse explícitamente al lenguaje.
Escriba para el combinador Y
En los lenguajes de programación que admiten tipos recursivos , es posible escribir el combinador Y contabilizando adecuadamente la recursividad en el nivel de tipo. La necesidad de autoaplicar la variable x puede gestionarse utilizando un tipo (Rec a), que se define de manera que sea isomorfo a (Rec a -> a).
Por ejemplo, en el siguiente código Haskell, tenemos In
y out
siendo los nombres de las dos direcciones del isomorfismo, con tipos: [18] [19]
In :: ( Rec a -> a ) -> Rec a out :: Rec a -> ( Rec a -> a )
que nos permite escribir:
newtype Rec a = In { out :: Rec a -> a }y :: ( a -> a ) -> a y = \ f -> ( \ x -> f ( fuera x x )) ( In ( \ x -> f ( fuera x x )))
O equivalentemente en OCaml:
escriba ' a recc = In of ( ' a recc -> ' a ) let out ( In x ) = xsea y f = ( fun x a -> f ( out x x ) a ) ( In ( fun x a -> f ( out x x ) a ))
Alternativamente:
let y f = ( fun x -> f ( fun z -> out x x z )) ( In ( fun x -> f ( fun z -> out x x z )))
Información general
Debido a que los combinadores de punto fijo se pueden usar para implementar la recursividad, es posible usarlos para describir tipos específicos de cálculos recursivos, como los de iteración de punto fijo , métodos iterativos , unión recursiva en bases de datos relacionales , análisis de flujo de datos , y SEGUIR conjuntos de no terminales en una gramática libre de contexto , cierre transitivo y otros tipos de operaciones de cierre .
Una función para la cual cada entrada es un punto fijo se llama función de identidad . Formalmente:
En contraste con la cuantificación universal sobre todos , un combinador de punto fijo construye un valor que es un punto fijo de. La propiedad notable de un combinador de punto fijo es que construye un punto fijo para una función dada arbitraria.
Otras funciones tienen la propiedad especial de que, una vez aplicadas, las demás aplicaciones no tienen ningún efecto. Más formalmente:
Tales funciones se denominan idempotentes (ver también proyección ). Un ejemplo de tal función es la función que devuelve 0 para todos los enteros pares y 1 para todos los enteros impares.
En el cálculo lambda , desde un punto de vista computacional, la aplicación de un combinador de punto fijo a una función de identidad o una función idempotente normalmente da como resultado un cálculo sin terminación. Por ejemplo, obtenemos
donde el término resultante solo puede reducirse a sí mismo y representa un bucle infinito.
Los combinadores de punto fijo no existen necesariamente en modelos de cálculo más restrictivos. Por ejemplo, no existen en el cálculo lambda simplemente tipado .
El combinador Y permite definir la recursividad como un conjunto de reglas de reescritura , [20] sin requerir soporte de recursividad nativo en el lenguaje. [21]
En los lenguajes de programación que soportan funciones anónimas , los combinadores de punto fijo permiten la definición y uso de funciones recursivas anónimas , es decir, sin tener que vincular dichas funciones a identificadores . En esta configuración, el uso de combinadores de punto fijo a veces se denomina recursividad anónima . [nota 4] [22]
Ver también
- Iteración de punto fijo
- Función anónima
- Cálculo lambda
- Dejemos expresión
- Levantamiento de lambda
Notas
- ^ A lo largo de este artículo,se utilizanlas reglas de sintaxis proporcionadas en el cálculo de Lambda # Notación para guardar paréntesis.
- ^ a b Para un término lambda arbitrario f , la propiedad del punto fijo se puede validar mediante beta reduciendo el lado izquierdo y el derecho: , donde y denotan igualdad sintáctica por definición y reducción beta, respectivamente. De manera similar a los dos primeros pasos, se obtiene . Dado que ambos términos y podrían reducirse al mismo término, son iguales.
- ^
- ^ Esta terminología parece ser en gran parte folklore , pero aparece en lo siguiente:
- Trey Nash, Accelerated C # 2008 , Apress, 2007, ISBN 1-59059-873-3 , pág. 462—463. Derivado sustancialmente del blog de Wes Dyer (ver siguiente artículo).
- Wes Dyer Anonymous Recursion en C # , 02 de febrero de 2007, contiene un ejemplo sustancialmente similar que se encuentra en el libro anterior, pero acompañado de más discusión.
Referencias
- ^ a b Peyton Jones, Simon L. (1987). La implementación de la programación funcional . Prentice Hall International.
- ^ a b Henk Barendregt (1985). El cálculo Lambda: su sintaxis y semántica . Estudios de Lógica y Fundamentos de las Matemáticas. 103 . Amsterdam: Holanda Septentrional. ISBN 0444867481.
- ^ Selinger, Peter. "Notas de la conferencia sobre cálculo Lambda (PDF)" . pag. 6.
- ^ "Para aquellos de nosotros que no sabemos qué es un Y-Combinator o por qué es útil, ..." Hacker News . Consultado el 2 de agosto de 2020 .
- ^ "Álgebra abstracta - ¿Alguien puede explicar el Combinador Y?" . Intercambio de pila de matemáticas .
- ^ Bimbó, Katalin (27 de julio de 2011). Lógica combinatoria: pura, aplicada y mecanografiada . pag. 48. ISBN 9781439800010.
- ↑ a b Goldberg, 2005
- ^ Alan Mathison Turing (diciembre de 1937). "La-función en --conversion ". Journal of Symbolic Logic . 2 (4): 164. JSTOR 2268281 .
- ^ "Muchas caras del combinador de punto fijo" . okmij.org .
- ↑ Polyvariadic Y in pure Haskell98 Archivado el 4 de marzo de 2016 en Wayback Machine , lang.haskell.cafe, 28 de octubre de 2003
- ^ "recursividad - ¿combinador de punto fijo para funciones recursivas entre sí?" . Desbordamiento de pila .
- ^ Bene, Adam (17 de agosto de 2017). "Combinadores de punto fijo en JavaScript" . Bene Studio . Medio . Consultado el 2 de agosto de 2020 .
- ^ "CS 6110 S17 Conferencia 5. Recurrencia y combinadores de punto fijo" (PDF) . Universidad de Cornell . 4.1 Un combinador de punto fijo CBV.
- ^ La definición original en Data.Function .
- ^ Felleisen, Matthias (1987). El cálculo Lambda-v-CS . Universidad de Indiana.
- ^ Talcott, Carolyn (1985). La esencia del ron: una teoría de los aspectos intensional y extensional de la computación tipo Lisp (tesis doctoral). Universidad Stanford.
- ^ Una introducción al cálculo Lambda Archivado el 8 de abril de 2014 en la Wayback Machine.
- ^ Hilo de la lista de correo de Haskell sobre cómo definir el combinador de Y en Haskell , 15 de septiembre de 2006
- ^ Geuvers, Herman; Verkoelen, Joep. Sobre combinadores de punto fijo y bucle en teoría de tipos . CiteSeerX 10.1.1.158.1478 .
- ^ Daniel P. Friedman , Matthias Felleisen (1986). "Capítulo 9 - Lambda The Ultimate". El pequeño Lisper . Asociados de investigación científica . pag. 179. "En el capítulo hemos derivado un combinador Y que nos permite escribir funciones recursivas de un argumento sin usar define".
- ^ Mike Vanier. "El combinador de Y (retorno leve) o: cómo tener éxito en la recursividad sin realmente recurrir" . Archivado desde el original el 22 de agosto de 2011. "De manera más general, Y nos brinda una forma de obtener la recursividad en un lenguaje de programación que admite funciones de primera clase, pero que no tiene la recursividad incorporada".
- ↑ The If Works Deriving the Y combinator , 10 de enero de 2008
- Werner Kluge, Máquinas de computación abstracta: una perspectiva de cálculo lambda , Springer, 2005, ISBN 3-540-21146-2 , págs. 73–77
- Mayer Goldberg, (2005) Sobre la enumerabilidad recursiva de combinadores de punto fijo , Informe BRICS RS-05-1, Universidad de Aarhus
- Matthias Felleisen . Una conferencia sobre el por qué de Y .
enlaces externos
- [1]
- [2]
- Combinador Y
- "Una conferencia sobre el por qué de Y"
- "Un uso del combinador Y en Ruby"
- "Programación funcional en Ada"
- Código Rosetta - Combinador Y