Le lambda-calcul et la formalisation des maths
avec Marco
Marco
est arrivé à Nice en 2001 comme post-doc du CNR italien,
pour faire de la géométrie algébrique sous ma
responsabilité.
Un peu par hasard, il a suivi mon cours de DEA sur le
lambda-calcul,
et nous avons rapidement constaté tous les deux que
ce
sujet lui convenait encore mieux que la géométrie
algébrique.
Depuis, genre vers 2003, il a obtenu un post-doc CNRS d'un an
pour faire de la formalisation des
maths sous ma
responsabilité.
La consigne du CNRS etait qu'il fallait
absolument le caser après.
C'était un peu stressant mais
finalement, l'année suivante,
il a gagné un poste
permanent de chercheur à Florence.
Mon projet avec Marco est un de mes trois projets prioritaires.
Il s'agit
de domestiquer les ordinateurs pour qu'on puisse faire nos maths avec. Voici
où on en est.
Notre premier travail est plus ou moins terminé. On y trouve une
approche originale à la fois
de la syntaxe abstraite d'ordre supérieur et du lambda-calcul (pur)
que
nous caractérisons comme la monade "exponentielle" initiale.
On savait depuis longtemps qu'un lambda-calcul typé est plus ou moins
une catégorie cartésienne close, mais on n'avait rien de tel pour
les lambda-calculs non typés.
La question de maitriser la syntaxe avec lieurs (syntaxe d'ordre
supérieur)
est une question brûlante en informatique,
voir par exemple le
Poplmark challenge.
D'ailleurs, pour vérifier que notre approche est performante, nous
avons nous-mêmes programmé une
solution de la partie A1 de
ce challenge, que nous sommes en train de peaufiner avant soumission.
Il y a
bientôt deux ans que nous avons compris notre caractérisation
du lambda-calcul et
il nous a fallu tout ce temps pour en terminer la
preuve sur ordinateur.
Il s'agit sans doute de l'énoncé le plus
abstrait prouvé sur ordinateur.
Nous manipulons des monades et des
morphismes entre modules sur des monades alors que
les tours de force qu'on
connaît (théorème fondamental de l'algèbre,
théorème des quatre couleurs,
théorème de Jordan
sur les courbes planes)
ne manipulent pas des structures aussi abstraites.
Pour se faire une petite idée de ce travail, on peut
Ce travail n'est qu'un début. Voici les directions dans lesquelles
on s'est déjà engagés.
- Notre définition du lambda-calcul pur n'est qu'une étape.
Nous savons déjà qu'on peut avantageusement
voir le lambda-calcul
comme une certaine monade en catégories initiale. Nous avons
déjà écrit l'énoncé, et compris tous les
points-clefs de la démonstration,
mais la preuve formelle
de ce résultat nous prendra sans doute encore un an.
- Notre preuve sur ordinateur (tout comme notre solution du challenge) est
encore bien trop compliquée.
Nous
réfléchissons depuis longtemps à ce qu'il faut mettre en place pour que ces
preuves deviennent
compréhensibles et acceptables pour un
mathématicien pas trop obtus.
- Nous n'avons pas encore une philosophie stable sur la "bonne" façon
de programmer la théorie des ensembles.
Nous avons proposé (voir
notre
preprint, et sorry pour la biblio)
une
approche originale pour réconcilier types et ensembles,
à base de
"typoïdes" et de localisation de catégories.
Cette vision des choses aura sans
doute sa place dans
la construction finale,
mais il faut encore beaucoup travailler pour en faire une solution
performante.
André Hirschowitz
Last
modified: December2005