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

De AgregmathKL
Aller à : navigation, rechercher
(leçon dans une semaine !)
 
 
(11 révisions intermédiaires par 5 utilisateurs non affichées)
Ligne 1 : Ligne 1 :
−
"Rien"
+
= Plans =
  
−
Le jury (s'il était unifié à {LMB}).
+
[[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 (2012) =
+
[[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.
  
−
=== I - Unification ===
+
<math>\texttt{let\ f\ =\ function}</math>
−
# Langage du premier ordre et termes.
+
<math>\;\texttt{ |\ []\ ->\ (fun\ y\ ->\ [y])}</math>
−
# Substitutions
+
<math>\;\texttt{ |\ a::l\ ->\ (fun\ y\ ->\ a::y::l )}</math>
−
#* Definition, exemples
+
−
#* Autre chose
+
−
# Unification
+
−
#* Definition exemple
+
−
#* Unificateur principal
+
  
−
=== II - Algorithmes ===
+
==== 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]]
  
−
=== III - Applications ===
+
==== 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)
+
−
#* Le langage Prolog
+
−
# Typage
+
  
 +
===== Logique =====
 +
* Méthode de résolution
 +
** Developpement : [[Complétude de la méthode de résolution]] (Stern)
 +
* Le langage Prolog
  
−
== Développements Possibles ==
+
===== Typage et filtrage =====
−
=== Proposés ===
+
−
* [[Complétude de la méthode de résolution]]
+
−
* [[Lemme des paires critiques]]
+
  
−
=== Possibles ===
+
 
−
* [[Algorithme d'unification]]
+
 
 +
= Développements =
 +
<DynamicPageList>
 +
category            = Développement de la leçon 919
 +
</DynamicPageList>
 +
== Autres ==
 +
* [[Lemme des paires critiques]]
 
* [[Cas particuliers dans la compression de Knuth-Bendix]]
 
* [[Cas particuliers dans la compression de Knuth-Bendix]]
  
−
== Références ==
+
 
 +
= 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

Plans

Pdf Plan détaillé de l'année 2012-2013

Pdf Plan détaillé de l'année 2013-2014

Pdf Plan détaillé de l'année 2014-2015

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.

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

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.

Algorithmes

  1. Naïf
    • Celui de Stern
    • Celui de AllThat (si différent)
  2. Evolué

Applications

Réécriture
Logique
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
Récupérée de « https://minerve.ens-rennes.fr/index.php?title=919_--_Unification_:_algorithmes_et_applications.&oldid=4818 »