Унификацию помните?

[vak]

Представьте что у нас имеется два выражения, состоящие их переменных и констант. Ну или два дерева, ведь выражения однозначно представляются деревьями. И нам хочется сравнить эти два выражения или дерева. Это одно и тоже или разные вещи? В том смысле, что при каких-то значениях переменных выражения совпадают.

Такой алгоритм сопоставления назвали унификацией. Когда-то на нём строили экспертные системы: помните язык Пролог? Алгоритм унификации пытается сделать два символических выражения равными, вычисляя объединяющую подстановку для этих выражений. Подстановка — это функция, заменяющая переменные другими выражениями. Очень важно, что она действует одинаково на все вхождения одной и той же переменной: если подстановка меняет одно вхождение переменной x на a, она должна заменить все вхождения x на a.

Объединяющая подстановка (или унификатор) для двух выражений e1 и e2 — это подстановка σ, такая что применение σ делает e1 и e2 структурно одинаковыми. Рассмотрим на примерах.

Пример 1: простая унификация. Выражения f(x) и f(y) можно унифицировать, заменив y на x (или наоборот).
Тогда унификатор σ действует так:

σ(y) = x

σ оставляет остальные переменные без изменений.

Пример 2: неудачная унификация. Выражения x + 1 и y + 2 нельзя унифицировать. Не стоит пытаться подставить 3 вместо x и 2 вместо y, чтобы оба выражения стали равны 4. Унификация требует символического равенства, а 1 не сопоставляется с 2.

Пример 3: несколько возможных унификаторов. Для выражений f(x, y) и f(1, y) возможны разные унификаторы:

σ₁ = { x ↦ 1 } даёт результат f(1, y).
σ₂ = { x ↦ 1, y ↦ 5 } даёт f(1, 5).

Оснований менять y нет, поэтому σ₁ предпочтительнее.

Алгоритмы унификации обычно стремятся получить наиболее общий унификатор (most general unifier, MGU). Это когда делаются только необходимые подстановки. Все остальные унификаторы получаются из MGU путём добавления новых замен. В примере выше σ₁ — MGU, а σ₂ — его частный случай.

Красивая реализация унификации приведена как пример в книжке The Scheme Programming Language: Section 12.10. A Unification Algorithm. Меньше сотни строчек с комментариями, но понять непросто: unify.ss.

А давайте перепишем на смешной язык Gisp. Который внутри тот же Scheme, но с синтаксисом Go. Мне кажется, гораздо яснее выходит.

// occurs? returns true if and only if u occurs in v
func occurs(u, v) {
    if !pairp(v) {
        return false
    }
    return occursHelper(u, rest(v))
}

func occursHelper(u, l) {
    if !pairp(l) {
        return false
    }
    if eq(u, first(l)) {
        return true
    }
    if occurs(u, first(l)) {
        return true
    }
    return occursHelper(u, rest(l))
}

// sigma returns a new substitution procedure extending s by
// the substitution of u with v
func sigma(u, v, s) {
    return func(x) {
        return sigmaApply(u, v, s, s(x))
    }
}

func sigmaApply(u, v, s, x) {
    if symbolp(x) {
        if eq(x, u) {
            return v
        }
        return x
    }
    return cons(first(x), map(func(elem) {
        return sigmaApply(u, v, s, elem)
    }, rest(x)))
}

// try-subst tries to substitute u for v but may require a
// full unification if (s u) is not a variable, and it may
// fail if it sees that u occurs in v.
func trySubst(u, v, s, ks, kf) {
    var uSub = s(u)
    if !symbolp(uSub) {
        return uni(uSub, v, s, ks, kf)
    }
    var vSub = s(v)
    if eq(uSub, vSub) {
        return ks(s)
    }
    if occurs(uSub, vSub) {
        return kf("cycle")
    }
    return ks(sigma(uSub, vSub, s))
}

