Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur Graph Search.
Concept
Unification
Résumé
vignette|Unifier deux termes, c'est les rendre identiques en remplaçant les variables.
En informatique et en logique, l'unification est un processus algorithmique qui, étant donnés deux termes, trouve une substitution qui appliquée aux deux termes les rend identiques. Par exemple, et peuvent être rendus identiques par la substitution et , qui donne quand on l'applique à chacun de ces termes le terme . Dit autrement, l'unification est la résolution d'une équation dans l'algèbre des termes (unification syntaxique) ou dans une algèbre quotient par un ensemble d'identités (unification modulo une théorie) ; la solution de l'équation est la substitution qui rend les deux termes identiques et que l'on appelle l'unificateur.
L'unification a des applications en inférence de types, programmation logique, en démonstration automatique de théorèmes, en système de réécriture, en traitement du langage naturel.
Souvent, on s'intéresse à l'unification syntaxique où il faut que les termes obtenus par application de l'unificateur soient syntaxiquement égaux, comme dans l'exemple ci-dessus. Par exemple, le problème d'unification syntaxique ayant pour données et n'a pas de solution. Le filtrage par motif (ou pattern matching) est une restriction de l'unification où l'unificateur n'est appliquée qu'à un seul des deux termes. Par exemple, et sont rendus égaux par la substitution .
La fin de l'article présente aussi l'unification modulo une théorie, qui est le cas où on dispose de connaissances supplémentaires sur les fonctions (par exemple, est commutatif).
vignette|John Alan Robinson, considéré comme le fondateur de l'unification.
Le premier chercheur à évoquer un algorithme d'unification est Jacques Herbrand dans sa thèse en 1930. Il s'agit d'un algorithme non-déterministe pour unifier deux termes. Herbrand était intéressé par la résolution d'équations. En 1960, Prawitz et Voghera ont généralisé le calcul propositionnel à des formules du premier ordre non instanciées, ou tout au moins en les instanciant a minima.
Source officielle
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.