In Prolog - Programmierung für künstliche Intelligenz sagt Bratko Folgendes auf Seite 58.

"Matching in Prolog entspricht der sogenannten Vereinheitlichung in der Logik. Wir vermeiden jedoch das Wort Unification, da Matching aus Effizienzgründen in den meisten Prolog-Systemen auf eine Weise implementiert wird, die nicht genau der Vereinheitlichung entspricht sogenannter vorkomme-check: Tritt eine gegebene Variable in einem gegebenen Term auf? Der vorkomme-check würde den Abgleich ineffizient machen. "

Meine Frage ist, ob die Vereinigung in miniKanren diesen Effizienzverlust erleidet oder wie dieses Problem gelöst wird.