919 -- Unification : algorithmes et applications.

De AgregmathKL
Aller à : navigation, rechercher

Plans scannés


Développements


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é

III - Applications

Réécriture

Logique

Typage et filtrage

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