919 -- Unification : algorithmes et applications.
De AgregmathKL
Sommaire
Plans
Plan détaillé de l'année 2012-2013
Plan détaillé de l'année 2013-2014
Plan détaillé de l'année 2014-2015
Plan détaillé de l'année 2015-2016
Autre Plan (Basile et Kévin, 2012)
Le plan
Intro : motivation de l'intérêt de l'unification pour le typage. Exemple avec Ocaml.
Unification
Langage du premier ordre et termes.
On se donne une famille d'ensemble de symboles de fonctions (dits d'arité ) : pour . On pose . Et on considère un ensemble infini de symboles de variables.
- Definition -algèbre : ensemble + interpréation pour tous les symboles de fonctions.
- Definition ensemble des termes à variable dans par induction.
- C'est une -algèbre.
- Les termes clos sont les éléments de .
- Définition annexes (par induction) : positions, variables.
- Exemple.
Substitutions
- Propriété universelle des termes clos, propriété universelle des termes (liberté).
- Corollaire définition : existence des substitutions.
- Définitions annexes : domaine, portée d'une substitutions.
- Exemple
Unification
- Problème d'unification. notation.
- Définition unificateur, ordre
- Unificateur principal
- Problème de correspondance/filtrage.
Algorithmes
- Naïf
- Celui de Stern
- Celui de AllThat (si différent)
- Evolué
- Union-find et termes en DAG (AllThat)
- Developpement : Algorithme d'unification
- Union-find et termes en DAG (AllThat)
Applications
Réécriture
- Definitions SRT
- Confluence locale
- Lemme de Newman
- Developpement : Lemme des paires critiques (AllThat)
Logique
- Méthode de résolution
- Developpement : Complétude de la méthode de résolution (Stern)
- Le langage Prolog
Typage et filtrage
Développements
Autres
Références
- Baader, Nipkow : Term Rewriting and All That
- J. Stern : Fondements mathématiques de l'informatique
- Weis, Leroy : Le langage Caml