Επόμενη: Η Αρχή της Ανάλυσης Πάνω Επίπεδο: Ανάλυση Προηγούμενη: Αντικατάσταση

4.4 Ενοποίηση

Ονομάζουμε ενοποίηση (unification) τη διαδικασία που απαιτείται για να γίνουν δύο εκφράσεις όμοιες, με χρήση αντικαταστάσεων. Για δύο εκφράσεις E₁ και E₂, o ενοποιητής (unifier) τους, είναι μια αντικατάσταση , τέτοια ώστε η έκφραση να είναι συντακτικά όμοια με την . Αν υπάρχει μια τέτοια αντικατάσταση , θα λέμε ότι οι εκφράσεις E₁, E₂ είναι ενοποιήσιμες (unifiable).

Για παράδειγμα, η αντικατάσταση είναι ένας ενοποιητής για τις εκφράσεις και , αφού μετά την εφαρμογή της παίρνουμε .

Αν η είναι ένας ενοποιητής για ένα σύνολο εκφράσεων και αν για κάθε ενοποιητή του υπάρχει μια αντικατάσταση τέτοια, ώστε , τότε η ονομάζεται γενικότερος ταυτοποιητής - mgu (most general unifier) για το . Για παράδειγμα, αν

τότε η αντικατάσταση

είναι ένας mgu για το , ενώ η αντικατάσταση

είναι ενοποιητής για το αλλά όχι και mgu , διότι δεν υπάρχει αντικατάσταση με

Αξίζει να παρατηρηθεί ότι υπάρχει αλγόριθμος, τέτοιος ώστε αν ένα πεπερασμένο σύνολο τύπων είναι ενοποιήσιμο, να τερματίζει και να επιστρέφει τον mgu του . Αν πάλι δεν υπάρχει, τότε τερματίζει κι αναφέρει ότι το δεν είναι ενοποιήσιμο.