Hispanopedia Wiki
Articulo de referencia

Recursión polimórfica

En informática , la recursión polimórfica (también conocida como tipabilidad de Milner - Mycroft o cálculo de Milner - Mycroft ) se refiere a una función recursiva paramétricame...

Hispanopedia WikiContenido en espanolLectura gratuita

En informática , la recursión polimórfica (también conocida como tipabilidad de Milner - Mycroft o cálculo de Milner - Mycroft ) se refiere a una función recursiva paramétricamente polimórfica donde el parámetro de tipo cambia con cada invocación recursiva, en lugar de permanecer constante. La inferencia de tipos para la recursión polimórfica es equivalente a la semiunificación y, por lo tanto, indecidible , y requiere el uso de un semialgoritmo o anotaciones de tipo proporcionadas por el programador . [ 1 ]

Ejemplo

Tipos de datos anidados

Consideremos el siguiente tipo de dato anidado en Haskell :

datos Anidado a = a :<: ( Anidado [ a ]) | Epsilon infixr 5 :<:anidado = 1 :<: [ 2 , 3 , 4 ] :<: [[ 5 , 6 ],[ 7 ],[ 8 , 9 ]] :<: Épsilon

Una función de longitud definida sobre este tipo de datos será recursiva polimórfica, ya que el tipo del argumento cambia de Nested aa Nested [a]en la llamada recursiva:

longitud :: Anidado a -> Longitud entera Epsilon = 0 longitud ( _ :<: xs ) = 1 + longitud xs

Tenga en cuenta que Haskell normalmente infiere la firma de tipo para una función que parece tan simple como esta, pero aquí no se puede omitir sin provocar un error de tipo.

Tipos de mayor rango

Aplicaciones

Análisis del programa

En el análisis de programas basado en tipos, la recursión polimórfica suele ser esencial para lograr una alta precisión en el análisis. Ejemplos notables de sistemas que emplean recursión polimórfica incluyen el análisis de tiempo de enlace de Dussart, Henglein y Mossin [ 2 ] y el sistema de gestión de memoria basado en regiones de Tofte - Talpin [ 3 ] . Dado que estos sistemas asumen que las expresiones ya han sido tipificadas en un sistema de tipos subyacente (que no necesariamente emplea recursión polimórfica), la inferencia puede volver a ser decidible.

Estructuras de datos, detección de errores, soluciones gráficas

Las estructuras de datos de programación funcional suelen utilizar la recursión polimórfica para simplificar las comprobaciones de errores de tipo y resolver problemas con soluciones temporales intermedias que consumen mucha memoria en estructuras de datos más tradicionales, como los árboles. En las dos citas que siguen, Okasaki (pp.  144-146) ofrece un ejemplo de CONS en Haskell donde el sistema de tipos polimórficos detecta automáticamente los errores del programador. [ 4 ] El aspecto recursivo es que la definición de tipo asegura que el constructor más externo tenga un solo elemento, el segundo un par, el tercero un par de pares, etc., de forma recursiva, estableciendo un patrón automático de detección de errores en el tipo de datos. Roberts (p.  171) ofrece un ejemplo relacionado en Java , utilizando una clase para representar un marco de pila. El ejemplo dado es una solución al problema de la Torre de Hanoi donde una pila simula la recursión polimórfica con una estructura de sustitución de pila anidada inicial, temporal y final. [ 5 ]

Véase también

Notas

  1. ↑ Henglein 1993 .
  2. ↑ Dussart, Dirk; Henglein, Fritz ; Mossin, Christian. "Recursión polimórfica y cualificaciones de subtipos: análisis del tiempo de enlace polimórfico en tiempo polinomial". Actas del 2.º Simposio Internacional de Análisis Estático (SAS) . CiteSeerX 10.1.1.646.5884 . 
  3. ↑ Tofte, Mads ; Talpin, Jean-Pierre (1994). "Implementación del cálculo λ por valor tipado mediante una pila de regiones". POPL '94: Actas del 21.º simposio ACM SIGPLAN-SIGACT sobre principios de lenguajes de programación . Nueva York, NY, EE. UU.: ACM. págs. 188-201 . doi : 10.1145/174675.177855 . ISBN  0-89791-636-0.
  4. ↑ Chris Okasaki (1999). Estructuras de datos puramente funcionales . Nueva York: Cambridge. pág. 144. ISBN  978-0521663502.
  5. ↑ Eric Roberts (2006). Pensando recursivamente con Java . Nueva York: Wiley. pág . 171. ISBN  978-0471701460.

