Comment vérifiez-vous si deux algorithmes (disons, Tri par fusion et Tri naïf) renvoient le même résultat pour n'importe quelle entrée, lorsque l'ensemble de toutes les entrées est infini?
Mise à jour: Merci Ben d' avoir décrit comment cela est impossible à faire algorithmiquement dans le cas général. La réponse de Dave est un excellent résumé des méthodes algorithmiques et manuelles (soumises à l'esprit humain et à la métaphore) qui ne fonctionnent pas toujours, mais sont assez efficaces.
Réponses:
Contrairement à ce que disent les opposants, il existe de nombreuses techniques efficaces pour ce faire.
La bisimulation est une approche. Voir, par exemple, l'article de Gordon sur la coinduction et la programmation fonctionnelle .
Une autre approche consiste à utiliser les théories opérationnelles de l'équivalence des programmes, comme le travail de Pitts .
Une troisième approche consiste à vérifier que les deux programmes satisfont à la même spécification fonctionnelle. Il existe des milliers d'articles sur cette approche.
Une quatrième approche consiste à montrer qu'un programme peut être réécrit dans l'autre en utilisant des transformations de programmes sonores .
Bien sûr, aucune de ces méthodes n'est complète en raison de l'indécidabilité, mais des volumes et des volumes de travail ont été produits pour résoudre le problème.
la source
Pour élaborer un peu sur les affirmations «c'est impossible», voici un simple croquis de preuve.
Nous pouvons modéliser des algorithmes avec sortie par Turing Machines qui s'arrêtent avec leur sortie sur leur bande. Si vous voulez avoir des machines qui peuvent s'arrêter en acceptant avec une sortie sur leur bande ou en rejetant (dans ce cas, il n'y a pas de sortie), vous pouvez facilement trouver un encodage qui vous permet de modéliser ces machines avec le "stop ou stop non", il n'y a pas de machines à rejeter.
Supposons maintenant que j'ai un algorithme P pour déterminer si deux de ces MT ont la même sortie pour chaque entrée. Puis, étant donné un TM A et une entrée X , je peux construire un nouveau TM B qui fonctionne comme suit:
Maintenant , je peux courir P sur A et B . B ne s'arrête pas sur X , mais a la même sortie que A pour toutes les autres entrées, donc si et seulement si A ne s'arrête pas sur X, ces deux algorithmes ont la même sortie pour chaque entrée. Mais P était supposé pouvoir dire si deux algorithmes ont la même sortie pour chaque entrée, donc si nous avions P, nous pourrions dire si une machine arbitraire s'arrête sur une entrée arbitraire, ce qui est le problème de l'arrêt. Puisque le problème de l'arrêt est connu pour être indécidable, P ne peut pas exister.
Cela signifie qu'il n'y a pas d'approche générale (calculable) pour déterminer si deux algorithmes ont la même sortie qui fonctionne toujours, vous devez donc appliquer un raisonnement particulier à la paire d'algorithmes que vous analysez. Cependant, dans la pratique, il peut y avoir des approches calculables qui fonctionnent pour de grandes classes d'algorithmes, et il existe certainement des techniques que vous pouvez utiliser pour essayer de trouver une preuve pour un cas particulier. La réponse de Dave Clarke vous donne quelques éléments pertinents à regarder ici. Le résultat de "l'impossibilité" ne s'applique qu'à la conception d'une méthode générique qui résoudra le problème une fois pour toutes, pour toutes les paires d'algorithmes.
la source
C'est impossible en général, mais de nombreuses contraintes peuvent le rendre possible. Par exemple, vous pouvez vérifier l'équivalence de deux programmes de code linéaire utilisant des BDD. L'exécution symbolique peut gérer de nombreux autres cas.
la source
Il est impossible de concevoir un algorithme qui prouve cette égalité en général. Astuce: réduction du problème Halting.
la source