Serge Vakulenko (![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png)
vak) wrote2025-11-19 01:12 am
vak) wrote2025-11-19 01:12 am
Entry tags:
Унификацию помните?
Представьте что у нас имеется два выражения, состоящие их переменных и констант. Ну или два дерева, ведь выражения однозначно представляются деревьями. И нам хочется сравнить эти два выражения или дерева. Это одно и тоже или разные вещи? В том смысле, что при каких-то значениях переменных выражения совпадают.
Такой алгоритм сопоставления назвали унификацией. Когда-то на нём строили экспертные системы: помните язык Пролог? Алгоритм унификации пытается сделать два символических выражения равными, вычисляя объединяющую подстановку для этих выражений. Подстановка — это функция, заменяющая переменные другими выражениями. Очень важно, что она действует одинаково на все вхождения одной и той же переменной: если подстановка меняет одно вхождение переменной x на a, она должна заменить все вхождения x на a.
Объединяющая подстановка (или унификатор) для двух выражений e1 и e2 — это подстановка σ, такая что применение σ делает e1 и e2 структурно одинаковыми. Рассмотрим на примерах.
Пример 1: простая унификация. Выражения f(x) и f(y) можно унифицировать, заменив y на x (или наоборот).
Тогда унификатор σ действует так:
Пример 2: неудачная унификация. Выражения x + 1 и y + 2 нельзя унифицировать. Может показаться, будто можно подставить 3 вместо x и 2 вместо y, чтобы оба выражения стали равны 4. Но унификация требует символического равенства, а выражения 3 + 1 и 2 + 2 — всё ещё разные синтаксические структуры, хотя и дают одинаковое числовое значение.
Пример 3: несколько возможных унификаторов. Для выражений f(x, y) и f(1, y) возможны разные унификаторы:
Алгоритмы унификации обычно стремятся получить наиболее общий унификатор (most general unifier, MGU). Это когда делаются только необходимые подстановки. Все остальные унификаторы получаются из MGU путём добавления новых замен. В примере выше σ₁ — MGU, а σ₂ — его частный случай.
Красивая реализация унификации приведена как пример в книжке The Scheme Programming Language: Section 12.10. A Unification Algorithm. Меньше сотни строчек с комментариями, но понять непросто: unify.ss.
А давайте перепишем на смешной язык Gisp. Который внутри тот же Scheme, но с синтаксисом Go. Мне кажется, гораздо яснее выходит.
Такой алгоритм сопоставления назвали унификацией. Когда-то на нём строили экспертные системы: помните язык Пролог? Алгоритм унификации пытается сделать два символических выражения равными, вычисляя объединяющую подстановку для этих выражений. Подстановка — это функция, заменяющая переменные другими выражениями. Очень важно, что она действует одинаково на все вхождения одной и той же переменной: если подстановка меняет одно вхождение переменной 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. Но унификация требует символического равенства, а выражения 3 + 1 и 2 + 2 — всё ещё разные синтаксические структуры, хотя и дают одинаковое числовое значение.
Пример 3: несколько возможных унификаторов. Для выражений f(x, y) и f(1, y) возможны разные унификаторы:
σ₁ = { x ↦ 1 } даёт результат f(1, y).Оснований менять y нет, поэтому σ₁ предпочтительнее.
σ₂ = { x ↦ 1, y ↦ 5 } даёт f(1, 5).
Алгоритмы унификации обычно стремятся получить наиболее общий унификатор (most general unifier, MGU). Это когда делаются только необходимые подстановки. Все остальные унификаторы получаются из MGU путём добавления новых замен. В примере выше σ₁ — MGU, а σ₂ — его частный случай.
Красивая реализация унификации приведена как пример в книжке The Scheme Programming Language: Section 12.10. A Unification Algorithm. Меньше сотни строчек с комментариями, но понять непросто: unify.ss.
А давайте перепишем на смешной язык Gisp. Который внутри тот же Scheme, но с синтаксисом Go. Мне кажется, гораздо яснее выходит.
( исходный код )
![[livejournal.com profile]](https://www.dreamwidth.org/img/external/lj-userinfo.gif){kind=small}