Lecturas adicionales

  • Meertens, Lambert (1983). "Verificación de tipos polimórficos incrementales en B" (PDF) . Simposio ACM sobre Principios de Lenguajes de Programación (POPL), Austin, Texas .
  • Mycroft, Alan (1984). «Esquemas de tipos polimórficos y definiciones recursivas». Simposio Internacional sobre Programación, Toulouse, Francia . Lecture Notes in Computer Science. Vol.  167. pp. 217–228 . doi : 10.1007/3-540-12925-1_41 . ISBN  978-3-540-12925-7.
  • Henglein, Fritz (1993). "Inferencia de tipos con recursión polimórfica". ACM Transactions on Programming Languages ​​and Systems . 15 (2): 253– 289. CiteSeerX 10.1.1.42.3091 . doi : 10.1145/169701.169692 . S2CID 17411856 .  
  • Kfoury, AJ ; Tiuryn, J.; Urzyczyn, P. (abril de 1993). "Reconstrucción de tipos en presencia de recursión polimórfica" . ACM Transactions on Programming Languages ​​and Systems . 15 (2): 290–311 . doi : 10.1145/169701.169687 . ISSN 0164-0925 . S2CID 18059949 .  
  • Michael I. Schwartzbach (junio de 1995). "Inferencia de tipo polimórfico" . Informe técnico BRICS-LS-95-3 .
  • Emms, Martin ; Leiß, Hans (1996). "Extending the type checker for SML by polymorphic recursion — A correctness proof" . Technical Report 96-101 .
  • Richard Bird y Lambert Meertens (1998). "Tipos de datos anidados" .
  • C. Vasconcellos, L. Figueiredo, C. Camarao (2003). " Inferencia práctica de tipos para recursión polimórfica: una implementación en Haskell"". Revista de Ciencias de la Computación Universal .
  • L. Figueiredo, C. Camarao. " Inferencia de tipos para definiciones recursivas polimórficas: una especificación en Haskell ".
  • Hallett, J. J; Kfoury, AJ (julio de 2005). "Ejemplos de programación que requieren recursión polimórfica" . Electronic Notes in Theoretical Computer Science . 136 : 57–102 . doi : 10.1016/j.entcs.2005.06.014 . hdl : 2144/1532 . ISSN 1571-0661 . 
  • Aprendizaje automático estándar con recursión polimórfica por Hans Leiß, LMU Múnich
Lecturas relacionadas
6 articulos
Ciencias de la ComputaciónCiencias de la ComputaciónÁreas fundamentales de la informática La informática es el estudio de la computación , la información y la automatización . [1] [2] [3] La informát...Robin MilnerRobin MilnerArthur John Robin Gorell Milner FRS (13 January 1934 – 20 March 2010) was a British computer scientist, and a Turing Award winner.[5][6][7][8][9][10]Icono de trozoAlan MycroftAlan Mycroft es profesor en el Laboratorio de Computación de la Universidad de Cambridge y miembro del Robinson College de Cambridge , donde tambié...Función (programación informática)Función (programación informática)En programación informática , una función (también procedimiento , método , subrutina , rutina o subprograma ) es una unidad invocable [1] de lógic...Recursión (informática)Recursión (informática)En informática , la recursión es un método para resolver un problema computacional en el que la solución depende de soluciones a instancias más peq...{\displaystyle {\mathsf {id}}(x)=x}Polimorfismo paramétricoEn los lenguajes de programación y la teoría de tipos , el polimorfismo paramétrico permite que a una sola pieza de código se le asigne un tipo "ge...