Discussion :

[davcha]

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 :

Sélectionner tout - Visualiser dans une fenêtre à part

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 :

Sélectionner tout - Visualiser dans une fenêtre à part

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

[Matthieu Brucher]

Si on pouvait faire cela, ça simplifierait grandement la tâche de la preuve des programmes !
En fait, on peut montrer que sur un certain échantillon d'entrées, on a la même sortie, ça c'est assez facile à faire, le reste est plus complexe, si DrTopos passe par là, il te le dira aussi, je pense

[davcha]

Oui, je me doute.
C'est pas totalement innocent non plus comme question.

La deuxième question "encore plus difficile" c'est d'avoir une fonction qui prend deux algorithmes en entrée et qui renvoie un nombre représentant le degré de différence entre les deux algorithmes.
Là ça parait presque utopique je trouve. Déjà faudrait être capable de définir une "unité de différence", pas évident.

[DrTopos]

A la première question la réponse est très certainement non. Ceci me rappelle le problème de l'arrêt des machines de Turing: existe-t-il un algorithme capable de déterminer si un algorithme (ou une machine de Turing) va s'arreter on non. Turing a démontré que ça n'existe pas. Le problème que tu poses est analogue (et s'y ramène peut-être).

Quant-à la deuxième question, il faudrait savoir ce qu'on entend effectivement par 'différence'. Il y a peut-être des cas où on peut faire quelque chose, mais cela dépend sûrement des types de départ et d'arrivée. Si le départ est un type fini, et si le type d'arrivée a lui-même un tel algorithme d'égalité booléenne, alors ça peut marcher, sinon, même avec le type des entiers naturels comme départ, qui est le plus simple des types infinis, je crois qu'il n'y a aucune chance, à moins de se limiter à la comparaison d'algorithme très primitifs, sans boucle ni récursion.

En lambda-calcul, il existe un moyen de comparer les fonction. Il suffit de réduire les lambda-expressions à leurs formes normales et de comparer ces dernières. Toutefois, la notion d'égalité qu'on obtient de cette manière est plus faible que l'égalité mathématique des fonctions, à savoir que deux fonctions sont égales si et seulement si elles donnent la même valeur sur la même donnée. Par exemple, si on définit l'identité de N vers N par une récursion primitive:

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
 
f(0) = 0
f(n+1) = f(n) + 1

la réduction à la forme normale ne mettra pas en évidence le fait qu'il s'agit bien de la fonction identité.

[davcha]

En fait l'idée derrière ces questions est un système qui permetterait à un ordinateur de produire des algorithmes répondant à un ensemble de contraintes, sans intervention humaine (si ce n'est pour la définition des contraintes).

J'avais réalisé quelque chose comme ça il y a quelques temps en lambda-calcul, effectivement. Et ça marchait.... plus ou moins... euh mal.
Disons qu'il mettait énormément de temps à produire le code en lambda-calcul permettant d'ajouter 1 aux entiers naturels de church.

Dans tous les cas c'est une question qui m'a longtemps intéressé et m'intéresse toujours.
Quand j'ai commencé à m'y intéresser je pensais à faire quelque chose qui serait capable de produire un algorithme à partir de rien ou presque (un ensemble de contraintes).

En ce moment je cherche davantage à trouver un système, similaire, mais qui optimiserait un algorithme déjà existant selon certains axes.
Par exemple, optimiser la vitesse ou la taille du code (classique), mais aussi des choses plus "loufoques" du genre "produire un algorithme sans utiliser telle ou telle fonction" (par exemple : une factorielle sans utiliser l'opérateur de multiplication).

Donc concernant cette "différence" dont je parlais, dans la mesure où mon "petit truc en lambda-calcul" utilisait un algorithme génétique pour converger vers la solution, j'avais besoin d'un opérateur de "différence" pour déterminer la "distance à la solution" d'un algorithme (dans ce cas un bête lambda-terme) donné.


Le gros problème dans cette question, je crois, est d'être suffisamment descriptif quand on utilise une fonction ou un opérateur du langage.

Par exemple, si je refaisais ce petit programme en me basant sur autre chose que du lambda calcul pur, j'aurais bien du mal à faire "comprendre" à la machine qu'il y a un rapport entre l'opérateur + et * dans l'ensemble des entiers naturels.
Il faudrait quasiment "décomposer" l'opérateur * en instructions atomiques. C'est pour ça que je trouvais le lambda calcul pur très intéressant, d'ailleurs, puisque tout est "construit" suivant 2-3 principes logiques.
Ces 2-3 principes sont en fait nos "briques de base" et on peut jouer aux légos à partir de là. Mais si on touche à quelque chose de plus élaboré, ça devient tout de suite beaucoup plus problématique parce que le rapport entre un opérateur et un autre est "caché", dans la mesure où on a pas accès à "l'algorithme de ces opérateurs".

Je ne sais pas si je suis très compréhensible, par contre.

[méphistopheles]

A la première question la réponse est très certainement non. Ceci me rappelle le problème de l'arrêt des machines de Turing: existe-t-il un algorithme capable de déterminer si un algorithme (ou une machine de Turing) va s'arreter on non. Turing a démontré que ça n'existe pas. Le problème que tu poses est analogue (et s'y ramène peut-être).