// uni attempts to unify u and v with a continuation-passing
// style that returns a substitution to the success argument
// ks or an error message to the failure argument kf.  The
// substitution itself is represented by a procedure from
// variables to terms.
func uni(u, v, s, ks, kf) {
    if symbolp(u) {
        return trySubst(u, v, s, ks, kf)
    }
    if symbolp(v) {
        return trySubst(v, u, s, ks, kf)
    }
    if eq(first(u), first(v)) && length(u) == length(v) {
        return uniHelper(rest(u), rest(v), s, ks, kf)
    }
    return kf("clash")
}

func uniHelper(u, v, s, ks, kf) {
    if nullp(u) {
        return ks(s)
    }
    return uni(first(u), first(v), s, func(newS) {
        return uniHelper(rest(u), rest(v), newS, ks, kf)
    }, kf)
}

// unify shows one possible interface to uni, where the initial
// substitution is the identity procedure, the initial success
// continuation returns the unified term, and the initial failure
// continuation returns the error message.
func unify(u, v) {
    return uni(u, v, func(x) {
        return x
    }, func(s) {
        return s(u)
    }, func(msg) {
        return msg
    })
}

Comments

[chaource]

Это чудовищно. Книга ничего не объясняетъ, вываливаетъ на читателя громоздкiй кодъ. Даже не объясняется, какимъ образомъ представлены структуры данныхъ. Дается примѣръ, что (unify '(f x y) '(g x y)) не работаетъ, но не объясняется, почему здѣсь нельзя унифицировать f = g. Потому, что мы не унифицируемъ символы функцiй, а только символы аргументовъ? А почему, вѣдь мы можемъ унифицировать переменную и функцiю, какъ въ слѣдующемъ примѣрѣ унифицируется х и (h)? Этого не объясняется въ текстѣ. Текстъ комментарiевъ объясняетъ, что происходитъ съ continuation passing, а это какъ разъ простая деталь, но не объясняетъ ничего про алгоритмъ. Ссылка на статью Робинсона, гдѣ алгоритмъ сформулированъ очень кратко, но потомъ долго доказываются теоремы о его правильности.

Я постараюсь прочитать какую-нибудь статью съ объясненiемъ алгоритма и напишу его на языкѣ Haskell. Я ожидаю, что будетъ строк 30-40, не больше, и что вѣсь алгоритмъ станетъ декларативнымъ (т.е. сразу понятнымъ при чтенiи кода).

[straktor]

> мы не унифицируемъ символы функцiй, а только символы аргументовъ?

таков Пролог
с большой буквы переменные, с маленькой буквы конкретные функторы и атомы
разные атомы разные, разные функторы разные
функтор не может быть переменной, это основа Пролога

[chaource]

Но въ текстѣ этого не написано, и всѣ буквы строчныя.

Я согласенъ, что имѣется въ виду именно это. Конструкторы функцiй и атомы - это константы, ихъ нельзя подставлять.

[juan_gandhi]

Ого как!

[chaource]

Я написалъ въ редакторѣ Сursor слѣдующее:

-- The unification algorithm of Robinson

data Term = Var Text | App Term Term | Const Text

isVar :: Term -> Bool

Послѣ чего мнѣ внезапно предложили autocomplete на вѣсь оставшiйся кодъ.

isVar, occurs, substitute, unify - все было уже тамъ.

Аж 15 строкъ, включая сигнатуры типовъ и пустыя строки.

Потомъ я попросилъ перевести тесты на Хаскель.

Естественно, кодъ былъ совершенно невѣрнымъ и не компилировался. Послѣ промпта и вопроса о кодѣ, кодъ былъ переписанъ и сталъ занимать 22 строки. Четыре изъ шести тестовъ заработали, два нѣтъ. Но это уже хлѣбъ, дальше читать кодъ и руками исправлять. Кодъ по-прежнему совершенно невѣрный и имѣетъ мало общаго съ алгоритмомъ Робинсона. Ну ничего, такъ и работаемъ.

