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.