Recherchez sur tout Techno-Science.net
       
Techno-Science.net : Suivez l'actualité des sciences et des technologies, découvrez, commentez
Catégories
Techniques
Sciences
Encore plus...
Techno-Science.net
Bons plans et avis Gearbest: Xiaomi Mi Mix2, OnePlus 5T
Code promo Gearbest: réduction, coupon, livraison...
Photo Mystérieuse

Que représente
cette image ?
 A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | +
Unification

Introduction

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 (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.) de deux termes t1 et t2 consiste à trouver (quand il en existe) un troisième terme t tel qu'on puisse passer (Le genre Passer a été créé par le zoologiste français Mathurin Jacques Brisson (1723-1806) en 1760.) 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 (En mathématiques et en logique, une variable est représentée par un symbole. Elle est utilisée pour marquer un rôle dans une formule, un prédicat ou un algorithme. En statistiques, une...) 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 (Un atome (du grec ατομος, atomos, « que l'on ne peut diviser ») est la plus petite partie d'un corps simple pouvant se combiner chimiquement avec une autre. Il est...) et représentera dorénavant ce terme ou atome ;
  3. un atome (Un atome (grec ancien ἄτομος [atomos], « que l'on ne peut diviser ») est la plus petite partie d'un corps simple pouvant se...) 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 (La joue est la partie du visage qui recouvre la cavité buccale, fermée par les mâchoires. On appelle aussi joue le muscle qui sert principalement à ouvrir et fermer la bouche et à mastiquer.) (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 (En géographie, la situation est un concept spatial permettant la localisation relative d'un espace par rapport à son environnement proche ou non. Il inscrit un lieu dans un cadre...) 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 (La notion de nombre en linguistique est traitée à l’article « Nombre grammatical ».) 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

Wiktprintable without text.svg

Voir « unification » sur le Wiktionnaire.

Source: Wikipédia publiée sous licence CC-BY-SA 3.0. Vous pouvez soumettre une modification à cette définition sur cette page.

La liste des auteurs de cet article est disponible ici.