Было немного сложно понять, что именно Том спрашивает здесь. Возможно, предполагается, что предикат натуральное_число/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, производя конечный поиск (который находит одно решение, а затем терпит неудачу при возврате), согласуется с бесконечная рекурсия, созданная предыдущим запросом. Я подозреваю, что существует неправильное понимание того, что движок Пролога пытается отследить (для исходного запроса), поэтому я собираюсь углубиться в это. Надеюсь, это прояснит ситуацию для Тома, но посмотрим, так ли это. По общему признанию, моя трактовка многословна, но механизм выполнения Пролога (объединение и разрешение подцелей) достоин изучения.
[Добавлено: Предикат имеет очевидную связь со знаменитой функцией Аккермана, которая полностью вычислима, но не примитивно-рекурсивный. Известно, что эта функция быстро растет, поэтому нам нужно быть осторожными, заявляя о бесконечной рекурсии, потому что возможна очень большая, но конечная рекурсия. Однако в третьем предложении два рекурсивных вызова располагаются в порядке, противоположном тому, который я бы сделал, и это обращение, похоже, играет решающую роль в бесконечной рекурсии, которую мы обнаруживаем при пошаговом выполнении кода ниже.]
Когда передается цель верхнего уровня ackermann(M,N,s(s(0))), SWI-Prolog пробует предложения (факты или правила), определенные для ackermann/3, пока не найдет то, чья "голова" унифицируется с данным запросом. Механизм Пролога не должен далеко смотреть в качестве первого предложения, этот факт:
ackermann(0, N, s(N)).
унифицирует, связав M = 0 и N = s(0) как уже было описано как первый успех.
Если вас попросят вернуться, например. когда пользователь вводит точку с запятой, механизм Пролога проверяет, есть ли альтернативный способ выполнить это первое предложение. Нет. Затем механизм Prolog пытается выполнить следующие предложения для 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
Но чтобы добиться успеха, механизм Пролога также должен удовлетворять телу второго предложения, которое теперь выглядит следующим образом:
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 , создавая (по знакомой логике) под-под-под-подцель:
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, не позволяют добиться успеха второй подцели тела третьего предложения. Поэтому механизм Пролога пытается найти решения, удовлетворяющие третьему пункту. Но очевидно, что теперь это переходит в бесконечную рекурсию, так как третье предложение объединится в своем заголовке, но тело третьего предложения будет повторять точно такой же поиск, который мы только что выполнили. Таким образом, механизм Пролога теперь бесконечно углубляется в тело третьего предложения.
person
hardmath
schedule
26.06.2011
