Про унификацию.
В одной чистой реализации встраивания Пролога в Хаскель использовался чистый же алгоритм унификации, так называемый "Martelli-Montanari алгоритм".
Вот интересный комментарий по поводу этого алгоритма и алгоритма многих реализаций Пролога (использующих ссылки и изменение на месте):Moreover, Martelli-Montanari's algorithm, as well as all proposed unification _algorithms_ always terminates. Prolog's unification procedure does not necessarily terminate. But when it works it is usually much more efficient than, e.g., Martelli-Montanari, or Huet's or basically any other algorithm. A bit like the difference between applicative-order and normal-order in functional programming, really.
На этом тему чистых и не очень чистых реализаций Пролога (она когда-то случилась и я не могу ее найти) я для себя закрою.
Вот интересный комментарий по поводу этого алгоритма и алгоритма многих реализаций Пролога (использующих ссылки и изменение на месте):Moreover, Martelli-Montanari's algorithm, as well as all proposed unification _algorithms_ always terminates. Prolog's unification procedure does not necessarily terminate. But when it works it is usually much more efficient than, e.g., Martelli-Montanari, or Huet's or basically any other algorithm. A bit like the difference between applicative-order and normal-order in functional programming, really.
На этом тему чистых и не очень чистых реализаций Пролога (она когда-то случилась и я не могу ее найти) я для себя закрою.