Des langages pratiques non-Turing-complets?

Presque tous les langages de programmation utilisés sont Turing Complete , et bien que cela donne le langage pour représenter tout algorithme calculable , il a également son propre ensemble de problèmes . Voyant que tous les algorithmes que j’écris sont destinés à s’arrêter, je voudrais pouvoir les représenter dans un langage qui leur garantira de s’arrêter.

Les expressions régulières utilisées pour faire correspondre les chaînes et les machines à états finis sont utilisées lors du lexing , mais je me demande s’il existe un langage plus général, plus large, qui n’est pas complet pour Turing?

edit: Je devrais préciser, par “but général” Je ne veux pas nécessairement être capable d’écrire tous les algorithmes d’arrêt dans le langage (je ne pense pas qu’un tel langage existe) mais je soupçonne qu’il y a des points communs dans arrêt de preuves pouvant être généralisées pour produire un langage dans lequel tous les algorithmes sont garantis.

Il y a aussi une autre façon de résoudre ce problème – éliminer la nécessité d’une mémoire théoriquement infinie. Une fois que vous avez limité la quantité de mémoire autorisée par la machine, le nombre d’états de la machine est limité et vous pouvez déterminer si l’algorithme s’arrêtera (en ne permettant pas à la machine de passer à un état antérieur). ).

N’écoutez pas les opposants. Il y a de très bonnes raisons pour lesquelles on pourrait préférer un langage complet non-Turing dans certains contextes, si vous souhaitez garantir la résiliation ou simplifier le code, par exemple en supprimant la possibilité d’erreurs d’exécution. Parfois, ignorer les choses ne suffit peut-être pas.

Le document Total Functional Programming soutient de manière plus ou moins convaincante qu’en fait, nous devrions presque toujours préférer un langage aussi restreint car les garanties du compilateur sont beaucoup plus fortes. Etre capable de prouver qu’un programme s’arrête peut être significatif en soi, mais c’est en réalité le produit du raisonnement beaucoup plus simple que les langages les plus simples permettent. En tant que composante d’une hiérarchie de langues de capacités variables, l’utilité des langues non universelles est très large.

Hume est un autre système qui aborde ce concept de stratification beaucoup plus en profondeur. Le rapport Hume donne une description complète du système et de ses cinq couches de langues progressivement plus complètes et progressivement moins sûres.

Et enfin, n’oubliez pas la charité . C’est un peu abstrait, mais c’est aussi une approche très intéressante d’un langage de programmation utile mais pas universel, qui repose très directement sur les concepts de la théorie des catégories.

BlooP (abréviation de boucle bouclée ) est un langage intéressant, non complet. C’est essentiellement un langage Turing-complet, avec un avertissement (majeur): chaque boucle doit contenir une limite sur le nombre d’itérations. Les boucles infinies ne sont pas autorisées. En conséquence, le problème d’arrêt peut être résolu pour les programmes BlooP.

Le problème n’est pas avec la machine Turing, c’est avec “algorithme”. La raison pour laquelle vous ne pouvez pas prédire si un algorithme s’arrêtera ou non est à cause de cela:

function confusion() { if( halts( confusion ) ) { while True: no-op } else return; } 

Tout langage ne permettant pas la récursivité ou les boucles ne serait pas vraiment “généraliste”.

Les expressions régulières et les machines à états finis sont la même chose! Lexing et correspondance de chaîne sont la même chose! La raison pour laquelle les FSM s’arrêtent est qu’ils ne font jamais de boucle. ils ne font que transmettre le char-by-char et quitter.

MODIFIER:

Pour beaucoup d’algorithmes, il est évident qu’ils s’arrêteront ou non.

par exemple:

 function nonhalting() { while 1: no-op } 

Cette fonction ne s’arrête clairement jamais.

Et, cette fonction interrompt évidemment:

 function simple_halting_function() { return 1; } 

Donc, en fin de compte: vous POUVEZ garantir que votre algorithme s’arrête, il suffit de le concevoir pour qu’il le fasse.

Si vous n’êtes pas sûr si l’algorithme s’arrêterait tout le temps; alors vous ne pouvez probablement pas l’implémenter dans un langage qui garantit “l’arrêt”.

La charité n’est pas Turing complète, cependant, elle n’est pas seulement théoriquement, didactiquement intéressante (théorie des catégories), mais de plus, elle peut résoudre des problèmes pratiques (tours de Hanoi). Sa force est telle qu’elle peut exprimer la fonction même d’ Ackermann .

Il s’avère que c’est assez facile à réaliser. Par exemple, vous n’avez besoin que des 8 instructions ala BrainF ** k , et plus précisément , vous n’avez besoin que d’ une seule instruction .

Le cœur de ces langages est une construction en boucle, et dès que vous avez des boucles illimitées, vous avez un problème d’arrêt inhérent. Quand la boucle se terminera-t-elle? Même dans un langage complet ne prenant pas en charge Turing et supportant des boucles illimitées, vous pourriez toujours avoir le problème en suspens dans la pratique .

Si vous souhaitez que tous vos programmes se terminent, il vous suffit d’écrire votre code avec soin. Une langue spécifique peut être plus adaptée à votre goût et à votre style, mais je ne pense pas qu’aucune langue puisse garantir absolument que le programme résultant s’arrêtera.

“éliminer le besoin de mémoire théoriquement infinie.” — Ben ouais. Tout ordinateur physique est limité par l’entropie de l’univers et, même avant, par la vitesse de la lumière (= = vitesse maximale à laquelle l’information peut se propager).

Encore plus facile, dans un ordinateur réalisable physiquement, il vous suffit de surveiller la consommation de ressources et de la limiter. (c.-à-d. en cas de consommation de mémoire ou de temps> MY_LIMIT, tuez le processus).

Si vous demandez une solution purement mathématique / théorique, comment définissez-vous “objective général”?

La bonne façon de le faire, à mon humble avis, est d’avoir un langage qui est complet à Turing, mais de fournir un système pour indiquer la sémantique pouvant être traitée par un vérificateur de preuves.

Ensuite, en supposant que vous rédigiez délibérément un programme de terminaison, vous avez en tête un bon argument pour expliquer pourquoi il est interrompu et, avec ce nouveau type de langage, vous devriez pouvoir exprimer cet argument et le prouver.

En réserve dans mon compilateur de production, j’ai des récursions que je sais, bien sûr, ne s’arrêteront PAS sur certaines entrées. J’utilise un piratage désagréable pour arrêter ceci: un compteur avec une limite “sensible”. FYI le code actuel est impliqué dans le code polymorphe monomorphisant, et l’expansion infinie se produit lors de l’utilisation de la récursion polymorphe. Haskell attrape ça, mon compilateur pour Felix ne le fait pas (c’est un bogue dans le compilateur que je ne connais pas bien).

À la suite de mon argument général, je voudrais bien savoir quels types d’annotations seraient utiles pour l’object indiqué: j’ai le contrôle d’un langage et d’un compilateur pour pouvoir facilement append un tel support si seulement je savais exactement quoi faire. add 🙂 J’ai vu l’ajout d’une clause “invariant” et “variant” aux boucles à cet effet, bien que je ne pense pas que le langage étendu à l’utilisation de cette information pour la preuve de terminaison (plutôt vérifié l’invariant et la variante à temps d’exécution si je me souviens bien).

Peut-être que cela mérite une autre question ..

Toute langue non-Turing-complete ne serait pas très utile en tant que langage généraliste. Vous pourriez être en mesure de trouver quelque chose qui se présente comme un langage généraliste sans être Turing-complet, mais je n’en ai jamais vu.