Je me trompe surement, et ce n'est surement pas vrai pour toutes les fonctions, mais dans l'exemple donné par davcha, je crois qu'un système de calcul formel évolué pourrais nous donne facilement la solution (enfin avec maple par exemple, ça marche pour ces deux fonctions en lui mettant un factor à la fin).

évidement, avec des expressions compliquées, il et fort possible que le système obtenue en sortie soit encombré et inutilisable... Surtous si le nombre de variables en entrée est grand.

enfin, ce n'est qu'une idée ...


Pour la différence, on peu peut-être d'apliquer la même methode, mais à condition d'avoir le même nombre de varaible et des variables de même type en paramètres dans les deux fonctions... et encore.

[Tellmarch]

Il est possible dans une certaine mesure de dire si 2 algorithmes sont identiques.
Par exemple de nombreuses recherches sont effectuées en sémantique des langages de programmation à propos de ça.

voir par exemple http://fr.wikipedia.org/wiki/S%C3%A9..._programmation
pour une très courte introduction.

Il existe plusieurs types de sémantiques qui s'interessent justement à définir des équivalence entre programmes.
Par exemple la sémantique dénotationnelle consiste à associer à un programme la fonction mathématique qu'il calcule, c'est une forme d'équivalence.

un lien par exemple : http://www.risc.uni-linz.ac.at/peopl...em/densem.html

Donc la réponse à la premiere question est oui, au moins en partie.

[DrTopos]

Je me trompe surement, et ce n'est surement pas vrai pour toutes les fonctions, mais dans l'exemple donné par davcha, je crois qu'un système de calcul formel évolué pourrais nous donne facilement la solution (enfin avec maple par exemple, ça marche pour ces deux fonctions en lui mettant un factor à la fin).

