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.

I - Unification

Langage du premier ordre et termes.

On se donne une famille d'ensemble de symboles de fonctions (dits d'arité ) : pour . On pose . Et on considère un ensemble infini de symboles de variables.

  • Definition -algèbre : ensemble + interpréation pour tous les symboles de fonctions.
  • Definition ensemble des termes à variable dans par induction.
  • C'est une -algèbre.
  • Les termes clos sont les éléments de .
  • 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