919 -- Unification : algorithmes et applications.

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.

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

Unification

Langage du premier ordre et termes.

On se donne une famille d'ensemble de symboles de fonctions (dits d'arité $n$) : ${\mathcal {F}}_{n}$ pour $n\in {\mathbb {N}}.$. On pose ${\mathcal {F}}=\cup _{n}{\mathcal {F}}_{n}$. Et on considère un ensemble infini $X$ de symboles de variables.

• Definition ${\mathcal {F}}$-algèbre : ensemble + interpréation pour tous les symboles de fonctions.
• Definition $T(X)$ ensemble des termes à variable dans $X$ par induction.
• C'est une ${\mathcal {F}}$-algèbre.
• Les termes clos sont les éléments de $T(\emptyset )$.
• 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

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

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

Développements

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

Autres

• 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