C'est possible.
J'ai seulement dit qu'il n'existe pas d'algorithme capable étant donné deux fonctions quelconques f et g de N vers N de répondre à coup sûr vrai ou faux. Il est bien certain que des algos (d'intelligence artificielle) peuvent trouver la réponse dans certains cas. Ce qu'ils ne peuvent pas faire est de trouver la réponse dans tous les cas.

Il existe plusieurs types de sémantiques qui s'interessent justement à définir des équivalence entre programmes.
Par exemple la sémantique dénotationnelle consiste à associer à un programme la fonction mathématique qu'il calcule, c'est une forme d'équivalence.

Sauf que cela ne fait que déplacer le problème, puisque l'égalité entre fonctions mathématiques n'est pas plus décidable que l'égalité entre algorithmes.

Question: existe-t-il un algo capable de répondre oui ou non ou éventuellement de tourner indéfiniment ou de prépondre qu'il ne sait pas ? Reponse oui.

Question: existe-t-il un algo qui termine toujours en répondant oui ou non ? Réponse: non.

C'est tout ce que je voulais dire.

[10_GOTO_10]

Ces deux algorithmes sont égaux:

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
bool Fermat(unsigned int x, unsigned int y, unsigned int z)
  {
  if (x * x * x + y * y * y == z * z * z) return true;
  else return false;
  }

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
bool Fermat(unsigned int x, unsigned int y, unsigned int z)
  {
  return false;
  }

Mais le programme qui démontrera leur équivalence aura trouvé une démonstration au grand théorème de Fermat... Si quelqu'un sur ce forum pouvait m'écrire un petit programme qui fasse ça, ça m'interesse.

[Tellmarch]

je n'ai pas dit qu'il y avait un algorithme terminant toujours capable de décider de l'équivalence de deux algorithmes, juste qu'il y avait beaucoup de travail effectué dans ce sens, pour dire que c'était pas absurde d'imaginer ça...

Je suis d'accord qu'il n'est pas possible d'avoir une fonction qui décide ça, vu que c'est peut etre effectivement indécidable.
Par contre si on impose que les algos examinés terminent, c'est peut etre deja décidable, je ne suis pas sur, il faudrait que je reflechisse un peu plus...

Enfin dans tous les cas on peut avoir un algorithme capable de donner dans beaucoup de cas une preuve de l'équivalence de deux programmes.

Par exemple un systeme comme coq peut trouver des preuves d'equivalence de deux programmes.

Sauf que cela ne fait que déplacer le problème, puisque l'égalité entre fonctions mathématiques n'est pas plus décidable que l'égalité entre algorithmes.

Dans ce cas les fonctions ne seraient pas quelconques, donc ce n'est pas si évident que ça...

[DrTopos]

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.

[DrTopos]

je n'ai pas dit qu'il y avait un algorithme terminant toujours capable de décider de l'équivalence de deux algorithmes, juste qu'il y avait beaucoup de travail effectué dans ce sens, pour dire que c'était pas absurde d'imaginer ça...

Bien sûr, la recherche de preuves fait partie des directions possibles de l'intelligence artificielle, et c'est très prometteur malgré les limitations théoriques que l'on connait.

Par contre si on impose que les algos examinés terminent, c'est peut etre deja décidable, je ne suis pas sur, il faudrait que je reflechisse un peu plus...

Même là, c'est sans espoir me semble-t-il. Moi aussi, il faudrait que j'y réfléchisse. Mais il me semble que même dans le cas des fonctions primitivement récursives (qui terminent tout le temps), ça ne marche pas.

Enfin dans tous les cas on peut avoir un algorithme capable de donner dans beaucoup de cas une preuve de l'équivalence de deux programmes.

'beaucoup' est subjectif. Il est vrai que dans le cas du métro Meteor, le système B a trouvé lui-même 80% des preuves. Mais, les énoncés étaient loin d'être aussi durs que Fermat. C'est encourageant quand-même, et ça montre bien qu'il y a quelque chose à faire dans cette direction.

[Tellmarch]

'beaucoup' est subjectif. Il est vrai que dans le cas du métro Meteor, le système B a trouvé lui-même 80% des preuves. Mais, les énoncés étaient loin d'être aussi durs que Fermat. C'est encourageant quand-même, et ça montre bien qu'il y a quelque chose à faire dans cette direction.

Oui c'est vrai que c'est subjectif, mais je me plaçais dans la situation des programmes courant... en général prouver la correction d'un algorithme ne fait pas intervenir le théoreme de Fermat et sa preuve de 400 pages, il s'agit souvent juste de quelques regles de calcul élémentaires...

Pour de tels programmes je pense qu'un systeme existant de démonstration automatique marcherait bien. Je n'ai pas essayé, mais j'ai deja utilisé les mécanismes de preuve d'algorithmes en coq, et les preuves sont suffisament simples en général pour pouvoir etre trouvées automatiquement.

[10_GOTO_10]

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.

Oui, tout à fait. Pardon à Monsieur Fermat d'avoir pris des libertés avec son théorème, c'était juste pour me faire comprendre (j'aurais traité tous les cas, mon propos aurait été juste mais moins clair).

[méphistopheles]

je pense qu'on peut donc pour notre ami davcha se limmiter aux fonctions simples qui peuvent renvoyer des variables en sortie (plutot que de tester sur tout l'ensemble des nombres), en ayant quelques fonctions d'égalité de base... (dont par exemple le théorème de fermat).

par contre, ça consisterais à réécrire la fonction en remplaçant les variables par des expressions de variables... j'espère qu'il existe un système pour lire directement du code entré en string en execution, par-ce que si on doit remplacer toutes les chaines de caractères d'instructions par les instructions elles-mêmes, on est pas sorti de l'auberge...

[j.p.mignot]

DrTopos à écrit

J'ai seulement dit qu'il n'existe pas d'algorithme capable étant donné deux fonctions quelconques f et g de N vers N de répondre à coup sûr vrai ou faux.

Cela me semble parfaitement sur si non - sauf erreur de ma part - on serait en contradiction avec le théorème d'incomplétude de Goedel.

[Tellmarch]

Enfin bon il faudrait préciser un peu le contexte de toute façon...
Sur une architecture fixée, et si on ne traite que des algorithmes qui terminent, les entiers sont peut etre codés sur 32 bits par exemple, et dans ce cas le probleme est clairement décidable, vu qu'il suffit de tester tous les entiers possibles