Cette page est accessible
depuis la page Web du cours :
http://www.pps.jussieu.fr/~kesner/enseignement/mpri/caf/
Calculs Algébriques et Fonctionnels
Cours de Gérard Huet
Cette page donne accès aux documents pertinents au cours
"Calculs Algébriques et Fonctionnels", donné à l'automne 2004 dans le cadre
du MPRI (Mastère Parisien de Recherche en Informatique).
Notes de cours de CMU
Le document pdf
Formal Structures for Computation and Deduction constitue
les notes d'un cours donné à l'Université Carnegie-Mellon au printemps 1986.
Il présente l'état de l'art il y a 20 ans d'un domaine qui a progressé
dans les détails, mais non dans la présentation des notions fondamentales.
Ce cours s'efforçait de présenter les définitions et les énoncés sous une
forme complètement exécutable dans le langage ML. Cette implémentation de
ML est progressivement devenue Caml, puis OCaml. De légères différences
de syntaxe nécessitent une adaptation des programmes correspondants.
Constructive Computation Theory
Le cours de CMU ne comportait de présentation exécutable que pour les 6
premiers chapitres, couvrant en gros la Réécriture (théorie des calculs
algébriques) et la Programmation Logique. La programmation fonctionnelle,
c'est à dire la réécriture orthogonale et le lambda-calcul, ainsi que les
parties catégoriques et logiques culminant avec le Calcul des Constructions,
étaient encore rédigées dans un méta-langage de mathématiques molles.
Le document pdf Constructive Computation Theory
présente sous une forme homogène exécutable le lambda-calcul pur.
La bibliothèque Ocaml correspondante, qui peut être utilisée par les
versions récentes d'Ocaml, est disponible ici.
Ce cours, enseigné dans divers DEAs ces dernières années, donne une
introduction à la théorie de la calculabilité effective présentée par
le lambda-calcul.
Axiomatisation des calculs fonctionnels
L'utilisation d'un langage de programmation, aussi bien défini sémantiquement
qu'il soit, n'est pas pleinement satisfaisante pour servir de fondement
à un développement de nature mathématique, ne serait-ce que par le risque
de non-terminaison d'une définition récursive. On peut estimer que dans
un futur proche, les développements mathématiques seront disponibles sous
une forme absolument rigoureuse et mécaniquement vérifiée, par l'utilisation
de formalismes logiques du style "Théorie des Types". C'est ainsi
que toute la partie "confluence" du cours de lambda-calcul a été développée
dans le Calcul des Constructions Inductives, et vérifiée dans le
système Coq. L'article correspondant est disponible sous format pdf comme
Residual Theory.
Notes de cours de Marktoberdorf
Dans ce style ont été développées diverses axiomatisations en Coq,
rassemblées l'été 1995 dans les notes de cours d'une école d'été
à Marktoberdorf, disponible sous format pdf
ici.
Récurrence et terminaison
Le dernier chapitre du cours de CMU traitait du raisonnement par récurrence
dans un cadre général. Ce sujet important, et qui fera l'objet d'un
cours spécifique au Mastère, est tiré à part dans un article
disponible sous format pdf ici.
Logiciels
Les principaux logiciels utilisés dans le cours sont
Objective Caml
et Coq.
En cas de difficulté, n'hésitez pas à
m'écrire.
Programme provisoire
Cours 1 (27-9) - Echauffement. Notion de calcul. Calcul formel.
Formules-expressions (syntaxe concrète) et formules-termes (syntaxe abstraite).
Liaison, Typage. Calcul algébrique. Définitions diagrammatiques.
Déterminisme. Confluence. Preuves par récurrence.
Cours 2 (4-10) - Fondements du calcul fonctionnel.
Fonction et algorithme. La lambda-notation.
Indices de liaison et conversion de renommage. Substitution.
Réduction. Stratégies de calcul. Conversion.
Cours 3 (11-10) - Récursivité. Récursion primitive et itération.
Programmation fonctionnelle pure. Hiérarchies de types.
Cours 4 (18-10) - Résidus. Confluence de la réduction fonctionnelle.
Théorème de Church et Rosser. Finitude des résidus. Standardisation.
Cours 5 (25-10) - Extensionalité. Séparabilité. Arbres de Böhm.
Modèles du lambda calcul.
Les cours ont lieu le lieu salle 0D9 (sauf le cours 1 en 0D4),
175 rue du Chevaleret, Paris XIII.
Gerard.Huet@inria.fr
Dernière révision : 22 Septembre 2004