919 -- Unification : algorithmes et applications. : Différence entre versions
De AgregmathKL
m (→Développements Possibles) |
|||
(10 révisions intermédiaires par 5 utilisateurs non affichées) | |||
Ligne 1 : | Ligne 1 : | ||
− | + | = Plans = | |
− | + | [[Fichier:Pdf.png|alt=Pdf|link=|24px]] [[Média:919_2012-2013.pdf|Plan détaillé de l'année 2012-2013]] | |
− | = Plan Basile et Kévin | + | [[Fichier:Pdf.png|alt=Pdf|link=|24px]] [[Média:919_2013-2014.pdf|Plan détaillé de l'année 2013-2014]] |
− | == Le plan == | + | |
+ | [[Fichier:Pdf.png|alt=Pdf|link=|24px]] [[Média:919_2014-2015.pdf|Plan détaillé de l'année 2014-2015]] | ||
+ | |||
+ | [[Fichier:Pdf.png|alt=Pdf|link=|24px]] [[Média:919_2015-2016.pdf|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. | Intro : motivation de l'intérêt de l'unification pour le typage. Exemple avec Ocaml. | ||
− | = | + | <math>\texttt{let\ f\ =\ function}</math> |
− | + | <math>\;\texttt{ |\ []\ ->\ (fun\ y\ ->\ [y])}</math> | |
− | + | <math>\;\texttt{ |\ a::l\ ->\ (fun\ y\ ->\ a::y::l )}</math> | |
− | + | ||
− | + | ||
− | + | ||
− | + | ||
− | + | ||
− | === | + | ==== 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. | ||
+ | |||
+ | ==== Algorithmes ==== | ||
# Naïf | # Naïf | ||
#* Celui de Stern | #* Celui de Stern | ||
Ligne 22 : | Ligne 48 : | ||
# Evolué | # Evolué | ||
#* Union-find et termes en DAG (AllThat) | #* 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 | ||
− | == | + | ===== Typage et filtrage ===== |
− | === | + | |
− | + | ||
− | + | ||
− | === | + | |
+ | |||
+ | = Développements = | ||
+ | <DynamicPageList> | ||
+ | category = Développement de la leçon 919 | ||
+ | </DynamicPageList> | ||
+ | == Autres == | ||
* [[Lemme des paires critiques]] | * [[Lemme des paires critiques]] | ||
* [[Cas particuliers dans la compression de Knuth-Bendix]] | * [[Cas particuliers dans la compression de Knuth-Bendix]] | ||
− | + | ||
+ | = Références = | ||
* Baader, Nipkow : Term Rewriting and All That | * Baader, Nipkow : Term Rewriting and All That | ||
* J. Stern : Fondements mathématiques de l'informatique | * J. Stern : Fondements mathématiques de l'informatique | ||
* Weis, Leroy : Le langage Caml | * Weis, Leroy : Le langage Caml | ||
+ | |||
+ | |||
+ | [[Category:Leçon d'informatique]] | ||
+ | [[Category:Anciennes leçons]] |
Version actuelle en date du 21 avril 2022 à 22:13
Sommaire
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.
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.
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)
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
Autres
Références
- Baader, Nipkow : Term Rewriting and All That
- J. Stern : Fondements mathématiques de l'informatique
- Weis, Leroy : Le langage Caml