Qu'est-ce que la «programmation fonctionnelle totale»?

Question

Wikipedia a ceci à dire:

  

Programmation fonctionnelle totale (également   connu comme fort fonctionnel   programmation, à contraster avec   ordinaire, ou fonctionnel faible   programmation) est un paradigme de programmation   ce qui limite la gamme de programmes   à ceux qui sont prouvés   se terminant.

et

  

Ces restrictions signifient que le total   la programmation fonctionnelle n'est pas   Turing-complet. Cependant, l'ensemble des   algorithmes qui peuvent être utilisés est encore   énorme. Par exemple, tout algorithme qui   a eu une limite supérieure asymptotique   calculé pour cela peut être trivialement   transformé en un   fonction se terminant de manière prouvable en utilisant   la limite supérieure comme argument supplémentaire   qui est décrémenté sur chaque   itération ou récursivité.

Il existe également un article dans The Ultimate Lambda sur un article sur la programmation fonctionnelle totale .

Je ne l'avais pas vu jusqu'à la semaine dernière sur une liste de diffusion.

Existe-t-il d'autres ressources, références ou exemples d'implémentations que vous connaissez?

Answer 1

Si j’ai bien compris, la programmation fonctionnelle totale n’est que cela: Programmation avec fonctions totales. Si je me souviens bien de mes cours de mathématiques, une fonction totale est une fonction définie sur l’ensemble du domaine, une fonction partielle en est une qui comporte des "trous". dans sa définition.

Maintenant, si vous avez une fonction qui, pour une valeur d'entrée v , passe dans une récursion infinie ou une boucle infinie ou si, en général, ne se termine pas d'une autre manière, votre fonction n'est pas défini pour v , et donc partiel, c'est-à-dire non total.

La programmation fonctionnelle totale ne vous permet pas d’écrire une telle fonction. Toutes les fonctions renvoient toujours un résultat pour toutes les entrées possibles; et le vérificateur de type s’assure que tel est le cas.

Je suppose que cela simplifie grandement la gestion des erreurs: il n'y en a pas.

L'inconvénient est déjà mentionné dans votre devis: ce n'est pas Turing-complete. Par exemple. un système d'exploitation est essentiellement une boucle infinie géante. En effet, nous ne voulons pas qu’un système d’exploitation se termine, nous appelons ce comportement un "crash". et crier à nos ordinateurs à ce sujet!

Answer 2

Bien qu'il s'agisse d'une vieille question, je pense qu'aucune des réponses à ce jour ne mentionne la véritable motivation pour la programmation fonctionnelle totale, qui est la suivante:

Si les programmes sont des preuves et que les preuves sont des programmes, les programmes comportant des "trous" n'ont aucun sens comme preuves et introduisent une incohérence logique.

En gros, si une preuve est un programme, une boucle infinie peut être utilisée pour prouver quoi que ce soit . C'est vraiment mauvais et cela explique en grande partie pourquoi nous pourrions vouloir programmer totalement. Les autres réponses tendent à ne pas prendre en compte le revers du papier. Bien que les langues ne soient techniquement pas complètes, vous pouvez récupérer de nombreux programmes intéressants en utilisant des définitions et des fonctions co-inductives. Nous sommes très enclins à penser aux données inductives , mais codata remplit une fonction importante dans ces langages, dans lesquels vous pouvez définir totalement une définition qui est infinie calcul qui se termine, vous utiliserez potentiellement seulement une partie finie de ceci, ou peut-être pas si vous écrivez un système d’exploitation!).

Il est également à noter que la plupart des assistants de preuve travaillent sur ce principe, par exemple Coq.

Answer 3

La charité est un autre langage qui garantit la résiliation:
http://pll.cpsc.ucalgary.ca/charity1/www/home.html

Hume est une langue à 4 niveaux. Le niveau extérieur est complet et la couche la plus interne garantit la terminaison:
   http://www-fp.cs.st-andrews.ac. uk / hume / report /