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 son demostrablemente terminantes . [2]
La terminación está garantizada por las siguientes restricciones:
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 utilice la recursión de Walther) se puede transformar de manera trivial en una función demostrablemente terminante utilizando el límite superior como un argumento adicional que se decrementa en cada iteración o recursión.
Por ejemplo, no se demuestra de manera trivial que quicksort sea recursivo subestructural, pero solo recurre hasta una profundidad máxima de la longitud del vector (complejidad temporal en el peor de los casos O ( n 2 )). Una implementación de quicksort en listas (que sería rechazada por un verificador recursivo subestructural) es, utilizando Haskell :
importar Data.List ( partición ) qsort [] = [] qsort [ a ] = [ a ] qsort ( a : como ) = let ( menor , mayor ) = partición ( < a ) como en qsort menor ++ [ a ] ++ qsort mayor Para hacerlo recursivo subestructural 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 la terminación -- casos estándar de qsort qsortSub ( l : ls ) [] = [] -- no recursivo, por lo que se acepta qsortSub ( l : ls ) [ a ] = [ a ] -- no recursivo, por lo que se acepta qsortSub ( l : ls ) ( a : as ) = let ( lesser , greater ) = partition ( < a ) as -- recursivo, pero recurre en ls, que es una subestructura de -- su primera entrada. in qsortSub ls lesser ++ [ a ] ++ qsortSub ls greater Algunas clases de algoritmos no tienen un límite superior teórico, pero sí tienen un límite superior práctico (por ejemplo, algunos algoritmos basados en heurísticas pueden programarse para "darse por vencidos" después de ciertas recursiones, lo que también garantiza la terminación).
Otro resultado de la programación funcional total es que, en principio, tanto la evaluación estricta como la evaluación perezosa dan como resultado el mismo comportamiento; 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 : 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 codatos implica el uso de operaciones como la 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 totalmente funcionales, aunque no funcionen de la forma que Turner especifica en su artículo. Lo mismo podría decirse de la programación directa en el Sistema F , en la teoría de tipos de Martin-Löf o en el Cálculo de Construcciones .