919 -- Unification : algorithmes et applications.

"Rien"

Le jury (s'il était unifié à {LMB}).

Plan Basile et Kévin (2012)

Le plan

Intro : motivation de l'intérêt de l'unification pour le typage. Exemple avec Ocaml.

${\texttt {let\ f\ =\ function}}$ $\;{\texttt {|\ []\ ->\ (fun\ y\ ->\ [y])}}$ $\;{\texttt {|\ a::l\ ->\ (fun\ y\ ->\ a::y::l)}}$

I - Unification

1. Langage du premier ordre et termes.
2. Substitutions
   • Definition, exemples
   • Autre chose
3. Unification
   • Definition exemple
   • Unificateur principal

II - Algorithmes

1. Naïf
   • Celui de Stern
   • Celui de AllThat (si différent)
2. Evolué
   • Union-find et termes en DAG (AllThat)

III - Applications

1. Réécriture
   • Definitions
   • Confluence locale
     • Developpement : Lemme des paires critiques (AllThat)
2. Logique
   • Méthode de résolution
     • Developpement : Complétude de la méthode de résolution (Stern)
   • Le langage Prolog
3. Typage

Développements Possibles

Proposés

• Complétude de la méthode de résolution
• Algorithme d'unification

Possibles

• Lemme des paires critiques
• Cas particuliers dans la compression de Knuth-Bendix

Références

• Baader, Nipkow : Term Rewriting and All That
• J. Stern : Fondements mathématiques de l'informatique
• Weis, Leroy : Le langage Caml