919 -- Unification : algorithmes et applications. : Différence entre versions
De AgregmathKL
m (→Développements Possibles) |
m (→Plan Basile et Kévin (2012)) |
||
Ligne 6 : | Ligne 6 : | ||
== 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. | ||
+ | |||
+ | <math>\texttt{let\ f\ =\ function}</math> | ||
+ | <math>\;\texttt{ |\ []\ ->\ (fun\ y\ ->\ [y])}</math> | ||
+ | <math>\;\texttt{ |\ a::l\ ->\ (fun\ y\ ->\ a::y::l )}</math> | ||
=== I - Unification === | === I - Unification === |
Version du 1 juin 2012 à 21:38
"Rien"
Le jury (s'il était unifié à {LMB}).
Sommaire
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.
- Substitutions
- Definition, exemples
- Autre chose
- Unification
- Definition exemple
- Unificateur principal
II - Algorithmes
- Naïf
- Celui de Stern
- Celui de AllThat (si différent)
- Evolué
- Union-find et termes en DAG (AllThat)
III - Applications
- Réécriture
- Definitions
- Confluence locale
- 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
- Méthode de résolution
- Typage
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