Réécriture et lambda-calcul (année 2005-2006)

Ce cours est assuré par Pierre Lescanne assisté de Christoph Lauter et Damien Pous.

J'utilise la vidéoprojection.

Ce cours garde le nom de réécriture, mais en fait, en transition vers un cours de L3 qui s'appelera PROG-2, il comporte la présentation de concepts fondamentaux liés à la programmation, à savoir les bases de la sémantique et les bases de la réécriture.

Il commence par la présentation des trois types de sémantique (opérationnelle, dénotationnelle et axiomatique), puis par la présentation des trois sémantique d'un petit langage appelé IMP.

Il continue par une introduction à la récriture.

• une introduction,
• des rappels sur les relations abstraites,
• la définition des termes
• l'unification
• la complétion
• la ordre sur les preuves
• la terminaison
• éléments de sémantique opérationnelle

Réécriture et lambda-calcul (année 2004-2005)

Dans ce cours nous aborderons les principaux concepts des systèmes de réécriture du premier ordre et un peu d'ordre supérieur (unification).

Ce module se compose de 32 heures de cours assurés par Pierre Lescanne et de 32 heures de travaux dirigés assurés par Romain Kervarc. Cette page évoluera avec l'avancement du cours et servira de lien avec les étudiants. Elle complète la liste d'envoi mim.reecriture@listes.ens-lyon.fr, qui permet de faire le lien entre les étudiants.

Ce cours s'appuie essentiellement sur le livre de Franz Baader et Tobias Nipkow Term Rewriting and All That. Cambridge University Press, 1998 que nous appellerons le All that, mais que je présente à ma manière. Pour les compléments sur le lambda calcul, je recommande le livre de Chris Hankin Lambda Calculi: a Guide for Computer Scientists, Oxford U. Press, 1994. Pour l'unification on pourra consulter Wayne Snyder, A proof theory for general unification, Birkhäuser, (1991), Vol 11, Series Progress in computer science and applied logic. Deux bons livres sur la réécriture sont Enno Ohlebusch Advanced Topics in Term Rewriting Springer-Verlag, (2002) et Terese, Term Rewriting Systems, Cambridge University Press, (2003), vol. 55, serie Cambridge Tracts in Theoretical Computer Science.

Voici les différents cours (voir aussi ici) sous formes de transparents en PostScript et en PDF.  Les sources LaTeX sont fournis (voir les répertoire OUTILS pour y trouver les fichiers spécifiques que j'utilise). En général, ces documents sont susceptibles d'évoluer légèrement (quelques fois profondément).  Vérifiez la date de votre version.

Le cours

• introduction ((source, PDF)
• reductions abstraites (source, PDF),
• termes (source, PDF),
• terminaison (source, PDF),
• unification (source, PDF),
• autres algorithmes d'unification (source, PDF, notes de cours) : par combinaison, associative et commutative, d'ordre supérieur.
• completion (source, PDF)
• ordre sur les preuves (source, PDF)
• bases de Gröbner (source, PDF)
• résolution (source, PDF)

Les exercices

Examen final

Compléments (2003)

Quelques excursions

• A propos de Newman, je vous invite à lire deux lettres d'Alan Turing à sa mère (1, 2).
• J'ai présenté le dixième problème de Hilbert, mais concernant les problèmes de Hilbert et plus précisément le seizième, assistez virtuellement à la conférence d'Étienne Ghys. Vous verrez aussi que la notion de vérité chez les mathématiciens est un concept plus social et plus complexe que ce qu'un cours lié à la déduction automatique pourrait faire croire! Un sujet à méditer et à débattre.
• Voici quelques références intéressantes (Leipzig, Alberta, Lyon, , la vie de Post) au problème de correspondance de Post qui vous conduiront à MC Solaar.
• Lisez une discussion intéressante par Marc Bezem et Thierry Coquand sur la démonstration du lemme de Newman.
• A propos de l'histoire de la procédure de Knuth et Bendix on pourra lire l'article de Knuth All Questions Answered.
• Voici une surprenante application de la réécriture

En 2001-2002

Les exercices

Voici les fiches d'exercices de Silvia Ghilezan(1, 2, 3, 4, 5, 6, 7, 8, 9) et le sujet du partiel (source et version tty).

En 2000-2001

• Dans la question 1. certains concluent que si un terme n'est pas de la forme s^k(0) alors il est de la forme n1 + n2 ou d(n) ou c(n).
• Dans les questions 3. et 4. les inégalités doivent être strictes.

Il y a eu aussi un examen avec son corrigé.