Sont ces exemples de problèmes d'unification?

Question

J'ai étudié l'unification, en particulier l'unification nominale (papier) attire mon attention. J'ai lu la théorie et les exemples. Mais je me demande quel type de problèmes se produit dans les unifications. Pour les exemples, les exemples suivants proviennent du papier d'unification nominal. (J'écris des variables liées distinctes, donc plus facile à voir les solutions)

(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) $

J'ai observé que chaque variable ($ x $ ou $ y $) ne se produit qu'une seule fois d'un côté des équations. Devrait-il être toujours ainsi? Puis-je écrire ce qui suit

(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) $

Et sont-ils des problèmes d'unification possibles?

J'ai lu de nombreuses sources, mais et tous les problèmes d'unification présentés avec des variables n'ont qu'une seule fois d'occurrences d'un côté des équations. J'ai essayé de trouver plus d'exemples, mais je n'ai rien trouvé de différent.

Je sais que les problèmes d'unification découlent de la programmation logique. Et jusqu'à présent, je n'ai vu aucun programme logique qui met $ x $ deux fois dans un terme.

Quoi qu'il en soit, espérant que quelqu'un clarifie ces points.

Merci d'avance!