919 -- Unification : algorithmes et applications. : Différence entre versions

De AgregmathKL
Aller à : navigation, rechercher
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.
+
 
−
# Substitutions
+
==== Langage du premier ordre et termes. ====
−
#* Definition, exemples
+
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>.
−
#* Autre chose
+
On pose <math>\mathcal{F} = \cup_n \mathcal{F}_n</math>.
−
# Unification
+
Et on considère un ensemble infini <math>X</math> de '''symboles de variables'''.
−
#* Definition exemple
+
* Definition <math>\mathcal{F}</math>-algèbre : ensemble + interpréation pour tous les symboles de fonctions.
−
#* Unificateur principal
+
* 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
+
==== Réécriture ====
−
#* Definitions
+
* Definitions SRT
−
#* Confluence locale
+
* Confluence locale
−
#** Developpement : [[Lemme des paires critiques]] (AllThat)
+
** Lemme de Newman
−
# Logique
+
** Developpement : [[Lemme des paires critiques]] (AllThat)
−
#* Méthode de résolution
+
 
−
#** Developpement : [[Complétude de la méthode de résolution]] (Stern)
+
==== Logique ====
−
#* Le langage Prolog
+
* Méthode de résolution
−
# Typage
+
** 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.

{\texttt {let\ f\ =\ function}} \;{\texttt {|\ []\ ->\ (fun\ y\ ->\ [y])}} \;{\texttt {|\ a::l\ ->\ (fun\ y\ ->\ a::y::l)}}

I - Unification

Langage du premier ordre et termes.

On se donne une famille d'ensemble de symboles de fonctions (dits d'arité n) : {\mathcal {F}}_{n} pour n\in {\mathbb {N}}.. On pose {\mathcal {F}}=\cup _{n}{\mathcal {F}}_{n}. Et on considère un ensemble infini X de symboles de variables.

  • Definition {\mathcal {F}}-algèbre : ensemble + interpréation pour tous les symboles de fonctions.
  • Definition T(X) ensemble des termes à variable dans X par induction.
  • C'est une {\mathcal {F}}-algèbre.
  • Les termes clos sont les éléments de T(\emptyset ).
  • 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
Récupérée de « https://minerve.ens-rennes.fr/index.php?title=919_--_Unification_:_algorithmes_et_applications.&oldid=647 »