Minimisation du programme

La minimisation des circuits est le problème pour minimiser la taille d'un circuit donné. Existe-t-il quelque chose de similaire pour les programmes généraux?

En particulier, ma question est -

Existe-t-il des algorithmes pour minimiser le nombre d'instructions pour un programme donné. Je sais que c'est un problème indécidable mais je ne cherche pas une solution qui renvoie quelque chose d'optimique.

Bien que l'on puisse appliquer des transformations de compilateur préexistantes pour y parvenir, je cherche quelque chose où je n'ai pas à définir un ensemble de transformations et d'algorithmes très étroits pour les rechercher à l'avance.

Edit: L'autre question que je me pose est de savoir si l'on peut avoir un calcul solide et complet qui nous permet d'explorer tout l'espace de ces programmes sémantiquement équivalents ou n'est-ce pas possible.

Il existe un algorithme naïf pour les programmes avec des entrées de taille limitée: énumérer tous les programmes par ordre croissant de longueur (ou temps d'exécution, qui est une fonction limitée de la longueur). Si vous pouvez prouver que le programme est équivalent à l'original, arrêtez; sinon continuez à chercher.

Cet algorithme est solide. Pour qu'il soit complet, vous devez être en mesure de prouver que tous les programmes rejetés ne sont pas équivalents à l'original. Cela est possible dans les modèles de machines finitaires, tant que vous avez une limite pour la taille d'entrée.

Notez que lorsque le temps d'exécution du programme dépend de l'entrée, il peut ne pas y avoir de solution optimale. Si vous recherchez, par exemple, le pire des cas, vous rencontrerez très rapidement des équivalences indécidables lorsque vous quantifiez sur toutes les entrées illimitées possibles, et des problèmes insolubles si les entrées sont limitées.

Il y a dix ans, «Denali: un superoptimiseur dirigé par un objectif» par Rajeev Joshi, Greg Nelson et Keith Randall a pu trouver des programmes optimaux d'environ 5 instructions machine. Je n'ai pas regardé de résultats plus récents.