Est-il possible de résoudre le problème d'arrêt si vous avez une entrée contrainte ou prévisible?

Le problème de l'arrêt ne peut être résolu dans le cas général. Il est possible de trouver des règles définies qui restreignent les entrées autorisées et le problème d'arrêt peut-il être résolu pour ce cas particulier?

Par exemple, il semble probable qu'un langage qui n'autorise pas les boucles, par exemple, serait très facile de dire si le programme s'arrêterait ou non.

Le problème que j'essaie de résoudre en ce moment est que j'essaie de créer un vérificateur de script qui vérifie la validité du programme. Le problème d'arrêt peut-il être résolu si je sais exactement à quoi m'attendre des scénaristes, ce qui signifie des entrées très prévisibles. Si cela ne peut pas être résolu exactement, quelles sont les bonnes techniques d'approximation pour résoudre ce problème?

La réponse intuitive est que si vous n'avez pas de boucles illimitées et que vous n'avez pas de récursivité et que vous n'avez pas goto, vos programmes s'arrêtent. Ce n'est pas tout à fait vrai, il existe d'autres façons de dissimuler la non-terminaison, mais c'est assez bon pour la plupart des cas pratiques. Bien sûr, l'inverse est faux, il existe des langages avec ces constructions qui n'autorisent pas les programmes sans terminaison, mais ils utilisent d'autres types de restrictions telles que les systèmes de type sophistiqués.

Récursivité

Une restriction courante dans les langages de script est d'empêcher dynamiquement la récursivité: si A appelle B appelle C appelle ... appelle A, alors l'interpréteur (ou le vérificateur, dans votre cas) abandonne ou signale une erreur, même si la récursivité peut effectivement se terminer. Deux exemples concrets:

• Le préprocesseur C laisse une macro intacte lors de son expansion. L'utilisation la plus courante consiste à définir un wrapper autour d'une fonction:

  #define f(x) (printf("calling f(%d)\n", (x)), f(x))
  f(3);
  

  Cela s'étend à

  (printf("calling f(%d)\n", (3)), f(3))
  

  La récursion mutuelle est également gérée. Une conséquence est que le préprocesseur C se termine toujours, bien qu'il soit possible de créer des macros avec une complexité d'exécution élevée.

  #define f0(x) x(x)x(x)
  #define f1(x) f0(f0(x))
  #define f2(x) f1(f1(x))
  #define f3(x) f2(f2(x))
  f3(x)
  

• Les shells Unix développent les alias de manière récursive, mais uniquement jusqu'à ce qu'ils rencontrent un alias déjà développé. Encore une fois, l'objectif principal est de définir un alias pour une commande portant le même nom.

  alias ls='ls --color'
  alias ll='ls -l'
  

Une généralisation évidente est de permettre une profondeur de récursivité allant jusqu'à , pouvant être configurable.$n$$n$

Il existe des techniques plus générales pour prouver que les appels récursifs se terminent, comme la recherche d'un entier positif qui diminue toujours d'un appel récursif au suivant, mais ceux-ci sont considérablement plus difficiles à détecter. Ils sont souvent difficiles à vérifier, et encore moins à déduire.

Boucles

Les boucles se terminent si vous pouvez limiter le nombre d'itérations. Le critère le plus courant est que si vous avez une forboucle (sans astuces, c'est-à-dire qui compte vraiment de à ), elle effectue un nombre fini d'itérations. Donc, si le corps de la boucle se termine, la boucle elle-même se termine.$m$$n$

En particulier, avec les boucles for (plus les constructions de langage raisonnables telles que les conditionnelles), vous pouvez écrire toutes les fonctions récursives primitives , et vice versa. Vous pouvez reconnaître syntaxiquement les fonctions récursives primitives (si elles sont écrites de manière non obscurcie), car elles n'utilisent pas de boucle while ou goto ou récursivité ou autre astuce. Les fonctions récursives primitives sont assurées de se terminer, et la plupart des tâches pratiques ne vont pas au-delà de la récursivité primitive.

Voir Terminator et AProVe . Ils ont tendance à s'appuyer sur l'heuristique, et je ne sais pas s'ils décrivent clairement la classe de programmes pour lesquels ils travaillent. Pourtant, ils sont considérés comme à la pointe de la technologie, ils devraient donc être de bons points de départ pour vous.

Oui, c'est possible. Une manière courante de résoudre de tels problèmes consiste à considérer un paramètre non calculable supplémentaire (monotone) dépendant du code comme partie de l'entrée. La complexité du problème ayant ce paramètre peut être considérablement réduite.

Nous ne pouvons pas calculer le paramètre, mais si vous savez que les instances d'entrée avec lesquelles vous traitez ont de petites valeurs de paramètre, vous pouvez le fixer à un petit nombre et utiliser l'algorithme.

Cette astuce et des astuces similaires sont utilisées dans les méthodes formelles pour faire face à l'indécidabilité de l'arrêt et à des problèmes similaires. Mais si ce que vous voulez décider est compliqué, la complexité de vos algorithmes ne sera probablement pas meilleure que l'exécution de l'algorithme sur ces instances.

En ce qui concerne l'autre question, si vous limitez suffisamment les entrées, le problème d'arrêt peut être facile. Par exemple, si vous savez que les entrées sont des algorithmes temporels polynomiaux, décider du problème d'arrêt pour eux est trivial (puisque chaque algorithme temporel polynomial s'arrête).

Les problèmes qui surviennent dans les méthodes formelles sont généralement indécidables, vous voudrez peut-être vérifier la littérature sur la façon dont ils traitent ces problèmes dans la pratique.

Pas une réponse formellement rigide, mais voici:

Le problème pour déterminer s'il s'arrête ou boucle pour toujours. Boucler sur des collections finies un élément à la fois ou entre un intervalle de nombres est correct. EDIT: Évidemment, cela ne fonctionnera que si la collection ou l'intervalle itéré est interdit de changer (par exemple, par immuabilité) quand il est itéré (ou au moins, interdit de croître).

La récursivité n'est probablement pas correcte, sauf si vous définissez une règle artificielle pour la rendre finie, comme autoriser une profondeur de pile maximale ou forcer qu'un paramètre non négatif diminue à chaque itération.

Les gotos arbitraires sont généralement mauvais. Les gotos en arrière sont très susceptibles de conduire à des boucles qui pourraient être infinies.

Les instructions whiles et do-whiles sont un problème, car elles dépendent d'une condition qui n'est pas garantie de changer ou non pendant l'exécution. Une manière possible (mais probablement très insatisfaisante) de restreindre cela est de donner un nombre maximum d'itérations possible.

Vous devez fournir une définition de votre langage de script, et qu'entendez-vous par «attendre» des scénaristes.

${\cal O}(n^\omega)$

Il y a un résultat similaire pour une classe de programme polynomial d'Aaron R. Bradley, Zohar Manna et Henny B. Sipma. Mais AFAIK (je peux me tromper ici), le temps d'exécution est doublement exponentiel (essentiellement le temps requis pour calculer une base Groebner).