Vers un calcul des constructions pédagogique

• Main Author: Demange, Vincent
• Language: FRE
• Published: Université de Metz 2012
• Subjects: [INFO:INFO_LO] Computer Science/Logic in Computer Science; [MATH:MATH_LO] Mathematics/Logic; logique; systèmes formels; systèmes fonctionnels; théorie des types; calcul des constructions; mathématiques sans négation; pédagogie formelle
• Online Access: http://tel.archives-ouvertes.fr/tel-00838147; http://tel.archives-ouvertes.fr/docs/00/83/81/47/PDF/these.pdf; http://tel.archives-ouvertes.fr/docs/00/83/81/47/ANNEX/slides.pdf

Les systèmes pédagogiques sont apparus récemment à propos des calculs propositionnels (jusqu'à l'ordre supérieur), et consistent à donner systématiquement des exemples des notions (hypothèses) introduites. Formellement, cela signifie que pour mettre un ensemble Delta de formules en hypothèse, il est requis de donner une substitution sigma telle que les instances de formules sigma(Delta) soient démontrables. Cette nécessité d'exemplification ayant été pointée du doigt par Poincaré (1913) comme relevant du bon sens: une définition d'un objet par postulat n'ayant d'intérêt que si un tel objet peut être construit. Cette restriction appliquée à des systèmes formels intuitionnistes rejoint l'idée des mathématiques sans négation défendues par Griss (1946) au milieu du siècle dernier, et présentées comme une version approfondie de l'intuitionnisme. À travers l'isomorphisme de Curry-Howard (1980), la contrepartie calculatoire est l'utilité des programmes définis dans les systèmes fonctionnels correspondants: toute fonction peut être appliquée à un argument clos. Les premiers résultats concernant les calculs propositionnels jusqu'au second ordre ont été publiés récemment par Colson et Michel (2007, 2008, 2009). Nous exposons dans cette thèse une tentative d'uniformisation et d'extension au Calcul des Constructions (CC) des précédents résultats. Tout d'abord une définition formelle et précise de sous-système pédagogique du Calcul des Constructions est introduite, puis différents tels sous-systèmes sont déclinés en exemple.