L'Unification par la transformation

Question

Je suis en train d'écrire un l'unification algorithme en F# pour une utilisation avec AST les transformations à l'aide de "La Réécriture de termes et de Tout ce Qui" (WoldCat) par Franz Baader et Tobias Nipkow.Pour la section 4.6 de l'Unification par la transformation, il avait trop de mathématiques de la théorie avec des exemples, et pas aussi clair que je l'aurais aimé.

Quelqu'un peut-il donner ou point de plus simple exemples qui rendent l'utilisation de transformations:

Supprimer, De Les Décomposer, Les Orienter, De Les Éliminer.

Answer 1

Supprimer: t = t est inutile et peut être retiré de l'ensemble des équations.

1 =? 1 -> nil

Orient:Nous voulons que toutes les équations sous la forme de x =? t, alors lance des équations sous la forme de t =? x.

2 =? x1 -> x1 =? 2

Éliminer:Compte tenu de x =? t, changement de toutes les autres équations pour remplacer toutes les occurrences de x avec t.

x1 + x2 = 7, x2 = 5 -> x1 + 5 = 7, x2 = 5

Décomposer:Nous avons besoin de prendre de fonctions et de les éliminer pour obtenir les équations sous la forme de x =? t.Notez que ce processus techniquement supprime uniquement une fonction à la fois.

x1 + 5 = 7 -> x1 = 2
2 * (x1 + x2) = 14 -> x1 + x2 = 7

Espérons que cela aide.