Démonstration constructive
Cet article est une ébauche concernant les mathématiques.
Vous pouvez partager vos connaissances en l’améliorant (comment ?) selon les recommandations des projets correspondants.
Consultez la liste des tâches à accomplir en page de discussion.
Une première vision d'une démonstration constructive est celle d'une démonstration mathématique qui respecte les contraintes des mathématiques intuitionnistes, c'est-à-dire qui ne fait pas appel à l'infini, ni au principe du tiers exclu. Ainsi, démontrer l'impossibilité de l'inexistence d'un objet ne constitue pas une démonstration constructive de son existence : il faut pour cela en exhiber un et expliquer comment le construire.
Si une démonstration est constructive, on doit pouvoir lui associer un algorithme. Cet algorithme est le contenu calculatoire de la démonstration. La correspondance de Curry-Howard énonce cette association, usuellement appelée correspondance preuve-programme, pour les démonstrations constructives.
Une deuxième vision d'une démonstration constructive découle de la remarque précédente, c'est une démonstration à laquelle on peut donner un contenu calculatoire.
En 1990, Timothy G. Griffin étend la correspondance de Curry-Howard à la loi de Peirce, ((α → β) → α) → α[1], et montre ainsi que l'on peut associer, via des continuations, un contenu calculatoire à la logique classique, faisant d'elle une logique constructive[2].
Exemples[modifier | modifier le code]
Un exemple de démonstration constructive est la démonstration du théorème de Stone-Weierstrass qui utilise les polynômes de Bernstein. Un autre exemple est la démonstration du théorème de Brooks qui utilise l'algorithme glouton de coloration des graphes.
Notes et références[modifier | modifier le code]
- Griffin, Timothy G. (1990), The Formulae-as-Types Notion of Control, Conf. Record 17th Annual ACM Symp. on Principles of Programming Languages, POPL '90, San Francisco, CA, USA, 17–19 janvier 1990, p. 47–57.
- Voir notamment Jean-Yves Girard « A New constructive logic: classical logic » [PDF], INRIA, Rapport de recherche no 1 443, juin 1991 et les travaux de Jean-Louis Krivine.
