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 la gama de programas a aquellos que probablemente estén finalizando . ^[2]

Restricciones

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

1. Una forma restringida de recursividad , que opera sólo sobre formas "reducidas" de sus argumentos, como la recursividad de Walther , la recursividad subestructural o la "fuertemente normalizante", como lo demuestra la interpretación abstracta del código. ^[3]
2. Cada función debe ser una función total (en lugar de parcial ). Es decir, debe tener una definición para todo lo que esté dentro de su dominio.
   • Hay varias formas posibles de extender funciones parciales comúnmente utilizadas, 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 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 tipos de refinamiento . ^[2] ${\displaystyle \forall x\in \mathbb {N} .x\div 0=0}$

Estas restricciones significan que la programación funcional total no es completa en Turing . Sin embargo, el conjunto de algoritmos que se pueden utilizar sigue siendo enorme. Por ejemplo, cualquier algoritmo para el cual se pueda calcular un límite superior asintótico (mediante un programa que solo usa la recursión de Walther) se puede transformar trivialmente en una función terminante demostrable usando el límite superior como un argumento adicional decrementado en cada iteración o recursión. .

Por ejemplo, no se demuestra trivialmente que la ordenación rápida sea recursiva subestructural, pero solo recurre a una profundidad máxima de la longitud del vector (complejidad temporal en el peor de los casos O ( n ² )). Una implementación de clasificació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 : 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 terminación -- casos qsort estándar 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 , 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 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 "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 como la evaluación perezosa dan como resultado el mismo comportamiento, en principio; sin embargo, uno u otro puede seguir siendo 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 codata. ^[5]

Tanto Epigram como Charity podrían considerarse lenguajes de programación totalmente funcionales, aunque no funcionan de la manera que Turner especifica en su artículo. También podría serlo la programación directa en el Sistema F simple , en la teoría de tipos de Martin-Löf o en el Cálculo de Construcciones .

Ver también

• Análisis de terminación

Referencias

1. 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. vol. 1022, págs. 1-13..
2. 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
3. Turner, DA (28 de abril de 2000), "Garantizar la terminación en ESFP", Journal of Universal Computer Science , 6 (4): 474–488, doi :10.3217/jucs-006-04-0474
4. Las diferencias entre evaluación perezosa y entusiasta se analizan en: Granström, JG (2011). Tratado sobre la teoría de tipos intuicionista. Lógica, epistemología y unidad de la ciencia. vol. 7.ISBN​ 978-94-007-1735-0.Véanse en particular las págs. 86 a 91.
5. 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