La programación funcional total (también conocida como programación funcional fuerte , [1] en contraste con la programación funcional ordinaria o débil ) es un paradigma de programación que restringe el rango de programas a aquellos que probablemente están terminando . [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 solo use la recursividad de Walther) puede transformarse trivialmente en una función de terminación comprobable utilizando el límite superior como un argumento adicional decrementado en cada iteración o recursión. .
Por ejemplo, no se muestra trivialmente que el ordenamiento rápido sea recursivo subestructural, pero solo recurre a una profundidad máxima de la longitud del vector (complejidad de tiempo en el peor de los casos O ( n 2 )). Una implementación de clasificación rápida en listas (que sería rechazada por un verificador recursivo subestructural) es, usando Haskell :
Algunas clases de algoritmos no tienen un límite superior teórico, pero tienen un límite superior práctico (por ejemplo, algunos algoritmos basados en heurística se pueden programar para "abandonar" después de tantas recursiones, lo que también garantiza la terminación).
Otro resultado de la programación funcional total es que tanto la evaluación estricta como la evaluación perezosa dan como resultado el mismo comportamiento, en principio; sin embargo, uno u otro puede ser preferible (o incluso necesario) por motivos de rendimiento. [4]
En la programación funcional total, se hace una distinción entre datos y codatos: los primeros son finitos , mientras que los segundos son potencialmente infinitos. Estas estructuras de datos potencialmente infinitas se utilizan para aplicaciones como E/S . El uso de codata implica el uso de operaciones como corecursion . Sin embargo, es posible realizar E/S en un lenguaje de programación totalmente funcional (con tipos dependientes ) también sin codatos. [5]