Применение унификации?

Question

Каковы (практические) области применения Объединение?Где это на самом деле используется в реальном мире?

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

Answer 1

Объединение - это, по сути, процесс замена.Я видел, что это называется "двустороннее сопоставление".

В Prolog, на других языках логического программирования и на языках, непосредственно основанных на логике перезаписи (Мод, Элан, и т.д. ...) - это механизм, с помощью которого свободные (логические) переменные привязываются к терминам / значениям.В параллельном прологе эти переменные интерпретируются как каналы связи.

ИМО, лучший способ понять это с некоторыми примерами из математики (унификация была / является базовым ключевым механизмом, например, в контексте исследования автоматизированных доказательств теорем, подполя искусственного интеллекта;другое использование в в алгоритмы вывода типов).Приведенные ниже примеры взяты из контекста системы компьютерной алгебры (CAS):

Первый пример:

учитывая множество Q и две двоичные операции * и + над ним, тогда * является левораспределительным над +, если:

X * (Y + Z)   =   (X * Y) + (X * Z)   |1|

это - правило перезаписи (набор правил перезаписи - это система перезаписи).

Если мы хотим применить это правило перезаписи к конкретному случаю, скажем:

a * (1 + b)   |2|

мы объединить (с помощью алгоритма объединения) этот термин, |2|, с левая сторона (ЛСЗ) из |1| и мы имеем эту (тривиальную по назначению) замену (the самый общий объединитель, мгу):

{X/a, Y/1, Z/b}   |3|

Теперь, применяя |3| к правая сторона (резус - фактор) из |1|, мы имеем, наконец:

(a * 1) + (a * b)

Это было просто, и чтобы оценить, что может сделать объединение, я покажу немного более сложный пример.

Второй пример:

Учитывая это правило перезаписи:

log(X,Y) + log(X,Z)   =>   log(X,Y*Z)   |4|

мы применяем его к этому уравнению:

log(e,(x+1)) + log(e,(x-1)) = k   |5|

(ЛСЗ из |5| объединить в ЛСЗ из |4|), таким образом, мы имеем это мгу:

{X/e, Y/(x+1), Z/(x-1)}   |6|

Обратите внимание, что X и x - это две разные переменные.Здесь у нас есть две переменные, X и Y, которые соответствуют двум сложные термины, (x+1) и (x-1), а не простые значения или переменные.

Мы применяем это мгу, |6|, к резус - фактор из | 4 | затем и мы помещаем обратно это в | 5 |;итак, у нас есть:

log(e,(x+1)*(x-1)) = k   |7|

и так далее.

(Надеюсь, я не допустил никакой ошибки, иначе это может еще больше запутать неофитов.)

Answer 2

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

Answer 3

Пролог, например, использует унификацию для поиска значений переменных , удовлетворяющих правилам - см. это объяснение для примера.Я ожидаю, что это типичный метод для логических языков программирования в целом, хотя у меня нет опыта работы с какими-либо другими.

Answer 4

Унификация подобна сопоставлению с образцом, когда вы объединяете две структуры, где переменным в одной разрешено сопоставлять значения в другой.

Простейшая форма унификации происходит всякий раз, когда вы вызываете функцию на обычном языке.У вызывающего есть аргументы, а у вызываемого - параметры.Параметры "привязаны" к аргументам, и это создает экземпляр функции.

Другая простая форма унификации - это когда вы используете регулярное выражение для сопоставления, например, в командной строке вы можете сказать dir x*y*.z* который будет соответствовать некоторым, но не всем именам файлов.

Искусственный интеллект любит использовать механизмы вывода, пытаясь имитировать рассуждения на основе совокупности знаний, обычно в форме логических утверждений.Чтобы привести глупый пример, вы могли бы "знать", что "все люди смертны", как в forall(x)(man(x) implies mortal(x)).Тогда, если вы зададите вопрос "смертен ли Сэм", как mortal(Sam)?, вы могли бы объединить это с правилом, чтобы получить новый вопрос "является ли Сэм мужчиной". man(Sam)?

Надеюсь, это поможет.