La programación funcional total (también conocida como programación funcional fuerte , [1] para contrastarla con la programación funcional ordinaria o débil ) es un paradigma de programación que restringe el rango de programas a aquellos que están demostrablemente terminados . [2]
Restricciones
La terminación está garantizada por las siguientes restricciones:
- Una forma restringida de recursividad , que opera solo sobre formas 'reducidas' de sus argumentos, como la recursividad de Walther , la recursividad subestructural o la "fuerte normalización", como lo demuestra la interpretación abstracta del código. [3]
- Cada función debe ser una función total (en oposición a una función parcial ). Es decir, debe tener una definición para todo lo que está dentro de su dominio.
- Hay varias formas posibles de extender las funciones parciales de uso común, como la división, para que sea total: eligiendo un resultado arbitrario para entradas en las que la función normalmente no está definida (como para la división); agregar otro argumento para especificar el resultado de esas entradas; o excluirlos mediante el uso de características del sistema de tipos , como los tipos de refinamiento . [2]
Estas restricciones significan que la programación funcional total no es Turing-completa . Sin embargo, el conjunto de algoritmos que se pueden utilizar sigue siendo enorme. Por ejemplo, cualquier algoritmo para el que se pueda calcular un límite superior asintótico (mediante un programa que en sí mismo solo usa la recursividad de Walther) se puede transformar trivialmente en una función de terminación demostrable utilizando el límite superior como un argumento adicional decrementado en cada iteración o recursión. .
Por ejemplo, quicksort no se muestra trivialmente ser recursivo subestructural, pero sólo recurre a una profundidad máxima de la longitud del vector (peor caso de tiempo de complejidad O ( n 2 )). Una implementación de ordenación rápida en listas (que sería rechazada por un verificador recursivo subestructural) es, usando Haskell :
importar Data.List ( partición )qsort [] = [] qsort [ a ] = [ a ] qsort ( a : as ) = let ( menor , mayor ) = partición ( < a ) como en qsort menor ++ [ a ] ++ qsort mayor
Para hacerlo subestructural recursivo usando la longitud del vector como límite, podríamos hacer:
importar Data.List ( partición )qsort x = qsortSub x x - caso mínimo qsortSub [] as = as - muestra terminación - casos qsort estándar qsortSub ( l : ls ) [] = [] - no recursivo , así aceptado qsortSub ( l : ls ) [ a ] = [ a ] - no recursivo , así aceptado qsortSub ( l : ls ) ( a : as ) = let ( menor , mayor ) = partición ( < a ) as - recursivo, pero recurrente en ls, que es una subestructura de - su primera entrada. en qsortSub ls menor ++ [ a ] ++ qsortSub ls mayor
Algunas clases de algoritmos no tienen límite superior teórico, pero tienen un límite superior práctico (por ejemplo, algunos algoritmos basados en heurística pueden programarse para "darse por vencidos" después de tantas recursiones, asegurando también la terminación).
Otro resultado de la programación funcional total es que tanto la evaluación estricta y evaluación perezosa resultado en el mismo comportamiento, en principio; sin embargo, una u otra puede ser preferible (o incluso necesaria) por razones de rendimiento. [4]
En la programación funcional total, se hace una distinción entre datos y codatos: el primero es finitario , mientras que el segundo es potencialmente infinito. Tales estructuras de datos potencialmente infinito se utilizan para aplicaciones tales como I / O . El uso de codata implica el uso de operaciones como corecursion . Sin embargo, es posible realizar E / S en un lenguaje de programación funcional total (con tipos dependientes ) también sin codatos. [5]
Tanto Epigram como Charity podrían considerarse lenguajes de programación funcionales totales, aunque no funcionan de la manera que Turner especifica en su artículo. Lo mismo ocurre con la programación directamente en el Sistema F simple , en la teoría de tipos de Martin-Löf o en el Cálculo de Construcciones .
Referencias
- ^ Este término se debe a: Turner, DA (diciembre de 1995). Programación funcional fuerte elemental . Primer Simposio Internacional sobre Lenguajes de Programación Funcionales en Educación. Springer LNCS. 1022 . págs. 1-13..
- ^ a b Turner, DA ( 28 de julio de 2004 ), "Programación funcional total" , Journal of Universal Computer Science , 10 (7): 751–768, doi : 10.3217 / jucs-010-07-0751
- ^ Turner, DA (2000-04-28), "Asegurar la terminación en ESFP" , Journal of Universal Computer Science , 6 (4): 474–488, doi : 10.3217 / jucs-006-04-0474
- ^ Las diferencias entre la evaluación perezosa y ansiosa se discuten en: Granström, JG (2011). Tratado de teoría intuicionista de tipos . Lógica, epistemología y unidad de la ciencia. 7 . ISBN 978-94-007-1735-0. Véanse en particular las págs. 86–91.
- ^ Granström, JG (mayo de 2012), "Un nuevo paradigma para el desarrollo basado en componentes", Journal of Software , 7 (5): 1136–1148, doi : 10.4304 / jsw.7.5.1136-1148[ enlace muerto ] Copia archivada