Réécriture et lambda-calcul
Cours de base (30 h de cours, 30h de TD)
Cours : Pierre Lescanne (Pierre.Lescanne)
TD : Daniel Hirschkoff (Daniel.Hirschkoff)
Présentation
La réécriture est une technique qui permet de modéliser les concepts
de réduction et de simplification. Elle sert de fondement au calcul
symbolique et à la sémantique opérationnelle de langages de
programmation notamment fonctionnel.
Dans ce cours nous aborderons les principaux concepts des systèmes de
réécriture du premier ordre et d'ordre supérieur (l-calcul) :
-
confluence,
- terminaison,
- unification,
- complétion.
Plan
Nous aborderons le thèmes suivants.
- Motivations et exemples,
- Unification,
- Confluence et théorème de Knuth-Bendix,
- Terminaison,
- Complétion,
- Présentation du l-calcul,
- Types et forte normalisation (c-à-d terminaison en l-calcul),
- Calculabilité et points fixes,
- l-calcul et système du premier ordre (logique
combinatoire et substitutions explicites)
Bibliographie
-
Hankin; Lambda Calculi: a Guide for Computer Scientists,
Oxford U. Press, 1994.
- F. Baader et T. Nipkow. Term Rewriting and All That.
Cambridge University Press, 1998.