пролог - бесконечное правило - PullRequest
6 голосов
/ 24 июня 2011

У меня есть следующие правила

% Signature: natural_number(N)/1
% Purpose: N is a natural number.
natural_number(0).
natural_number(s(X)) :-
   natural_number(X).

ackermann(0, N, s(N)). % rule 1
ackermann(s(M),0,Result):-
   ackermann(M,s(0),Result). % rule 2
ackermann(s(M),s(N),Result):-
   ackermann(M,Result1,Result),
   ackermann(s(M),N,Result1). % rule 3

Запрос: ackermann (M,N,s(s(0))).

Теперь, как я понял, в третьем расчете мы получили бесконечный поиск (ветка сбоя). Я проверяю это, и я получил конечный поиск (ошибка ветви).

Я объясню: во-первых, мы получили замену M = 0, N = s (0) (правило 1 - успех!). Во втором мы получили замену M = s (0), N = 0 (правило 2 - успех!). Но что теперь? Я пытаюсь сопоставить M = s (s (0)) N = 0, но он получил конечную ветвь поиска - неудачи. Почему компилятор не пишет мне "fail".

Спасибо.

Ответы [ 2 ]

8 голосов
/ 26 июня 2011

Было немного трудно понять, что именно Том спрашивает здесь. Возможно, ожидается, что предикат natural_number / 1 как-то влияет на выполнение ackermann / 3 . Я не буду. Последний предикат является чисто рекурсивным и не содержит подцелей, которые зависят от natural_number / 1 .

Когда три показанных пункта определены для ackermann / 3 , цель:

?- ackermann(M,N,s(s(0))).

заставляет SWI-Prolog найти (с обратным отслеживанием) два решения, о которых сообщает Том, и затем перейти к бесконечной рекурсии (что приводит к ошибке «Out of Stack»). Мы можем быть уверены, что эта бесконечная рекурсия включает в себя третье предложение, данное для ackermann / 3 (правило 3 для комментариев Тома в коде), потому что при его отсутствии мы получаем только два подтвержденных решения и затем явный сбой:

M = 0,
N = s(0) ;
M = s(0),
N = 0 ;
false.

Мне кажется, Том просит объяснить, почему изменяет отправленный запрос на тот, который устанавливает M = s(s(0)) и N = 0, производя конечный поиск (который находит одно решение, а затем дает сбой при возврате) ), согласуется с бесконечной рекурсией, созданной предыдущим запросом. Мое подозрение здесь заключается в том, что есть недопонимание того, что движок Prolog пытается откатить назад (для исходного запроса), поэтому я собираюсь углубиться в это. Надеюсь, это прояснит ситуацию для Тома, но давайте посмотрим, так ли это. По общему признанию мое лечение многословно, но механизм выполнения Пролога (объединение и решение подцелей) заслуживает изучения.

[ Добавлено: Предикат имеет очевидную связь со знаменитой функцией Аккермана , которая является полностью вычислимой, но не примитивно-рекурсивной. Эта функция, как известно, быстро растет, поэтому мы должны быть осторожны в заявлении о бесконечной рекурсии, потому что очень большая, но конечная рекурсия также возможна. Однако третье предложение помещает два его рекурсивных вызова в порядке, противоположном тому, что я сделал бы, и это обращение, похоже, играет критическую роль в бесконечной рекурсии, которую мы находим при пошаговом выполнении кода ниже.]

Когда передается цель верхнего уровня ackermann(M,N,s(s(0))), SWI-Prolog пробует предложения (факты или правила), определенные для ackermann / 3 , пока не найдет тот, чья «голова» объединяется с данным запросом , Движок Prolog не так уж далек от первого предложения, этот факт:

ackermann(0, N, s(N)).

объединится, связав M = 0 и N = s(0), как уже было описано как первый успех.

Если запрашивается возврат, например, пользователь вводит точку с запятой, механизм Пролог проверяет, есть ли альтернативный способ удовлетворить это первое предложение. Нет. Затем механизм Пролога пытается выполнить следующие пункты для ackermann / 3 в указанном порядке.

Опять же, поиск не должен идти далеко, потому что заголовок второго предложения также объединяется с запросом. В этом случае у нас есть правило:

ackermann(s(M),0,Result) :- ackermann(M,s(0),Result).

