Retour à la page du séminaire

26/03/99: Jean Goubault (Dyade, Rocquencourt)
Encore un calcul du premier ordre pour le lambda-calcul.

résumé

Le lambda-calcul n'est pas un formalisme du premier ordre, ce qui signifie que les algorithmes manipulant des termes du lambda-calcul sont usuellement rendus complexes par le besoin de manipuler des variables liees en respectant leur portee. En fait, ne serait-ce que coder une machine implementant la reduction de lambda-termes est une activite parsemee de difficultes.
Dans ce but (parfois pour d'autres raisons), de nombreux chercheurs ont propose des calculs du premier ordre, c'est-a-dire sans variables liees, realisant exactement la reduction du lambda-calcul : combinateurs de Curry-Sch"onfinkel, lambda-sigma-calcul d'Abadi-Cardelli-Curien-Levy, et leurs quelques centaines de variantes.
Un probleme vexant est alors que pour chacun de ces calculs, il y a toujours au moins une bonne propriete du lambda-calcul qu'il ne possede pas : confluence, terminaison dans le cas type, preservation de la normalisation forte, simulation de la beta-reduction notamment.
Je presenterai deux nouveaux calculs, SKIn (du a Healfdene Goguen) et SKInT (venant de mes travaux sur S4), dont je discuterai des proprietes. En particulier, SKInT a (quasiment) toutes les proprietes requises, et il semble que ce soit le premier calcul du premier ordre ayant toutes ces bonnes proprietes.
Enfin, j'illustrerai SKInT par la conception d'une machine a reduction, de facture classique, mais fonctionnant sur une structure de donnees tres proche de la structure de gap utilisee dans les traitements de texte comme Emacs.