Lazi

Problème de la force d'une fonction de recherche

Contexte

Pour la doc "Réflexions en sub-physique", j'aimerais montrer un exemple de fonction qui s'améliore elle-même. Pour cela j'ai besoin d'une comparaison pour déterminer, entre deux fonction de recherche de preuves, laquelle est la plus forte.

Question

Pour deux fonctions de recherche de preuve (voir "Réflexions en sub-physique"), comment comparer la force de telles fonctions ?

Étude

Le problème

On peut compter les temps de calculs cumulés pour toutes les formules classées par longueur de preuve minimale et comparer ces temps. Mais le problème est que l'on peut trouver une suite de fonctions de recherche de preuve croissantes pour l'ordre de la force , mais qui convergent vers un maximum qui peut pourtant être dépassé. Pour cela il suffit de partir d'une fonction de recherche de preuve qui peut être améliorée sur un ensemble E infini de vérités. On partitionne E en une union infini d'ensembles infinis, et on cré une suite de fonction de recherche de preuve qui améliore la précédente sur un élément de la partition. On pourrait par exemple le faire sur les racines des polynomes de second degré, en partitionnant suivant les paramètres du polynome.

Essai 2 : Solution du ratio fixe

On demande à ce que le ratio des temps de calculs cumulés entre les deux fonctions de recherche soit à partir d'un certain n, ≤ à une valeur fixée à l'avance et inférieur à 1. Cela assure qu'il y a une différence significative et que la multiplication des rations tendent vers 0, c'est à dire que l'efficacité augmente indéfiniment.

Essai 1 : Solution du ratio

On demande à ce que le ratio des temps de calculs cumulés entre les deux fonctions de recherche soit à partir d'un certain n, ≤ à une valeur dite "ratio de force" inférieur à 1. Cela assure qu'il y a une différence significative.

Problème : on pourrait créer une suite de fonction de recherche de telle sorte que le ration de force avec la précédente tende vers 1. Et donc au final en multipliant les ratios, on ne tendrait pas vers zero.

Réponse

Voir la solution de l'essai 2.