Unification (logique)

Unification (logique)

Unification

Wiktprintable without text.svg

Voir « unification » sur le Wiktionnaire.

Page d'aide sur l'homonymie Pour les articles homonymes, voir Unification (homonymie).

Le concept d'unification est une notion centrale de la logique des prédicats ainsi que d'autres systèmes de logique et est sans doute ce qui distingue le plus Prolog des autres langages de programmation.

L'unification de deux termes t1 et t2 consiste à trouver (quand il en existe) un troisième terme t tel qu'on puisse passer de t à t1 et à t2 en instanciant certaines variables. t est alors appelé un unificateur de t1 et t2. Intuitivement, l'unification est le fait d'attribuer une valeur à certaines variables de t1 et t2 et peut être regardé comme un genre d'assignation qui ne pourrait s'effectuer qu'une seule fois. Lorsqu'on résout une équation algébrique, une inconnue peut avoir une, plusieurs ou aucune solutions, mais sa valeur ne change pas durant les opérations; c'est pareil pour l'unification. En fait on peut voir la résolution d'une équation comme un cas particulier d'unification.

En prolog, cette opération est dénotée par symbole « = ». Les règles de l'unification sont les suivantes:

  1. une variable X non-instanciée (c'est-à-dire ne possédant pas encore de valeur) peut être unifiée avec une autre variable (instanciée ou pas); les deux variables deviennent alors simplement des synonymes l'une de l'autre et représenteront dorénavant la même chose ;
  2. une variable X non-instanciée peut être unifiée avec un terme ou un atome et représentera dorénavant ce terme ou atome ;
  3. un atome peut être unifié seulement avec le même atome ;
  4. un terme peut être unifié avec un autre terme : si leurs noms sont identiques, si leur nombres d'arguments sont identiques et si chacun des arguments du premier terme est (récursivement) unifiable avec l'argument correspondant du second terme.

En raison de sa nature déclarative, l'ordre dans une suite d'unifications ne joue (habituellement) aucun rôle.

Unification et logique d'ordre supérieur

Lorsqu'on raisonne en logique du premier ordre, où les variables ne peuvent être unifiées qu'à des constantes, les choses se passent bien: savoir si deux termes t1 et t2 sont unifiables est décidable (grâce par exemple à l'algorithme ci-dessus). De plus, s'ils le sont, il existe un unificateur le plus général (most general unifier ou mgu en anglais), c'est-à-dire un terme t tel que tous les autres unificateurs de t1 et t2 soient dérivables par instantiation de variables de t.

Cette situation idéale ne se retrouve hélas pas dans tous les systèmes logiques. En particulier, si on se place en logique d'ordre supérieur, c'est-à-dire qu'on s'autorise à utiliser des variables comme symboles de fonction ou comme prédicats, on perd la décidabilité et l'unicité de l'unificateur quand il existe. Au pire, deux termes peuvent même avoir une infinité d'unificateurs tous différents.

Exemples d'unification en prolog

On supposera que toutes les variables (en majuscules) sont non-instanciées.

A = A
réussit (tautologie)
A = B, B = abc
A et B sont unifiés avec l'atome 'abc'
xyz = C, C = D
réussit: l'unification est symétrique
abc = abc
réussit: les atomes sont identiques
abc = xyz
échoue: des atomes distincts ne s'unifient pas
f(A) = f(B)
réussit: A est unifié avec B
f(A) = g(B)
échoue: les termes ont des noms différents
f(A) = f(B, C)
échoue: les termes ont un nombre d'arguments différents
f(g(A)) = f(B)
réussit: B est unifié au terme g(A)
f(g(A), A) = f(B, xyz)
réussit: B est unifié au terme g(xyz) et A est unifié à l'atome 'xyz'
A = f(A)
l'unification est infinie: A est unifié au terme f(f(f(f(f(...)))). Suivant le système logique que l'on souhaite on peut considérer que l'unification échoue ou réussit; la plupart de ces systèmes considèrent que l'unification échoue.
A = abc, xyz = X, A = X
échoue: car abc=xyz échoue
  • Portail de la logique Portail de la logique
  • Portail des mathématiques Portail des mathématiques
Ce document provient de « Unification ».

Wikimedia Foundation. 2010.

Contenu soumis à la licence CC-BY-SA. Source : Article Unification (logique) de Wikipédia en français (auteurs)

Игры ⚽ Поможем написать реферат

Regardez d'autres dictionnaires:

  • Unification — Pour les articles homonymes, voir Unification (homonymie). Le concept d unification est une notion centrale de la logique des prédicats ainsi que d autres systèmes de logique et est sans doute ce qui distingue le plus Prolog des autres langages… …   Wikipédia en Français

  • Unification (homonymie) — Cette page d’homonymie répertorie les différents sujets et articles partageant un même nom. Sur les autres projets Wikimedia : « Unification (homonymie) », sur le Wiktionnaire (dictionnaire universel) Unification est un nom commun… …   Wikipédia en Français

  • Logique mathématique — La logique mathématique, ou logique formelle, est une discipline des mathématiques introduite à la fin du XIXe siècle et qui s est donnée comme objet l étude des mathématiques en tant que langage. Les objets fondamentaux de la logique… …   Wikipédia en Français

  • MATHÉMATIQUES , DE LA DIVERSITÉ À L’UNIFICATION — «Ce que nous appelons la réalité objective, c’est, en dernière analyse, ce qui est commun à plusieurs êtres pensants, et pourrait être commun à tous; cette partie commune [...], ce ne peut être que l’harmonie exprimée par des lois mathématiques.» …   Encyclopédie Universelle

  • Programmation logique — La programmation logique est une forme de programmation qui définit les applications à l aide d un ensemble de faits élémentaires les concernant et de règles de logique leur associant des conséquences plus ou moins directes. Ces faits et ces… …   Wikipédia en Français

  • Histoire De La Logique — L histoire de la logique, en Occident, prend ses racines dans la philosophie et les mathématiques de la Grèce antique pour se développer en richesse au XXe siècle. Des développements parallèles ont notamment eu lieu en Chine et en… …   Wikipédia en Français

  • Histoire de la logique — L histoire de la logique, en Occident, prend ses racines dans la philosophie et les mathématiques de la Grèce antique pour se développer en richesse au XXe siècle. Des développements parallèles ont notamment eu lieu en Chine et en… …   Wikipédia en Français

  • Grande Unification — Pour les articles homonymes, voir GUT. En physique théorique, une théorie de grande unification, encore appelée GUT (pour Grand Unified Theory en anglais) désigne un modèle étendant le modèle standard de la physique des particules dans lequel… …   Wikipédia en Français

  • Théorie de grande unification — Grande unification Pour les articles homonymes, voir GUT. En physique théorique, une théorie de grande unification, encore appelée GUT (pour Grand Unified Theory en anglais) désigne un modèle étendant le modèle standard de la physique des… …   Wikipédia en Français

  • Théorie de la grande unification — Grande unification Pour les articles homonymes, voir GUT. En physique théorique, une théorie de grande unification, encore appelée GUT (pour Grand Unified Theory en anglais) désigne un modèle étendant le modèle standard de la physique des… …   Wikipédia en Français

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”