919 -- Unification : algorithmes et applications.

Plans scannés

• 2012-2013 919 Unification : algorithmes et applications.
• 2013-2014 919 Unification : algorithmes et applications.
• 2014-2015 919 Unification : algorithmes et applications.
• 2015-2016 919 Unification : algorithmes et applications.

Développements

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

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

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.

II - 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

III - 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 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