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

[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

[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))