[chaource]

Алгоритмъ занимаетъ 32 строки. Простой кодъ, повторяющiй описанiе Робинсона, но безъ GOTO.

-- The unification algorithm of Robinson (1965).

data Term = VarF Text | AppF Term Term | ConstF Text
  deriving stock (Show, Eq)

data UnificationResult = UnificationSuccess Term | UnificationClash Term Term | UnificationCycle Term Term
  deriving stock (Show, Eq)

substitute :: Text -> Term -> Term -> Term
substitute x t (VarF y) = if x == y then t else VarF y
substitute x t (AppF t1 t2) = AppF (substitute x t t1) (substitute x t t2)
substitute _ _ (ConstF c) = ConstF c

occurs :: Text -> Term -> Bool
occurs x (VarF y) = x == y
occurs x (AppF t1 t2) = occurs x t1 || occurs x t2
occurs _ (ConstF _) = False

disagreements :: Term -> Term -> Maybe (Term, Term) -- "Disagreements" is a sorted pair of terms where variables go first.
disagreements t1 t2 = case (t1, t2) of
  (VarF x, VarF y) | x == y -> Nothing
  (ConstF x, ConstF y) | x == y -> Nothing
  (AppF a1 a2, AppF b1 b2)
    | a1 == b1 -> disagreements a2 b2
    | otherwise -> disagreements a1 b1
  (a, VarF x) -> Just (VarF x, a) -- Move the variable to the left (Robinson's "lexicographic" ordering).
  (a, b) -> Just (a, b)

unify :: Term -> Term -> UnificationResult
unify t1 t2 = case disagreements t1 t2 of
  Just (VarF x, b) ->  -- If the disagreement is on a variable, substitute [x/b] and unify again.
    if occurs x b      -- In this case, we can't substitute x.
      then UnificationCycle (VarF x) b
      else unify (substitute x b t1) (substitute x b t2)
  Just (a, b) -> UnificationClash a b -- Cannot substitute since "a" is not a variable.
  Nothing -> UnificationSuccess t1

spec :: Spec
spec = do
  describe "unification algorithm of Robinson" do
    it "unifies two variables" do
      let x = VarF "x"
          y = VarF "y"
      unify x y `shouldBe` UnificationSuccess x

    it "fails to unify different function symbols (clash)" do
      let t1 = AppF (AppF (ConstF "f") (VarF "x")) (VarF "y")
          t2 = AppF (AppF (ConstF "g") (VarF "x")) (VarF "y")
      unify t1 t2 `shouldBe` UnificationClash (ConstF "f") (ConstF "g")

    it "unifies terms with substitutions" do
      let t1 = AppF (AppF (ConstF "f") (VarF "x")) (ConstF "h")
          t2 = AppF (AppF (ConstF "f") (ConstF "h")) (VarF "y")
          expected = AppF (AppF (ConstF "f") (ConstF "h")) (ConstF "h")
      unify t1 t2 `shouldBe` UnificationSuccess expected

    it "fails to unify when cycle is detected" do
      let t1 = AppF (AppF (ConstF "f") (AppF (ConstF "g") (VarF "x"))) (VarF "y")
          t2 = AppF (AppF (ConstF "f") (VarF "y")) (VarF "x")
      unify t1 t2 `shouldBe` UnificationCycle (VarF "x") (AppF (ConstF "g") (VarF "x"))

    it "unifies terms with nested applications" do
      let t1 = AppF (AppF (ConstF "f") (AppF (ConstF "g") (VarF "x"))) (VarF "y")
          t2 = AppF (AppF (ConstF "f") (VarF "y")) (AppF (ConstF "g") (VarF "x"))
          expected = AppF (AppF (ConstF "f") (AppF (ConstF "g") (VarF "x"))) (AppF (ConstF "g") (VarF "x"))
      unify t1 t2 `shouldBe` UnificationSuccess expected

    it "unifies terms with variable and constant" do
      let t1 = AppF (AppF (ConstF "f") (AppF (ConstF "g") (VarF "x"))) (VarF "y")
          t2 = AppF (AppF (ConstF "f") (VarF "y")) (VarF "z")
          expected = AppF (AppF (ConstF "f") (AppF (ConstF "g") (VarF "x"))) (AppF (ConstF "g") (VarF "x"))
      unify t1 t2 `shouldBe` UnificationSuccess expected

[vak]

Ну и чем это понятнее? Много визуального шума.

[chaource]

Программа на Хаскелѣ существенно короче, чѣмъ на Схемѣ, и кодъ на Хаскелѣ легко сопоставить съ алгоритмомъ изъ статьи Робинсона, въ отличiе отъ кода на Схемѣ.

Скажемъ, гдѣ на Схемѣ вычисляются робинсоновскiя "disagreements"? Не видно. Какъ работаетъ "occurs", что означаютъ "if eq(u, first(l))", "if occurs(u, first(l))"? Непонятно. Почему то провѣряется nullp, то symbolp, то pairp? Неясно. Можетъ тамъ ошибка, вмѣсто symbolp надо было написать nullp, какъ это увидѣть? Нельзя этого увидѣть, нѣтъ увѣренности въ правильности кода, надо тестировать и отлаживать программу.

Въ вашемъ кодѣ постоянно скобки и return, func, return. Это и есть визуальный шумъ. Невозможно это читать и визуально провѣрять правильность кода:

func unify(u, v) {
    return uni(u, v, func(x) {
        return x
    }, func(s) {
        return s(u)
    }, func(msg) {
        return msg
    })
}

Я спецiально не сталъ писать кодъ въ continuation-passing style, потому что это труднѣе читать. На Хаскелѣ вышеприведенный фрагментъ выглядѣлъ бы примѣрно такъ:

unify u v = uni u v (\x -> x) (\s -> s u) (\msg -> msg)

Читать и провѣрять такой кодъ куда легче, чѣмъ кодъ на Схемѣ или Gisp, но все равно труднѣе, чѣмъ кодъ въ прямомъ функцiональномъ стилѣ.

Еще примѣръ. Вот фрагментъ моего кода на Хаскелѣ, который говоритъ, что подстановка "t" вмѣсто "x" въ выраженiе вида "t1(t2)" дѣлается путемъ подстановки отдѣльно въ "t1" и отдѣльно въ "t2": (Выраженiе "t1(t2)" представляется какъ "AppF t1 t2", напоминая намъ, что это "function application".)

substitute x t (AppF t1 t2) = AppF (substitute x t t1) (substitute x t t2)

Очевидно, что этотъ кодъ правильный, тутъ нечего провѣрять.

Гдѣ соотвѣтствующiй фрагментъ кода на Схемѣ? Какъ найти этотъ фрагментъ и провѣрить, что онъ правильно написанъ?

Аналогично, occurs не вызываетъ вообще вопросовъ. Большинство кода на Хаскелѣ совершенно очевидно соотвѣтствуетъ словесному описанiю Робинсона:
Unification Algorithm. The following process, applicable to any finite
nonempty set A of well-formed expressions, is called the Unification Algorithm:

Step 1. Set sk = empty, k = 0, and goto step2.

Step 2. If A sk is not a singleton, go to step 3. Otherwise terminate.

Step 3. Let Vk be the earliest, and Uk the next earliest, in the lexical ordering of the disagreement set Bk of A sk. If Vk is a variable, and does not occur in Uk , set s(k+1) = sk {Uk/Vk}, add 1 to k, and return to step 2. Otherwise, terminate.

Это надо переписать попроще, для случая двухъ термовъ:

unify (u, v) =

Compute the disagreement set of u, v. This will be either a pair (U, V) of terms, or an empty set. If empty, we finish unification with success.

Sort the pair, so that the first term is a variable if any of them is.

If the first term of the disagreement pair is a variable U and that variable does not occur in V, we perform a substitution U/V on both u and v, and repeat trying to unify the terms (substitute U by V in u) and (substitute U by V in v). This is a recursive call to "unify".

If U is a variable and it does occur in V, we finish with a "cycle" error.

If U is not a variable, we finish with a "clash" error.

После этого провѣрять хаскельную программу легко чисто визуально.

О программѣ на Схемѣ (или Gisp) этого сказать нельзя. Совершенно неочевидно, что они реализуютъ алгоритмъ Робинсона, и вообще неочевидно, что эти программы дѣлаютъ.

[vak]

Робинсон голова, конечно, однако язык у него тяжёлый. И Хаскель могуч, ничего не имею против Хаскеля. Но мне больше симпатичен вариант на OCaml: https://github.com/sergev/vak-opensource/blob/master/languages/ocaml/unify.ml

[sobriquet9]

А проверять как? Например, можно ли унифицировать x²/x и просто x? Значения этих выражений совпадают почти всегда.

[straktor]

Нет, не унифицируется, первое это /(*(х,х)), второе атом
Вы говорите о сокращении, а тут ещё с делением

Интересно другое
X = f(X)
Унифицируется, но напечатать нельзя, бесконечно

[chaource]

x = f(x) не унифицируется - даетъ ошибку "cycle". Потому что f считается какъ произвольная функцiя.

[sobriquet9]

Унификация была объяснена как "хочется сравнить эти два выражения или дерева. Это одно и тоже или разные вещи? В том смысле, что при каких-то значениях переменных выражения совпадают".

x и x+x-x совпадают при всех значениях x, это одно и то же или нет. В чуть более сложном примере выше выражения совпадают при почти всех значениях x.

[chaource]

Задача унификацiи ставится для формальныхъ деревьевъ безъ семантики. Операцiи +, - и всѣ остальныя имена функцiй f, g в выраженiяхъ f(x + y), g(x, y + 1) ничего не означаютъ и интерпретируются какъ произвольныя, неизвѣстныя функцiи.

[vak]

Сопоставляем выражения, а не результат их вычислений.

[chaource]

Книга показываетъ 6 тестовъ унификацiи.

(unify 'x 'y)  ↦ y
(unify '(f x y) '(g x y))  ↦ "clash"
(unify '(f x (h)) '(f (h) y))  ↦ (f (h) (h))
(unify '(f (g x) y) '(f y x))  ↦ "cycle"
(unify '(f (g x) y) '(f y (g x)))  ↦ (f (g x) (g x))
(unify '(f (g x) y) '(f y z))  ↦ (f (g x) (g x))

[spamsink]

Пример 2, OMFG, x = 2, y = 1. Это удачная унификация, благо сложение у нас коммутативное?

[vak]

Сопоставляем выражения, не домысливая семантику их вычислений. Плюс вовсе не обязательно сложение, а константы не обязательно целые числа.

[spamsink]

Это возражение противоречит объяснению в посте:

Может показаться, будто можно подставить 3 вместо x и 2 вместо y, чтобы оба выражения стали равны 4. Но унификация требует символического равенства, а выражения 3 + 1 и 2 + 2 — всё ещё разные синтаксические структуры, хотя и дают одинаковое числовое значение.

[vak]

Я поэтому и говорю про деревья, чтобы отвлечь от арифметической семантики.

Про числовое значение это тоже попытка объяснить так не делать. 😀

[spamsink]

Тогда объяснение в корне неправильное. Необходимо было сказать, что унификация невозможна, поскольку 1 не сопоставляется с 2. И зачем говорить про деревья, если в отрыве от семантики достаточно говорить про строки токенов и editing distance?

[vak]

Правильно говоришь. Давай я переформулирую в посте.