Quelles sont les limites pratiques d'un langage complet non-turing comme Le Coq?

tout d'abord , je suppose que vous avez déjà entendu parler de la Church-Turing thesis , qui stipule que tout ce que nous appelons "calcul" est quelque chose qui peut être fait avec une machine de Turing (ou l'un des nombreux autres modèles équivalents). Ainsi, un langage Turing-complete est un langage dans lequel n'importe quel calcul peut être exprimé. A l'inverse, un langage Turing-incomplet est un langage dans lequel il y a un certain calcul qui ne peut pas être exprimé.

Ok, ce n'était pas très informatif. Permettez-moi de donner un exemple. Il y a une chose que vous ne pouvez pas faire dans n'importe quel Turing-le langage incomplet: vous ne pouvez pas écrire un simulateur de machine de Turing (autrement vous pourriez encoder n'importe quel calcul sur la machine de Turing simulée).

Ok, que encore n'était pas très instructif. la vraie question Est, ce utile programme ne peut pas être écrit dans un Turing-incomplet langue? Personne n'a trouvé de définition de "utile". programme" qui comprend tous les programmes quelqu'un quelque part a écrit pour un but utile, et qui n'inclut pas tous les calculs de machine de Turing. Ainsi, concevoir un langage Turing-incomplet dans lequel vous pouvez écrire tous les programmes utiles est encore un objectif de recherche à très long terme.

il y a maintenant plusieurs types de Turing très différents-des langues incomplètes là-bas, et ils diffèrent dans ce qu'ils ne peuvent pas faire. Cependant, il ya un thème commun. Si vous êtes à la conception d'une langue, il y sont deux principaux moyens d'assurer que la langue sera Turing-complete:

• exiger que la langue est arbitraire des boucles ( while ) et de l'allocation dynamique de la mémoire ( malloc )

• exiger que la langue prend en charge arbitraire des fonctions récursives

regardons quelques exemples de non-Turing langues que certaines personnes pourraient néanmoins appel langages de programmation.

• les premières versions de FORTRAN n'avaient pas d'allocation de mémoire dynamique. Vous avez dû comprendre à l'avance combien de mémoire votre calcul aurait besoin et allouer cela. Malgré cela, FORTRAN était autrefois le langage de programmation le plus utilisé.

  la limite pratique évidente est que vous devez prédire les besoins en mémoire de votre programme avant de l'exécuter. Qui peut être dur, et peut être impossible si la taille des données d'entrée n'est pas limitée à l'avance. À l'époque, la personne qui alimentait les données d'entrée était souvent la personne qui avait écrit le programme, donc ce n'était pas si important. Mais ce n'est pas vrai pour la plupart des programmes écrits aujourd'hui.

• Coq est un langage conçu pour prouver des théorèmes . Maintenant prouver théorèmes et les programmes en cours d'exécution sont très étroitement liés , donc vous pouvez écrire des programmes en Coq comme vous démontrer un théorème. Intuitivement, une preuve du théorème "A implique B" est une fonction qui prend une preuve d'Un théorème comme argument et retourne une preuve du théorème B.

  puisque le but du système est de prouver des théorèmes, vous ne pouvez pas laisser le programmeur écrire des fonctions arbitraires. Imaginez le langage vous a permis d'écrire une fonction récursive stupide qui vient de s'appeler (choisissez la ligne qui utilise votre langue préférée):

  theorem_B boom (theorem_A a) { return boom(a); }
  let rec boom (a : theorem_A) : theorem_B = boom (a)
  def boom(a): boom(a)
  (define (boom a) (boom a))
  

  vous ne pouvez pas laisser l'existence d'une telle fonction vous convaincre que A implique B, ou bien vous seriez en mesure de prouver n'importe quoi et pas seulement de vrais théorèmes! Ainsi, le Coq (et les théorèmes semblables) interdisent la récursion arbitraire. Quand vous écrivez une fonction récursive, vous devez prouver qu'il se termine toujours , de sorte que chaque fois que vous l'exécutez sur une preuve de théorème A vous savez qu'il construira une preuve de théorème B.

  L'immédiat la limitation pratique du Coq est que vous ne pouvez pas écrire des fonctions récursives arbitraires. Puisque le système doit pouvoir rejeter toutes les fonctions non terminantes, l'indécisabilité du problème d'arrêt (ou plus généralement théorème de Rice ) assure qu'il y a des fonctions terminantes qui sont rejetées aussi. Une autre difficulté pratique est que vous devez aider le système à prouver que votre fonction se termine.

  Il ya beaucoup de recherche en cours sur la fabrication de systèmes de preuve plus de programmation-comme le langage-sans compromettre leur garantie que si vous avez une fonction de A à B, il est aussi bon qu'une preuve mathématique que A implique B. étendre le système d'accepter plus de fonctions terminales est l'un des sujets de recherche. Parmi les autres solutions possibles, mentionnons la prise en compte de préoccupations "réelles" comme les intrants/extrants et la concurrence. Un autre défi consiste à rendre ces systèmes accessibles aux simples mortels (ou peut-être convaincre de simples mortels qu'ils sont en fait accessibles).

• Synchrone langages de programmation les langues sont conçus pour la programmation des systèmes temps-réel, c'est-à-dire où le programme doit répondre en moins de n cycles d'horloge. Ils sont principalement utilisés pour les systèmes essentiels tels que les contrôles de véhicules ou de signalisation. Ces langages offrent de solides garanties sur la durée d'un programme prendre et combien de mémoire il peut allouer.

  bien sûr, la contrepartie de telles garanties fortes est que vous ne pouvez pas écrire des programmes dont la consommation de mémoire et le temps d'exécution ne peuvent pas être prédits à l'avance. En particulier, vous ne pouvez pas écrire un programme dont la consommation de mémoire ou le temps d'exécution dépend des données d'entrée.

• il y a beaucoup de langages spécialisés qui n'essaient même pas d'être des langages de programmation et donc peut rester confortablement loin D'être complet: expressions régulières, langages de données, la plupart des langages de balisage,...

Par ailleurs, de Douglas Hofstadter , a écrit plusieurs très intéressants ouvrages de vulgarisation scientifique sur le calcul, en particulier Gödel, Escher, Bach: an Eternal Golden Braid . Je ne me souviens pas s'il parle explicitement des limites de Turing-incompleteness, mais la lecture de ses livres vous aidera certainement à comprendre le matériel plus technique.