919 -- Unification : algorithmes et applications. : Différence entre versions
De AgregmathKL
(2 révisions intermédiaires par 2 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]] | |
− | + | [[Fichier:Pdf.png|alt=Pdf|link=|24px]] [[Média:919_2013-2014.pdf|Plan détaillé de l'année 2013-2014]] | |
− | + | ||
− | + | ||
+ | [[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]] |
− | + | ||
− | + | ||
− | + | ||
− | = Plan Basile et Kévin | + | == Autre Plan (Basile et Kévin, 2012) == |
− | == Le plan == | + | === 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. | ||
Ligne 21 : | Ligne 17 : | ||
<math>\;\texttt{ |\ a::l\ ->\ (fun\ y\ ->\ a::y::l )}</math> | <math>\;\texttt{ |\ a::l\ ->\ (fun\ y\ ->\ a::y::l )}</math> | ||
− | === | + | ==== Unification ==== |
− | + | ===== Langage du premier ordre et termes. ===== | |
− | ==== 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 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>. | On pose <math>\mathcal{F} = \cup_n \mathcal{F}_n</math>. | ||
Ligne 34 : | Ligne 29 : | ||
* Exemple. | * Exemple. | ||
− | ==== Substitutions ==== | + | ===== Substitutions ===== |
* Propriété universelle des termes clos, propriété universelle des termes (liberté). | * Propriété universelle des termes clos, propriété universelle des termes (liberté). | ||
* Corollaire définition : existence des substitutions. | * Corollaire définition : existence des substitutions. | ||
Ligne 40 : | Ligne 35 : | ||
* Exemple | * Exemple | ||
− | ==== Unification ==== | + | ===== Unification ===== |
* Problème d'unification. notation. | * Problème d'unification. notation. | ||
* Définition unificateur, ordre | * Définition unificateur, ordre | ||
Ligne 47 : | Ligne 42 : | ||
* Problème de correspondance/filtrage. | * Problème de correspondance/filtrage. | ||
− | === | + | ==== Algorithmes ==== |
# Naïf | # Naïf | ||
#* Celui de Stern | #* Celui de Stern | ||
Ligne 55 : | Ligne 50 : | ||
#** Developpement : [[Algorithme d'unification]] | #** Developpement : [[Algorithme d'unification]] | ||
− | === | + | ==== Applications ==== |
− | ==== Réécriture ==== | + | ===== Réécriture ===== |
* Definitions SRT | * Definitions SRT | ||
* Confluence locale | * Confluence locale | ||
Ligne 62 : | Ligne 57 : | ||
** Developpement : [[Lemme des paires critiques]] (AllThat) | ** Developpement : [[Lemme des paires critiques]] (AllThat) | ||
− | ==== Logique ==== | + | ===== Logique ===== |
* Méthode de résolution | * Méthode de résolution | ||
** Developpement : [[Complétude de la méthode de résolution]] (Stern) | ** Developpement : [[Complétude de la méthode de résolution]] (Stern) | ||
* Le langage Prolog | * Le langage Prolog | ||
− | ==== Typage et filtrage ==== | + | ===== 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: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