919 -- Unification : algorithmes et applications. : Différence entre versions
De AgregmathKL
(leçon dans une semaine !) |
m (→Développements Possibles) |
||
| Ligne 38 : | Ligne 38 : | ||
=== Proposés === | === Proposés === | ||
* [[Complétude de la méthode de résolution]] | * [[Complétude de la méthode de résolution]] | ||
| − | * [[ | + | * [[Algorithme d'unification]] |
=== Possibles === | === Possibles === | ||
| − | * [[ | + | * [[Lemme des paires critiques]] |
* [[Cas particuliers dans la compression de Knuth-Bendix]] | * [[Cas particuliers dans la compression de Knuth-Bendix]] | ||
Version du 1 juin 2012 à 19:13
"Rien"
Le jury (s'il était unifié à {LMB}).
Sommaire
Plan Basile et Kévin (2012)
Le plan
Intro : motivation de l'intérêt de l'unification pour le typage. Exemple avec Ocaml.
I - Unification
- Langage du premier ordre et termes.
- Substitutions
- Definition, exemples
- Autre chose
- Unification
- Definition exemple
- Unificateur principal
II - Algorithmes
- Naïf
- Celui de Stern
- Celui de AllThat (si différent)
- Evolué
- Union-find et termes en DAG (AllThat)
III - Applications
- Réécriture
- Definitions
- Confluence locale
- 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
- Méthode de résolution
- Typage
Développements Possibles
Proposés
Possibles
Références
- Baader, Nipkow : Term Rewriting and All That
- J. Stern : Fondements mathématiques de l'informatique
- Weis, Leroy : Le langage Caml
