D’autres Livres d’intérêt

Les décompilateurs : L’univers en tête

Jean-Louis Krivine

Le livre de Krivine présente pour un large public intéressé aux sciences des propositions et des résultats radicalement nouveaux. Le livre est écrit sans recourir à aucun formalisme.

En ce qui concerne les mathématiques, il étend la correspondance preuves-programme (dite de Curry -Howard) à toutes les mathématiques en donnant les programmes des axiomes de la théorie des ensembles er ceux de l’axiome du choix général. Cela résout le problème d’Hilbert, les programmes étant les structures finies que Hilbert cherchait en mathématiques où d’après le théorème d’incomplétude de Gödel elles n’existent pas !

En particulier grâce à la machine de Krivine il devient possible d’écrire ces programmes en logique combinatoire étendue par Krivine par des instructions correspondant à la pile côté informatique et au code CC traduction de l’axiome du tiers exclu. On peut donc obtenir ces programmes en un langage type langage machine.

Vient ensuite ce qui est une hypothèse très largement admise en éthologie : certains programmes associés au comportement physique et sensoriel des mammifères (par exemple) sont la trace laissée lors de l’évolution par les interactions des animaux avec leur environnement. Homo sapiens est une espèce animale. Il n’y a des lors aucun mystère sur le fait que la physique s’écrit en mathématiques !

Pour expliquer comment faire des démonstrations, mathématiciens et philosophes ont recours à une notion, peu précise, l’intuition. Il est alors raisonnable de penser que l’intuition consiste à lire dans son propre cerveau les programmes et les traduire en mathématique. C’est décompiler si l’on considère les mathématiques écrites en théorie des ensembles comme un langage très évolué que Krivine justifie en détail.

Compilées, les démonstrations donnent les mathématiques écrites formellement comme un programme écrit en langage binaire interprété maintenant comme un programme du cerveau.

Si l’on prend le programme correspondant à une démonstration très simple, par exemple du théorème de Rolle, ce programme écrit en langage machine, nous ne comprenons pas, à ce jour comment il a été écrit au fil des millions d’année de l’évolution. Avis de recherche :une porte est ouverte vers certains programmes du cerveau, communs à bien des espèces animales, ceux de la physique en particulier.