919 -- Unification : algorithmes et applications. : Différence entre versions
De AgregmathKL
m (→Plan Basile et Kévin (2012)) |
(→Plan Basile et Kévin (2012)) |
||
Ligne 12 : | Ligne 12 : | ||
=== I - Unification === | === I - Unification === | ||
− | + | ||
− | + | ==== Langage du premier ordre et termes. ==== | |
− | + | On se donne une famille d'ensemble de '''symboles de fonctions''' (dits d''''arité''' <math>n</math>) : <math>\mathcal{F}_n</math> pour <math>n \in \mathbb{N}.</math>. | |
− | + | On pose <math>\mathcal{F} = \cup_n \mathcal{F}_n</math>. | |
− | + | Et on considère un ensemble infini <math>X</math> de '''symboles de variables'''. | |
− | + | * Definition <math>\mathcal{F}</math>-algèbre : ensemble + interpréation pour tous les symboles de fonctions. | |
− | + | * Definition <math>T(X)</math> ensemble des '''termes''' à variable dans <math>X</math> par induction. | |
+ | * C'est une <math>\mathcal{F}</math>-algèbre. | ||
+ | * Les '''termes clos''' sont les éléments de <math>T(\emptyset)</math>. | ||
+ | * 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 === | === II - Algorithmes === | ||
Ligne 26 : | Ligne 43 : | ||
# Evolué | # Evolué | ||
#* Union-find et termes en DAG (AllThat) | #* Union-find et termes en DAG (AllThat) | ||
+ | #** Developpement : [[Algorithme d'unification]] | ||
=== III - Applications === | === 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 | ||
+ | |||
+ | ==== Typage et filtrage ==== | ||
Version du 3 juin 2012 à 11:59
"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.
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
- Naïf
- Celui de Stern
- Celui de AllThat (si différent)
- Evolué
- Union-find et termes en DAG (AllThat)
- Developpement : Algorithme d'unification
- Union-find et termes en DAG (AllThat)
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
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