Бесконечное дерево успеха или нет?

Question

Я дал следующую программу:

edge(a,b). 
edge(b,c). 
edge(a,d). 

path(N,M):- path(N,New),edge(New,M). 
path(N,M):- edge(N,M). 

И спросил, если при применении алгоритма доказательства дерева к следующему запросу:

?- path(a,X). 

дерево доказательства бесконечное дерево успеха, или бесконечное дерево отказа?

Теперь, как я понимаю, во время строительства дерева, вы застряли в применении правила 1 путь снова и снова, создавая бесконечное дерево и никогда не получить, чтобы исключить 2 из пути ..

таким образом, создавая бесконечное дерево отказов. но решение, которое я имею в виду, это бесконечное дерево успеха, мой вопрос: правильно ли я, или мой профессор? :]

Answer 1

Я бы назвал это бесконечным циклом. Посмотрите на след:

?- trace, path(a,X). 
Call: (7) path(a, _G394) ? 
Call: (8) path(a, _G511) ? 
Call: (9) path(a, _G511) ? 
Call: (10) path(a, _G511) ? 
... 
Call: (147) path(a, _G511) ? 
Call: (148) path(a, _G511) ? 
... 
ERROR: Out of local stack 

Я не знаком с этими условиями, но я мог бы использовать его. Никаких решений не производится, поэтому мне было бы трудно утверждать, что это бесконечное дерево успеха. Даже учитывая бесконечное время и пространство, это никогда не создаст успешного решения. В то же время неудача в смысле Prolog является непосредственной, и это тоже не происходит. Я не уверен, что такая вещь, как бесконечное дерево отказов, может существовать, если только вы не назовете что-то, что порождает бесконечное количество точек выбора, все из которых терпят неудачу. Но здесь нет никаких сбоев. Было бы более честно просто называть это тем, чем он на самом деле является: бесконечный цикл. Такие вещи существуют вне сферы успеха и неудачи. Вот почему в Haskell ⊥ принадлежит к каждому типу. Может быть, в этом смысле вы оба правы.

Answer 2

Не уверен, что терминология используется, но общая терминология - как используется Ллойд, Основы логического программирования, является SLD-дерево, которое может содержать успех, бесконечное и ветви отказов. И я предполагаю, что вы используете стандартное правило вычисления Prolog (= выберите самый левый атом).

Дерево SLD в вашем примере бесконечно и содержит конечное количество ветвей успеха, соответствующих трем ответам ответа: X = b ; X = c ; X = d. Важно отметить, что, хотя это дерево имеет бесконечную ветвь отказа, оно тем не менее содержит все решения!

Самый выбор правила расчета может влиять на размер и структуру дерева SLD. Но самое приятное: независимо от вашего правила вычисления мы получим наши ветви успеха! Гарантированы! Ehm, гарантированный для тех, кто умеет рисовать бесконечное SLD-дерево, и умеет использовать ... мудро. Но для людей с бесконечным ресурсом и проницательностью нет проблем.

Другое наблюдение заключается в том, что форма этого SLD-дерева довольно независима от порядка предложений. Итак, независимо от того, записано ли нерекурсивное правило последним (как в вашем случае) или первым, не имеет большого значения для формы дерева: он будет иметь одинаковый размер (либо бесконечный, либо оба конечный), будет содержать то же количество узлов, но некоторые ветки появятся в другом порядке.

Prolog пытается произвести это дерево SLD пошагово, но использует самый примитивный способ сделать это. Он начинает исследовать ветку и исследует ее полностью, прежде чем расширять другие ветви.Это означает, что Prolog может использовать чрезвычайно пространственное представление дерева SLD (или, если быть точнее: только части дерева SLD), на самом деле это, по сути, стек, но цена за оплату заключается в том, что Когда встречается бесконечная ветвь, вы застряли - если только вы не имеете бесконечного ресурса. И порядок предложений будет иметь эффект, будут ли найдены ветви успеха (= ответы) или они будут похоронены какой-то бесконечной ветвью.

На практике довольно сложно визуализировать все эти бесконечные деревья, мы не так хорошо привыкли к ним.

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

Центральное понятие здесь Универсальное окончание запроса/цели, говорящего в SLD-деревьях, означает: конечность всех ветвей.

Это очень легко заметить всеобщее прекращение цели: просто выполнить Goal,false вместо этого.

И что же это такое false делать с нашим SLD-деревом? По существу, у нас есть бесконечная или конечная ветвь отказа только. Все ответы исчезли.

Теперь все становится еще лучше: мы можем ввести false в вашу программу. Полученная программа называется failure-slice. Хотя эта программа уже не совпадает с исходной программой, имеет место следующее свойство: если срез отказа не заканчивается (= имеет бесконечную ветвь), также исходная программа не заканчивается (= имеет бесконечную ветвь).

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

 
?- path(a,X), false. 

edge(a,b) :- false. 
edge(b,c) :- false. 
edge(a,d) :- false. 

path(N,M):- path(N,New), false, edge(New,M). 
path(N,M):- false, edge(N,M). 

Опытные программисты Prolog просто увидеть этот крохотный фрагмент программы, который гораздо легче понять. Они не тратят свое время на воображение бесконечных ветвей и не представляют себе фактическое выполнение Пролога — ну, может быть, немного, но только для фрагмента, а не для всей программы.

В некотором смысле, false уже показывает нам правила вычисления: Все на правой стороне false это штриховка через.

Вы также можете научиться «видеть» это, просто следуйте this link.