Унификация - бесконечность результатов - PullRequest
Новая
       49

Унификация - бесконечность результатов

3 голосов
/ 09 ноября 2010

Ради интереса я разрабатываю (на Java) приложение, в котором используется алгоритм объединения.

Я выбрал, что мой алгоритм объединения возвращает все возможные объединения. Например, если я попытаюсь решить

add (X, Y) = succ (succ (0))

возвращает

{X = succ (succ (0)), Y = 0}, {X = succ (0), Y = succ (0)}, {X = 0, Y = succ (succ (0))}

Однако в некоторых случаях существует бесконечное количество возможных объединений (например, X> Y = true).

Знает ли кто-нибудь алгоритм, позволяющий определить, можно ли встретить бесконечное число объединений?

Заранее спасибо

Ответы [ 2 ]

8 голосов
/ 09 ноября 2010

В контексте Пролога, когда вы говорите «объединение», вы обычно имеете в виду синтаксическое объединение. Поэтому добавьте (X, Y) и succ (succ (0)), не объединяйте (как термины), потому что их функторы и арности различаются. Похоже, вы имеете в виду теорию объединения по модулю, где различные термины, такие как add (X, Y) и succ (succ (0)), могут быть объединены при условии выполнения некоторых дополнительных уравнений или предикатов. Синтаксическая унификация разрешима, и число возможных унификаторов бесконечно, если после применения наиболее общего унификатора у вас все еще есть переменные в обоих терминах. Объединение по модулю теории вообще не поддается решению. Чтобы понять, что уже базовые вопросы могут быть трудными, рассмотрим, например, проблему объединения N> 2, X ^ N + Y ^ N = Z ^ N над целыми числами, которая, если вы могли бы легко алгоритмически решить, существует ли решение (т.е. , являются ли члены унифицируемыми (по модулю целочисленной арифметики), немедленно установит последнюю теорему Ферма. Рассмотрим также теорему Матиясевича и аналогичные результаты неразрешимости.

3 голосов
/ 09 ноября 2012

В некоторых системах программирования логики ограничений вы можете легко увидеть, является ли набор решений бесконечным или нет. Например, в некоторых реализациях CLP (FD) (например, SWI-Prolog, Jekejeke Minlog, других реализациях, таких как GNU Prolog и B-Prolog нет, поскольку они предполагают конечную верхнюю / нижнюю границу), определенная степень рассуждения с бесконечными целочисленными наборами равна таким образом поддерживается. Это видно по интервальным обозначениям, таким как (SWI-Prolog): 

?- use_module(library(clpfd)).
true.

?- X #\= 2.
X in inf..1\/3..sup.

Но у этих наборов есть недостаток: они не могут быть использованы при маркировке CLP (FD), где перечисляются элементы набора и делается дальнейшая попытка решения созданных экземпляров уравнений. Это также будет противоречить следующему результату, если что-то можно будет сделать вообще для решения запросов CLP (FD):

«В 1900 году, признавая их глубину, Дэвид Гильберт предложил разрешимость всех диофантовых задач как десятая часть его Отмеченные проблемы. В 1970 году появился новый результат в математической логике известная как теорема Матиясевича, проблема решена отрицательно: общие диофантовы проблемы неразрешимы ». (Из Википедии о Диофантовых уравнениях )

Другим логическим ограничивающим программированием, которое обычно может также работать с бесконечными наборами решений, является CLP (R). Рассуждения среди уравнений там немного сильнее. Например, CLP (FD) не обнаруживает следующее несоответствие (зависит от системы, это результат для SWI-Prolog, в Jekejeke Minlog вы сразу увидите No для второго запроса, а GNU Prolog будет зацикливаться в течение примерно 4 секунд. а затем сказать нет): 

?- X #> Y.
Y#=<X+ -1.

?- X #> Y, Y #> X.
X#=<Y+ -1,
Y#=<X+ -1.

С другой стороны, CLP (R) найдет: 

?- use_module(library(clpr)).

?- {X > Y}.
{Y=X-_G5542, _G5542 > 0.0}.

?- {X > Y, Y > X}.
false.

Системы ограничений работают, реализуя алгоритмы из теории чисел, линейной алгебры, анализа и т. Д. В зависимости от области, которую они моделируют, т.е. что * обозначает в обозначении CLP (*). Эти алгоритмы могут доходить до исключения квантификатора .

Bye

...