Programación funcional total

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 tienen una terminación demostrable . ^{[ 2 ]}

La rescisión está garantizada por las siguientes restricciones:

1. Una forma restringida de recursión , que opera solo sobre formas "reducidas" de sus argumentos, como la recursión de Walther , la recursión subestructural o la "normalización fuerte" como se demuestra mediante la interpretación abstracta del código. ^{[ 3 ]}
2. Toda función debe ser una función total (a diferencia de una función parcial ). Es decir, debe tener una definición para todo lo que se encuentra dentro de su dominio.
   • Hay varias formas posibles de extender funciones parciales de uso común, como la división, para que sean totales: elegir un resultado arbitrario para entradas en las que la función normalmente no está definida (como${\displaystyle \forall x\in \mathbb {N} .x\div 0=0}$para la división); agregar otro argumento para especificar el resultado para esas entradas; o excluirlas mediante el uso de características del sistema de tipos, como los tipos de refinamiento . ^{[ 2 ]}

Estas restricciones implican 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 una cota superior asintótica (mediante un programa que solo utilice la recursión de Walther) puede transformarse fácilmente en una función que termina de forma demostrable utilizando la cota superior como un argumento adicional que se decrementa en cada iteración o recursión.

Por ejemplo, no se demuestra trivialmente que quicksort sea recursivo subestructural, sino que solo recurre hasta una profundidad máxima igual a la longitud del vector (complejidad temporal en el peor de los casos ^O ( n² ) ). Una implementación de quicksort en listas (que sería rechazada por un verificador de recursividad subestructural) es, usando Haskell :

import Data.List ( partición )qsort [] = [] qsort [ a ] ​​= [ a ] ​​qsort ( a : as ) = let ( lesser , greater ) = partition ( < a ) as in qsort lesser ++ [ a ] ​​++ qsort greater

Para hacerlo recursivo subestructural usando la longitud del vector como límite, podríamos hacer lo siguiente:

import Data.List ( partición )qsort x = qsortSub x x -- caso mínimo qsortSub [] as = as -- muestra 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. en qsortSub ls lesser ++ [ a ] ​​++ qsortSub ls greater

Algunas clases de algoritmos no tienen un límite superior teórico, pero sí un límite superior práctico (por ejemplo, algunos algoritmos basados ​​en heurísticas pueden programarse para "rendirse" después de un cierto número de 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, una u otra puede ser preferible (o incluso necesaria) por razones de rendimiento. ^{[ 4 ]}

En la programación funcional total, se distingue 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 la entrada/salida ( E/S) . El uso de codatos implica el uso de operaciones como la correcursión . 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 como Turner lo especifica en su artículo. Lo mismo podría decirse de la programación directa en System F , en la teoría de tipos de Martin-Löf o en el Cálculo de Construcciones .

• Análisis de terminación