Унификация по Робинсону

[vak]

Вынесу из комментов, где chaource предложил реализацию на Хаскеле.

В исходной статье Робинсона алгоритм звучит не особо ясно.

The following process, applicable to any finite nonempty set A of well-formed expressions, is called the Unification Algorithm:

• Step 1. Set σ₀ = ε and k = 0, and go to step 2.
• Step 2. If Aσₖ is not a singleton, go to step 3. Otherwise, set σ_A = σₖ, and terminate.
• Step 3. Let Vₖ be the earliest, and Uₖ the next earliest, in the lexical ordering of the disagreement set Bₖ of Aσₖ. If Vₖ is a variable, and does not occur in Uₖ, set σₖ₊₁ = σₖ {Uₖ / Vₖ}, add 1 to k, and return to step 2. Otherwise, terminate.

Переведём на современный язык.

Step 1. Initialization

• Start with a substitution σ₀​ = ∅.
• Let k = 0.
• Continue to Step 2.

Step 2. Check Whether Unification Is Complete

• Apply the current substitution σₖ to the entire set A, producing Aσₖ.
• If all resulting expressions in Aσₖ are identical, the algorithm stops and returns σₖ as the most general unifier.
• Otherwise proceed to Step 3.

Step 3. Find a Disagreement

• Identify the first position (in a left-to-right, top-down scan) where two expressions in Aσₖ differ.
• Let the disagreeing subexpressions be p and q.

Step 4. Process the Disagreement

Depending on the form of p and q:
1. If one is a variable and it does not occur inside the other term (occurs-check in modern terminology):

• Construct a substitution that maps that variable to the other term.
• Compose this substitution with the current one to produce Aσ_k+1.
• Increment k; return to Step 2.
2. If both are variables but different:

• Substitute one variable with the other, compose as above, and repeat Step 2.
3. If both are compound expressions with different functors or different arity:

• Unification fails; the set has no unifier, and the algorithm terminates unsuccessfully.
4. If both are compound expressions with the same functor and arity:

• Add their corresponding arguments to the set of expressions being unified.
• Return to Step 2.

Бегая глазами по исходникам unify.gisp и по описанию, вроде всё однозначно соответствует, разве нет? Дело же не в количестве строк, а в лёгкости понимания.

Comments

[juan_gandhi]

Отличный перевод на внятный язык.

[chaource]

Что-то какой-то странный текстъ былъ сгенерированъ ИИ въ этотъ разъ. Надо разобраться. Почему "Add their corresponding arguments to the set of expressions being unified"? Этого вообще-то не надо дѣлать.

[chaource]

Очевидно, текстъ и кодъ на Окамлѣ писали не вы, а какая-нибудь языковая модель. Потому что довольно много лажи.

Я использовалъ богомерзкiй ИИ только, чтобы написать остовъ кода черезъ autocomplete, а главный алгоритмъ дѣлалъ самъ, потому что иначе была полная чушь.

То, что написано у Робинсона, не соотвѣтствуетъ въ деталяхъ ни тексту (Step 1 ... Step 4), ни коду на Схемѣ или на Окамлѣ.

Богомерзкiй ИИ не понялъ у Робинсона важную вещь - "the set of expressions being unified" всегда только подвергается очередной подстановкѣ σₖ и на каждомъ шагу лишь примѣняется еще одна подстановка. Въ этотъ наборъ выраженiй мы никогда ничего не добавляемъ.

Поскольку на каждомъ шагу мы лишь увеличиваемъ очередную σₖ на новую подстановку {Uₖ / Vₖ}, то алгоритмъ можно сильно упростить. На каждомъ шагу достаточно хранить лишь наборъ Аσₖ и, если мы переходимъ къ слѣдующему шагу, то примѣнять подстановку {Uₖ / Vₖ} прямо къ предыдущему набору, получить следующiй наборъ и дальше рекурсивно вызывать опять unify.

Такъ у меня и было сдѣлано на Хаскелѣ.

Обратите вниманiе, что въ текстѣ Step 4, item 2 вообще не нуженъ - у Робинсона этого нѣтъ - потому что item 1 уже дѣлаетъ то же самое въ случаѣ, если q является Variable.

Также Step 4, item 4, какъ я уже объяснилъ, надо вычеркнуть.

Текстъ программы на Окамлѣ примѣрно (но не точно) повторяетъ структуру кода на Схемѣ и не соотвѣтствуетъ написаннымъ шагамъ Step 1 - Step 4. Въ кодѣ (ни на Scheme, ни на Gisp, ни на OCaml) вообще нигдѣ нѣтъ реализацiи вычисленiя робинсоновскихъ "disagreement sets". Тамъ сразу вычисляются новыя подстановки въ разныхъ мѣстахъ, - и это дѣлаетъ кодъ болѣе запутаннымъ. У Робинсона алгоритмъ проще: новая подстановка вычисляется только въ одномъ мѣстѣ.

Далѣе, кодъ на Окамлѣ опредѣляетъ структуру данныхъ "term" такъ, что нельзя написать выраженiе ((f g) h), потому что Сompound всегда начинается съ названiя функцiи и потомъ идутъ аргументы. Так что въ этомъ кодѣ функцiя не можетъ быть сама какимъ-то "term", она можетъ быть только всегда названной по имени константой. Это невѣрно реализуетъ вообще всю постановку задачи унификацiи произвольныхъ деревьевъ выраженiй. (Безусловно, въ Схемѣ, Окамлѣ и т.д. функцiи могутъ быть вычисляемыми выраженiями.)

Это компенсируется наличiемъ функцiй съ нѣсколькими аргументами. Всегда можно эквивалентно переписать (f g) h какъ f (g, h). Но это важный моментъ, который не очевиденъ ни изъ кода на Scheme, ни изъ текста описанiя.

Пока что изъ всѣхъ нашихъ упражненiй (которыя мнѣ были вѣсьма интересны) я дѣлаю такiе выводы:

1) Богомерзкiй ИИ не понимаетъ логику рекурсивныхъ алгоритмовъ, не объясненныхъ подробно въ учебникахъ, на которыхъ ИИ тренировали.

2) Въ такихъ случаяхъ, богомерзкiй ИИ не въ состоянiи правильно написать кодъ или правильно объяснить, что дѣлаетъ уже написанный кодъ.