Quelles sont les limites de la programmation fonctionnelle totale?

19

Quelles sont les limites de la programmation fonctionnelle totale? Il n'est pas complet de Turing, mais prend toujours en charge un large sous-ensemble des programmes possibles. Y a-t-il des constructions importantes que vous pourriez écrire dans un langage complet de Turing, mais pas dans un langage fonctionnel total?

Et est-il exact de dire que les programmes écrits dans des langages fonctionnels totaux peuvent être complètement analysés statiquement, alors que l'analyse statique dans les langages Turing-complets est limitée par des choses comme le problème d'arrêt? Cela ne veut pas dire que dans les langages fonctionnels totaux, tout peut être déterminé statiquement, car certaines choses ne sont connues qu'au moment de l'exécution, mais je veux dire qu'en théorie, les programmes écrits dans un langage de programmation fonctionnel total idéal peuvent être analysés afin que tout ce qui pourrait en théorie être déterminé statiquement peut être déterminé statiquement. Ou y a-t-il encore des problèmes indécidables hérités dans les langages fonctionnels totaux qui rendent l'analyse statique incomplète? Certains problèmes seront toujours indécidables, quelle que soit la langue dans laquelle ils sont écrits, mais je suis intéressé par les problèmes hérités de la langue,

Matthijs Steen
la source

Réponses:

16

Cela dépend du langage fonctionnel total .

Cette réponse sonne comme une dérobade, mais rien de plus spécifique ne peut être dit. Après tout, considérez le programme décidable important qui vous intéresse. Écrivez un programme dans votre langue préférée de Turing pour le résoudre. Comme le problème est décidable, votre programme s'arrêtera sur toutes les entrées.

(On peut soutenir qu'un problème non décidable pourrait avoir des programmes intéressants, mais pas tels que les gens peuvent les utiliser, car ils ne pourront jamais attendre assez longtemps pour connaître la réponse.)

Maintenant, définissez un nouveau langage tel qu'il n'a qu'un seul programme d'entrée valide: le programme que vous venez d'écrire, avec la même sémantique qu'auparavant. C'est certainement total, car toutes les entrées de tous les programmes qui y sont écrits (dont il n'y en a qu'un) se terminent toujours.

Cette astuce bon marché est en fait utile: le langage Coq , par exemple, est un langage fonctionnel total en ce sens qu'aucun programme ne vérifie le type, sauf s'il existe une preuve qu'il se termine. (Si vous deviez renoncer à cette exigence, ce serait Turing-complete, donc le seul obstacle est de trouver une preuve de résiliation.)

Je ne sais pas ce que vous entendez par «tout ce qui pourrait en théorie être déterminé statiquement peut l'être statiquement»; cela semble tautologiquement vrai. Néanmoins, les langues totales ne sont pas intrinsèquement faciles à analyser; vous savez que rien ne diverge, ce qui est utile, mais la relation entre entrée et sortie est toujours complexe. (En particulier, il existe toujours une infinité d'entrées possibles, vous ne pouvez donc pas toutes les essayer de manière exhaustive, même en théorie.)

Paul Stansifer
la source
Merci pour votre réponse. Donc, être total aide quelque peu, mais cela reste un problème très difficile. Ce que je voulais dire par "tout ce qui pourrait théoriquement être déterminé statiquement peut être déterminé statiquement" était qu'il serait possible, extrêmement difficile ou non, d'analyser toutes les relations entre les entrées et les sorties, si vous aviez suffisamment de ressources pour le faire . Ou sont les raisons fondamentales pour lesquelles cela est limité? Comme la théorie de Rice prouve que c'est le cas pour les fonctions partielles. Ou est-ce que je comprends mal le théorème de Rice?
Matthijs Steen
Je pense que cela peut dépendre de ce que vous entendez par «relation». En particulier, si vous voulez simplement dire que "l'entrée A va à la sortie B", cela est trivialement déterminable dans un langage fonctionnel total; il suffit d'exécuter le programme. Mais vous êtes probablement intéressé par des analyses qui disent quelque chose sur une classe infinie d'entrées.
Paul Stansifer
(oups; appuyez sur Entrée accidentellement) ... mais cela ouvre une autre astuce idiote, car je peux poser des questions indécidables sur la fonction d'identité si je veux: "Pour certains X, est-ce (identity X)qu'une machine de Turing s'arrête?" Bien sûr, cela ne semble pas concerner identity , mais comment définissez-vous «à propos»?
Paul Stansifer
Oui, je veux savoir si cela vaut pour toutes les valeurs d'entrée possibles d'une certaine définition, pas pour les entrées individuelles. Donc, si je vous comprends bien, vous voulez dire qu'il y aura toujours des questions indécidables, quel que soit le type de langage de programmation utilisé? Bien que certaines de ces questions indécidables puissent être contournées en empêchant le problème de se produire en premier lieu, comme les langages fonctionnels totaux pour le problème d'arrêt? Parce que votre question sur la fonction d'identité ne serait pas décidable dans un langage fonctionnel total?
Matthijs Steen
Oui; une version modifiée du problème, dans laquelle "Turing Machine" est remplacé par "tombe en panne après l'expiration de sa garantie Turing Machine" est trivialement résoluble. C'est un peu gênant à ces fins que le problème d'arrêt est l'exemple incontournable d'un problème indécidable lorsque l'examen des programmes est plein d'indécidabilité.
Paul Stansifer
16

