Lundi 17 Novembre 2025 de 18h à 20h en Salle W du DMA à l'ENS

Henri Lombardi (LmB)

La méthode dynamique
pour décrypter constructivement
les démonstrations classiques

En 1985, paraît un article révolutionnaire de deux pages,
cité aujourd'hui comme D5 :

Della Dora J., Dicrescenzo C. et Duval D.
About a new method for computing in algebraic number fields.
In Caviness B.F. (Ed.) EUROCAL’85. Lecture Notes in Computer Science 204, 289–290. Springer (1985).

Dix-huit ans auparavant, était paru un ouvrage encore beaucoup plus révolutionnaire,
qui refondait les mathématiques constructives sur des bases intuitives parfaitement claires :

Errett Bishop, Foundations of Constructive Analysis. McGraw Hill, (1967).

Cet ouvrage traite les fondements de l'analyse moderne.
Dans ce livre tous les théorèmes correspondent à des algorithmes.
En particulier les théorèmes d'existence
construisent les objets dont on affirme qu'ils existent.

L'article D5 est basé sur ce que l'on appelle
l'évaluation paresseuse en informatique théorique.

On peut le voir comme donnant une sémantique constructive claire
pour l'objet "clôture algébrique d'un corps calculable".

Alors même que l'on sait que l'objet
"clôture algébrique d'un corps calculable K"
ne peut pas être construit en général comme un corps calculable.

La méthode dynamique qui généralise D5
est désormais un outil efficace et bien établi
pour la réalisation du programme de Bishop
de décryptage constructif des démonstrations classiques.

En fait cette méthode a déjà été inventée en 1953
par Paul Lorenzen dans son article :

Die Erweiterung halbgeordneter Gruppen zu Verbandsgruppen.
Math. Z., 58, 15–24, 1953.
http://eudml.org/doc/169331

Voir à ce sujet :

Thierry Coquand, Henri Lombardi, and Stefan Neuwirth.
Regular entailment relations, 2021.
https://arxiv.org/abs/1912.09480