Halter la théorie des problèmes vs pratique

Question

On affirme souvent que le problème d'arrêt est indécitable.Et prouver qu'il est vraiment trivial.

Mais cela ne s'applique qu'à un programme arbitraire.

Il y a eu une étude sur les classes de programmes humains gagnent habituellement?

Il peut parfois être facile d'analyser un programme et d'énumérer tous ses de ses degrés de liberté et de conclure qu'elle s'arrêtera.

Par exemple, a-t-il déjà été un effort pour créer un langage de programmation (vraiment des scripts) qui garantit l'arrêt?Il ne serait pas largement applicable mais pourrait toujours être utile pour les modules critiques.

Answer 1

Les langues qui sont garanties pour arrêter ont vu une large cuve d'utilisation. Des langues comme Coq / AGDA / IDRIS sont toutes dans cette catégorie. Beaucoup de systèmes de type de type sont en fait assurés de halte tels que le système F ou l'une de ses variantes par exemple. Il est courant que la solidité d'un système de type soit à ébullition pour prouver que tous les programmes se normalisent. Une forte normalisation est une propriété très souhaitable en général dans la recherche sur les langues de programmation.

Je n'ai pas vu beaucoup de succès pour attraper des boucles infinies dans la pratique, cependant "assurer la résiliation dans l'ESFP" de Telford et de Turner affiche un vérificateur de résiliation plus robuste qui a été capable de prouver que l'algorithme d'Euclid a toujours terminé et gère des cas partiels. L'algorithme d'Euclid est un exemple très délicat d'une fonction récursive primitive qui n'est pas simple primitive pour être primitive récursif. Il échoue à des dames qui recherchent simplement un paramètre décroissant (ou un modèle simple de paramètres décroissants tels que le vérificateur de terminaison du fœtus). Pour implémenter cela à l'aide de combinaisons récursif primitifs, vous devez coder une preuve de résiliation pour l'algorithme en tant que paramètre dans la fonction essentiellement.

Je ne peux penser à aucun résultat pour les langages procédurales du sommet de ma tête et la plupart des résultats des langues fonctionnelles utilisent une sorte de restriction qui rend évidemment terminer plutôt que d'essayer d'effectuer une analyse complexe pour garantir davantage Les programmes naturels se terminent.

Answer 2

Il y a des recherches passées et actuelles à ce sujet. Un tel problème s'appelle Analyse de terminaison et un look rapide sur Google (Scholar) fournit plusieurs anciens comme ainsi que de nouvelles publications sur ce sujet:

1. 2005, Analyse de terminaison des programmes fonctionnels supérieurs ;
2. 2006, Analyse de terminaison automatisée pour HASKELL < / a>;
3. 2008, Analyse de terminaison des programmes logiques basés sur la dépendance Graphiques ;
4. 2010, Résumé de la boucle et analyse de terminaison ;
5. 2014, Analyse de terminaison par des programmes de terminaison d'apprentissage ;
6. 2015, Analyse de terminaison avec des graphiques d'appel récursif ;
7. 2019, Analyse de terminaison statique pour les algorithmes distribués par événement < / a>;
8. 2019, mise en œuvre de l'analyse de terminaison sur la programmation quantique ;

y compris les langues existantes avec des mécanismes intégrés pour ceux-ci tels que:

• Mercury ;
• Idris, Coq, AGDA;

Answer 3

Microsoft has developed a practical code checker (whose name escapes me at the moment) which performs halt-testing. It exploits the fact that the code it checks is human-written and not arbitrary, just as you suggest. More importantly, it bypasses the impossibility proof by being allowed to return the answer 'Cannot decide' if it runs into code too difficult to check.

Answer 4

There are only 2 types of infinite programs:

1. Those that repeat their own state after a point (cyclical)
2. Those that grow indefinitely in used memory

Those in 1st type, follow this pattern:

Where there is a pair of distinct indices i and j such that xi = xj, and after which the cycle repeats itself again (thanks to the deterministic nature of programs). In this case the inputs x, contain the whole memory and variables used by the algorithm, plus the current instruction pointer.

Cycle detection algorithms work very well in practice for this type and can prove that a given cyclical program will never finish, usually after a small number of steps, for most random programs.

Proving those in the 2nd type is where the challenge is. One could argue that type 2 can never exist in reality (as all computers have finite memory) but that is not very useful in practice because the memory used may grow very slowly for a regular computer to ever be full. A simple example of that is a binary counter that never stops and never repeats its full state completely.

Answer 5

There is a huge class of functions that are trivially guaranteed to halt: Everything with a finite number of loops, with an upper limit for the number of iterations for each loop determined before the loop is started.

If you have a random program, it can be difficult to prove whether or not it halts. Programs that are written for a purpose are usually much easier.

Answer 6

The smart contracts functions in the Ethereum blockchain are an example of a system that needs the guarantee of halting, not to stall the whole chain.

Every function has a gas cost, and the gas cost translates into real Ethereum coins. A transaction fee must be paid to call the contract. If the gas used in the contract exceed the gas paid with the transaction fee, the computation terminates immediately.