Объединение запроса и заголовка этого правила дает привязки M = s(0), N = 0 в терминах переменных, используемых в запросе . В терминах переменных, используемых в правиле, как указано выше, M = 0 и Result = s(s(0)). Обратите внимание, что объединение сопоставляет термины по их внешнему виду в качестве вызывающих аргументов и не рассматривает имена переменных, повторно используемые через границу запроса / правила, как означающее идентичность.

Поскольку этот пункт является правилом (имеющим как тело, так и голову), объединение является лишь первым шагом в попытке добиться успеха с ним. Движок Prolog теперь пытается выполнить одну подцель, которая появляется в теле этого правила:

ackermann(0,s(0),s(s(0))).

Обратите внимание, что эта подцель происходит от замены "локальных" переменных, используемых в правиле, значениями объединения, M = 0 и Result = s(s(0)). Движок Prolog теперь рекурсивно вызывает предикат ackermann / 3 , чтобы проверить, может ли эта подзадача быть выполнена.

Может, как первый пункт (факт) для ackermann / 3 , объединяться очевидным образом (действительно, по сути, так же, как и ранее, в отношении переменных, используемых в предложении). И, таким образом (после успешного рекурсивного вызова) мы получаем второе решение, преуспевающее во внешнем вызове (запрос верхнего уровня).

Если пользователь просит механизм Пролога вернуться назад еще раз, он снова проверяет, может ли текущее предложение (второе для ackermann / 3 ) быть выполнено альтернативным способом. Не может, и поэтому поиск продолжается, переходя к третьему (и последнему) предложению для предиката ackermann / 3 :

ackermann(s(M),s(N),Result) :-
    ackermann(M,Result1,Result),
    ackermann(s(M),N,Result1).

Я собираюсь объяснить, что эта попытка производит бесконечную рекурсию. Когда мы объединяем запрос верхнего уровня с заголовком этого предложения, мы получаем привязки для аргументов, которые, возможно, могут быть четко поняты путем сопоставления терминов в запросе с терминами в заголовке:

   query     head
     M       s(M)
     N       s(N)
   s(s(0))  Result

Учитывая, что переменные, имеющие в запросе то же имя, что и переменные в правиле, не ограничивают объединение, эту тройку терминов можно объединить. Запрос M будет заголовком s(M), то есть составным термином, включающим функтор s, применяемый к некоторой пока неизвестной переменной M, появляющейся в голове. То же самое для запроса N. Пока единственным «наземным» термином является переменная Result, появляющаяся в заголовке (и теле) правила, которая связана с s(s(0)) из запроса.

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

ackermann(M,Result1,s(s(0))).

Позвольте мне указать, что я использовал здесь «локальные» переменные предложения, за исключением того, что я заменил Result значением, с которым он был связан в объединении. Теперь обратите внимание, что кроме замены N исходного запроса верхнего уровня на имя переменной Result1, мы просто запрашиваем то же самое, что и исходный запрос в этой подцели. Конечно, это большая подсказка, что мы можем войти в бесконечную рекурсию.

Однако нужно немного больше обсудить, чтобы понять, почему мы не получаем никаких дальнейших решений! Это связано с тем, что для первого успеха этой первой подцели (как и ранее было найдено) потребуются M = 0 и Result1 = s(0), а затем механизм Пролога должен продолжить попытки выполнить вторую подцель условия:

ackermann(s(0),N,s(0)).

К сожалению, эта новая подцель не объединяется с первым предложением (фактом) для ackermann / 3 . Он объединяет с заголовком второго предложения следующим образом:

   subgoal     head
     s(0)      s(M)
      N         0
     s(0)     Result

но это приводит к подцелию (из тела второго предложения):

ackermann(0,s(0),s(0)).

Это не объединяется с заголовком первого или второго предложения. Он также не объединяется с заголовком третьего предложения (который требует, чтобы первый аргумент имел форму s(_)). Таким образом, мы достигли точки отказа в дереве поиска. Движок Prolog теперь откатывается назад, чтобы увидеть, можно ли альтернативно удовлетворить первую подзадачу тела третьего предложения. Как мы знаем, это может быть (поскольку эта подцель в основном совпадает с исходным запросом).

Теперь M = s(0) и Result1 = 0 этого второго решения приводят к этому для второй подцели тела третьего предложения:

ackermann(s(s(0)),N,0).

Хотя это не объединяется с первым предложением (фактом) предиката, оно объединяется с заголовком второго предложения:

   subgoal     head
   s(s(0))     s(M)
      N         0
      0       Result

