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

De AgregmathKL
Aller à : navigation, rechercher
 
(Une révision intermédiaire par un autre utilisateur non affichée)
Ligne 1 : Ligne 1 :
−
== Plans scannés ==
+
= Plans =
  
−
*2012-2013 [[Fichier:Pdf.png|alt=Pdf|link=|24px]] [[Média:919_2012-2013.pdf|919 Unification : algorithmes et applications.]]
+
[[Fichier:Pdf.png|alt=Pdf|link=|24px]] [[Média:919_2012-2013.pdf|Plan détaillé de l'année 2012-2013]]
−
*2013-2014 [[Fichier:Pdf.png|alt=Pdf|link=|24px]] [[Média:919_2013-2014.pdf|919 Unification : algorithmes et applications.]]
+
−
*2014-2015 [[Fichier:Pdf.png|alt=Pdf|link=|24px]] [[Média:919_2014-2015.pdf|919 Unification : algorithmes et applications.]]
+
−
*2015-2016 [[Fichier:Pdf.png|alt=Pdf|link=|24px]] [[Média:919_2015-2016.pdf|919 Unification : algorithmes et applications.]]
+
  
 +
[[Fichier:Pdf.png|alt=Pdf|link=|24px]] [[Média:919_2013-2014.pdf|Plan détaillé de l'année 2013-2014]]
  
−
== Développements ==
+
[[Fichier:Pdf.png|alt=Pdf|link=|24px]] [[Média:919_2014-2015.pdf|Plan détaillé de l'année 2014-2015]]
−
<DynamicPageList>
+
 
−
category            = Développement de la leçon 919
+
[[Fichier:Pdf.png|alt=Pdf|link=|24px]] [[Média:919_2015-2016.pdf|Plan détaillé de l'année 2015-2016]]
−
</DynamicPageList>
+
  
−
= Plan Basile et Kévin (2012) =
+
== 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 20 : Ligne 17 :
 
<math>\;\texttt{ |\ a::l\ ->\ (fun\ y\ ->\ a::y::l )}</math>
 
<math>\;\texttt{ |\ a::l\ ->\ (fun\ y\ ->\ a::y::l )}</math>
  
−
=== I - Unification ===
+
==== 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 33 : 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 39 : 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 46 : Ligne 42 :
 
* Problème de correspondance/filtrage.
 
* Problème de correspondance/filtrage.
  
−
=== II - Algorithmes ===
+
==== Algorithmes ====
 
# Naïf
 
# Naïf
 
#* Celui de Stern
 
#* Celui de Stern
Ligne 54 : Ligne 50 :
 
#** Developpement : [[Algorithme d'unification]]
 
#** Developpement : [[Algorithme d'unification]]
  
−
=== III - Applications ===
+
==== Applications ====
−
==== Réécriture ====
+
===== Réécriture =====
 
* Definitions SRT
 
* Definitions SRT
 
* Confluence locale
 
* Confluence locale
Ligne 61 : 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 Possibles ==
 
−
=== Proposés ===
 
−
* [[Complétude de la méthode de résolution]]
 
−
* [[Algorithme d'unification]]
 
  
−
=== Possibles ===
+
= 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 ==
+
 
 +
= 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

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 »