Test d'égalité entre deux algorithmes, ça existe, est-ce faisable ?
Imaginons un algorithme, une fonction, qui prend deux algorithmes en paramètre et qui renvoie :- "vrai" si les deux algorithmes sont "égaux",
- sinon "faux".
Deux algorithmes sont "égaux" (du moins c'est ce que je signifie par cette expression ici), si les deux algorithmes, dans un contexte identique, renvoient des données identiques.
Exemples:
Ces deux algorithmes sont égaux :
Code:
1
2
3
4
5
6
7
8
9
| unsigned int multiplication(unsigned int a,unsigned int b){
return a*b;
}
unsigned int multiplication2(unsigned int a,unsigned int b){
unsigned int result=0;
for(unsigned int i=0;i<a;i++)
result+=b;
return result;
} |
Ces deux algorithmes ne sont pas égaux :
Code:
1
2
3
4
5
6
7
8
9
| double multiplication(double a,double b){
return a*b;
}
double multiplication2(double a,double b){
int result=0;
for(int i=0;i<a;i++)
result+=b;
return result;
} |
Et j'ai une question encore plus compliquée qui viendra après, mais après seulement :P
Qu'est-ce que unsigned int ?
10 GOTO 10 >> Ton exemple convainc immédiatement de la difficulté du problème, et même montre que dans le cas d'un langage comme C, la situation est encore pire.
D'abord, quelques remarques à propos de Fermat. D'abord, il faut demander que les solutions soient non triviales. Par exemple 5^3 + 0^3 = 5^3 marche. De plus, le théorème de Fermat pour l'exposant 3, n'est pas le grand théorème de Fermat, mais un cas particulier. Il n'est pas si facile à résoudre malgré tout, puisque c'est seulement un siècle après son énoncé par Fermat qu'Euler est venu à bout de ce cas particulier.
Mais ton exemple met en évidence un autre problème. Qu'est-ce que unsigned int ? Sur la plupart de nos ordinateurs c'est l'anneau Z/(2^32)Z, mais il ne semble pas que la norme du C l'impose. En tout cas, ce n'est pas l'ensemble des entiers naturels. Il en résulte que sans hypothèse supplémentaire, il me semble de toute façon impossible pour un programme de décider de l'égalité de fonctions utilisant le type unsigned int. Il se peut par ailleurs (je ne suis pas assez arithméticien pour le savoir), que l'équation x^3 + y^3 = z^3 ait des solutions non triviales sur l'anneau Z/(2^32)Z.
Autre chose. En logique, on montre facilement que tout énoncé est mécaniquement équivalent à une égalité entre données dont le type peut être fonctionnel (ce qui arrive par exemple quand on traduit un énoncé universellement quantifié). Si un test d'égalité existait pour tous ces types, on aurait un algorithme pour résoudre n'importe quel problème de mathématiques. On sait bien qu'un tel algorithme n'existe pas. Evidemment, davcha n'en demandait pas tant. Je crois que si on veut arriver à quelque chose dans cette direction, il faut d'abord bien préciser les types qui interviennent (avec des définition précises), et se limiter à certaines constructions de données (donc en particulier de fonctions ou d'algorithmes) pas trop méchantes. Ce que je crois est que dès qu'il y aura de la récursion dans les méthodes de définition des fonctions, on ne pourra pas obtenir un algorithme capable de décider dans tous les cas.
