Questi esempi di problemi di unificazione?

Question

Ho studiato unificazione, in particolare l'unificazione nominale (carta) riceve la mia attenzione. Ho letto la teoria e gli esempi. Ma mi chiedo che che tipo di problemi si verifichino nelle unificazioni. Per esempi, i seguenti esempi provengono da documenti di unificazione nominale. (Scrivo variabili limitate distinte, così più facile vedere le soluzioni)

(1) $ lambda a. lambda b. (X , b) = lambda c. lambda d. (d , x) $

(2) $ lambda a. lambda b. (X , b) = lambda c. lambda d. (d , y) $

(3) $ lambda a. lambda b. (B , x) = lambda c. lambda d. (d , y) $

Ho osservato che ogni variabile ($ x $ o $ y $) si verifica solo una volta su un lato delle equazioni. Dovrebbe essere sempre così? Posso scrivere quanto segue

(4) $ lambda a. lambda b. (X , x) = lambda c. lambda d. (d , x) $

(5) $ lambda a. lambda b. (Y , x) = lambda c. lambda d. (d , x) $

(6) $ lambda a. lambda b. (X , x) = lambda c. lambda d. (X , x) $

E questi possibili problemi di unificazione?

Ho letto molte fonti, ma tutti i problemi di unificazione presentati con variabili hanno solo una volta eventi da un lato delle equazioni. Ho cercato di trovare altri esempi, ma non sono riuscito a trovare nulla di diverso.

So che i problemi di unificazione derivano dalla programmazione logica. E finora non ho visto programmi logici che mettono $ x $ due volte in un termine.

Comunque, sperando che qualcuno chiarisca questi punti.

Grazie in anticipo!