Но чтобы преуспеть, движок Prolog также должен удовлетворять основанию второго предложения, которое теперь:

ackermann(s(s(0)),s(0),0).

Мы легко видим, что это не может объединиться с заголовком первого или второго предложения для ackermann / 3 . Его можно объединить с главой третьего пункта:

  sub-subgoal  head(3rd clause)
    s(s(0))       s(M)
      s(0)        s(N)
       0         Result

Как должно быть теперь известно, механизм Пролога проверяет, может ли быть удовлетворена первая подцель тела третьего предложения, что составляет эту под-под-подцель:

ackermann(s(0),Result1,0).

Это не объединяется с первым предложением (фактом), но объединяется с заголовком связывания второго предложения M = 0, Result1 = 0 и Result = 0, производя (по знакомой логике) подподсабвуфер -subgoal:

ackermann(0,0,0).

Так как это не может быть объединено ни с одной из глав трех пунктов, это терпит неудачу. В этот момент механизм Пролога возвращается к попытке удовлетворить вышеупомянутую подподчинение, используя третий пункт. Объединение происходит так:

  sub-sub-subgoal  head(3rd clause)
       s(0)             s(M)
      Result1           s(N)
         0             Result

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

ackermann(0,Result1,0).

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

ackermann(M,Result1,s(s(0))).

То, что мы видели выше, заключается в том, что решения для этой подцели, дублирующие исходный запрос из первого и второго пунктов ackermann / 3 , не позволяют второй подцели тела третьего предложения добиться успеха. Поэтому движок Prolog пытается найти решения, удовлетворяющие третьему пункту. Но ясно, что теперь это входит в бесконечную рекурсию, так как это третье предложение объединится в его голове, но тело третьего предложения будет повторять точно такой же поиск, который мы только что преследовали. Таким образом, движок Prolog теперь бесконечно входит в тело третьего предложения.

5 голосов
/ 24 июня 2011

Позвольте мне перефразировать ваш вопрос: запрос ackermann(M,N,s(s(0))). находит два решения, а затем зацикливается. В идеале, он должен завершаться после этих двух решений, поскольку нет других N и M, значение которых равно s(s(0)).

Так почему же запрос не завершается повсеместно? Понимание этого может быть довольно сложным, и лучший совет состоит в том, чтобы не пытаться понять точный механизм выполнения. Причина очень проста: механизм выполнения Prolog оказывается настолько сложным, что вы все равно легко поймете его неправильно, если попытаетесь понять его, шагая по коду.

Вместо этого вы можете попробовать следующее: Вставьте цели false в любом месте вашей программы. Если результирующая программа не завершается, то и исходная программа не прекращается.

В вашем случае:

<s>ackermann(0, N, s(N)) :- <b>false</b></s>.
<s>ackermann(s(M),0,Result):- <b>false</b></s>,
   <s>ackermann(M,s(0),Result)</s>.
ackermann(s(M),s(N),Result):-
   ackermann(M,Result1,Result), <b>false</b>,
   <s>ackermann(s(M),N,Result1)</s>.

Теперь мы можем удалить первое и второе правило. И в третьем правиле мы можем удалить цель после ложного. Поэтому, если следующий фрагмент не завершается, исходная программа также не завершается.

ackermann(s(M),s(N),Result):-ackermann(M,Result1,Result), false.

Эта программа теперь завершает работу, только если известен первый аргумент. Но в нашем случае это бесплатно ...

То есть: рассматривая небольшую часть программы, мы уже смогли вывести свойство всей программы. Подробнее см. , этот документ и другие на сайте.

К сожалению, такого рода рассуждения работают только в случаях не прекращения. Для прекращения дела сложнее. Лучше всего попробовать такой инструмент, как cTI , который определяет условия завершения и пытается доказать их оптимальность. Я уже вошел в вашу программу, поэтому попробуйте изменить, если и увидеть эффекты!

Если мы находимся в этом: этот небольшой фрагмент также говорит нам, что второй аргумент не влияет на завершение 1 . Это означает, что запросы типа ackermann(s(s(0)),s(s(0)),R). будут не прекратить либо. Обменяйтесь целями, чтобы увидеть разницу ...


1 Если быть точным, термин, который не объединяется с s(_), будет влиять на завершение. Подумайте о 0. Но любые s(0), s(s(0)), ... не будут влиять на завершение.

...