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