Quelles sont les limites de la programmation fonctionnelle totale? Il n'est pas complet de Turing, mais prend toujours en charge un large sous-ensemble des programmes possibles. Y a-t-il des constructions importantes que vous pourriez écrire dans un langage complet de Turing, mais pas dans un langage fonctionnel total?

LLL

  1. LLLLest consistent. C'est exactement ce que le théorème de Goedel exclut, en supposant que vous pouvez faire de l'arithmétique. Nous savons donc que nous ne pouvons pas écrire d'auto-interprètes dans le total des langues fonctionnelles.

  2. Le revers de la médaille, cependant, est que les limites du pouvoir expressif des langues totales sont essentiellement les limites du pouvoir expressif des mathématiques elles-mêmes . Par exemple, les fonctions définissables dans Coq (un assistant de preuve) sont celles qui peuvent être prouvées comme étant calculables en utilisant ZFC, avec un nombre innombrable de cardinaux inaccessibles. Donc, pratiquement n'importe quelle fonction que vous pourriez prouver totale à la satisfaction d'un mathématicien qui travaille est définissable dans Coq.

  3. Le revers de la médaille est que les mathématiques sont difficiles! Il n'y a donc pas de sens facile dans lequel le total des langues est "complètement analysable" - même si vous savez qu'une fonction se termine, vous devrez peut-être encore faire beaucoup de travail créatif pour prouver qu'elle a la propriété que vous voulez. Par exemple, le simple fait de savoir qu'une fonction de listes en listes est totale ne vous permet pas de prouver qu'il s'agit d'une fonction de tri ...

Neel Krishnaswami
la source
Merci pour votre réponse. J'ai lu le post sur ce problème sur le blog de Lambda the Ultimate , mais certaines personnes dans les commentaires déclarent que bien qu'il ne soit pas possible d'avoir son propre évaluateur comme terme régulier explicitement constructible, il serait possible de créer un auto-travail. évaluateur avec quelques astuces. Je me demande donc, y a-t-il des problèmes qui ne peuvent pas être résolus (ou approximés) dans un langage fonctionnel total avec quelques astuces de détours?
Matthijs Steen
Je dirais que l'auto-évaluation ne compte pas comme un problème, car elle varie selon la langue. Le problème "évaluer un programme dans la langue X" est le même problème, que vous essayiez de le résoudre dans la langue X ou Y. En particulier, si la langue X est une langue fonctionnelle totale, le problème peut être résolu dans une langue fonctionnelle totale , en utilisant le même truc idiot que j'ai utilisé auparavant.
Paul Stansifer
Neel, il semble qu'il devrait être beaucoup plus facile que cela de prouver qu'une langue totale ne peut pas prendre en charge son propre interprète. Suis-je mal compris? Par une simple diagonalisation, tout langage avec une fonction sans point fixe ne peut pas supporter son propre interprète (qu'il supporte ou non l'arithmétique). L'argument est développé par Conor McBride ici: mail.haskell.org/pipermail/haskell-cafe/2003-May/004343.html
Tom Ellis
@ TomEllis: Mon argument est essentiellement le même que celui de Conor. En fait, son poste fait déjà cette observation (avec l'esprit caractéristique de Conor) quand il l'appelle «l'argument Épiménide / Cantor / Russell / Quine / Godel / Turing».
Neel Krishnaswami