Investigations métamathématiques dans les lambda-calculs typés pédagogiques

Mots clés

lambda-calcul, théorie des types, théorie de la démonstration, constructivisme, isomorphisme Curry-Howard

Détail de l'offre

Les lambda-calculs typés pédagogiques (et les systèmes de déduction naturelle pédagogiques qui leur correspondent au travers de l'isomorphisme de Curry-Howard) sont des modèles de calcul et du raisonnement mathématique dans lesquels une contrainte supplémentaire par rapport aux systèmes de types habituels est imposée: il est demandé à chaque fois que l'on fait un ensemble d'hypothèses (ou que l'on déclare un ensemble de variables) de donner un EXEMPLE de situation où les hypothèses sont vérifiées.
Cette contrainte fait écho à la pratique courante dans l'enseignement d'illustrer une situation abstraite par un exemple qui 'aide à se faire une idée' de cette situation abstraite. Actuellement dans les systèmes formels de fondements des mathématiques et de l'informatique aucune contrainte semblable n'existe, on peut donc par exemple supposer 'soit X un cercle rectangulaire', ce qui est stérile car un tel objet n'existe pas. Noter que les programmes de démonstration automatique actuels passent une partie de leur temps à émettre des hypothèses inutiles comme celle-ci.
Dès qu'un système logique pédagogique est défini parfaitement formellement des questions très simples se posent: quel est le pouvoir expressif logique et algorithmique de ce système ? La contrainte pédagogique de ce système limite-t-elle la démonstration de théorèmes utiles?
Les premiers résultats obtenus ont concerné ces questions fondamentales.
Deux thèses ont été soutenues à l'Université de Lorraine. Ce domaine est entièrement nouveau et demande à être développé.