Доказательство в качестве выходного аргумента в мета-интерпретаторе Prolog

Question

Я собираю простой мета-интерпретатор, который выводит шаги доказательства. У меня проблемы с получением шагов доказательства в качестве выходного аргумента. Мой предикат explain1 возвращает подробное доказательство, которое мне хотелось бы, но не в качестве выходного аргумента. Мой предикат explain2 возвращает доказательство в качестве выходного аргумента, но не с уровнем детализации, который мне нужен. Можно ли изменить explain2 так, чтобы он выдавал столько же информации, сколько explain1? Мне не нужно выводить текст «Объяснение ...» и «Объяснение ...», только фактические объяснения и объяснения.

Игрушечные данные в нижней части программы («если они здоровы и богаты, то счастливы») являются лишь примером, и идея состоит в том, чтобы иметь базу данных с большим количеством фактов о других вещах. Я хочу попытаться создать предикат, который принимает эффект, например, happy(john) и возвращает объяснение этому. Таким образом, аргумент E explain должен быть введен пользователем; таким образом, другой запрос может быть explain(_, smokes(mary), _) и так далее. Я не могу получить то, что хочу, непосредственно из переменных C и E в объяснении, потому что я хочу, чтобы программа выводила шаги в процессе проверки, где C и E меняются, например, "богатый и здоровый, такой счастливый; побеждает такой богатый; ИСТИННЫЙ такой богатый; ИСТИННЫЙ такой счастливый" и так далее. То есть вернуть все причинно-следственные связи, которые приводят к эффекту.

На отличном сайте Маркуса Триски есть некоторые подробности об этом, но у меня возникают проблемы с адаптацией этого кода к моей проблеме.

Любая помощь будет принята с благодарностью!

Спасибо / JCR

Моя программа:

main1:-explain1(_, happy(john), _), fail.
main2:-explain2(_, happy(john), _, T), writeln(T), fail.

explain1(C, E, P):-
    C = ['True'],
    p(C, E, P),
    write('Explaining '), write(E), 
    write('. An explanation is: '), write(C), 
    write(' with probability '), write(P), nl.
explain1(C, E, P):-
    p(C, E, P),
    not(C = ['True']),
    write('Explaining '), write(E), 
    write('. An explanation is: '), write(C), 
    write(' with probability '), write(P), nl.
explain1(C, E, P):-
    p(C0, E, P0),
    maplist(explain1, C1, C0, P1),
    flatten(C1, C),
    append([P0], P1, P2),
    flatten(P2, P3),
    foldl(multiply, P3, 1, P),
    write('Explaining '), write(E), 
    write('. An explanation is: '), write(C), 
    write(' with probability '), write(P), nl.

explain2(C, E, P, T):-
    C = ['True'],
    p(C, E, P),
    T = [C, E, P].
explain2(C, E, P, T):-
    p(C, E, P),
    not(C = ['True']),
    T = [C, E, P].
explain2(C, E, P, T):-
    p(C0, E, P0),
    maplist(explain2, C1, C0, P1, _),
    flatten(C1, C),
    append([P0], P1, P2),
    flatten(P2, P3),
    foldl(multiply, P3, 1, P),
    T = [C, E, P].

multiply(V1, V2, R) :- R is V1 * V2.

p(['True'], wins(john), 0.7).
p([wins(john)], rich(john), 0.3).
p(['True'], healthy(john), 0.9).
p([rich(john), healthy(john)], happy(john), 0.6).

Вывод main1:

Explaining happy(john). An explanation is: [rich(john), healthy(john)] with probability 0.6
Explaining rich(john). An explanation is: [wins(john)] with probability 0.3
Explaining healthy(john). An explanation is: [True] with probability 0.9
Explaining happy(john). An explanation is: [wins(john), True] with probability 0.162
Explaining wins(john). An explanation is: [True] with probability 0.7
Explaining rich(john). An explanation is: [True] with probability 0.21
Explaining healthy(john). An explanation is: [True] with probability 0.9
Explaining happy(john). An explanation is: [True, True] with probability 0.1134

Выход main2:

[[rich(john), healthy(john)], happy(john), 0.6]
[[wins(john), True], happy(john), 0.162]
[[True, True], happy(john), 0.1134]

Answer 1

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

Вы можете думать оcall/1 в качестве прототипа интерпретатора для Пролога, потому что он просто доказывает единственную цель.Похоже, что API, который вы хотите, похож на prove(+Goal, -Proof), где Goal доказывается точно так же, как и с call/1, но вы получаете вторую вещь, доказательство какого-то рода.

Когда нормальноПролог видит выражение вроде Goal1, Goal2, можно подумать, что оно расширилось до call(Goal1), call(Goal2).Так что же делает вместо этого ваш корректор-метадейтер в этой ситуации?Он должен доказать обе цели, а затем каким-то образом объединить эти «подзаголовки».

Все это наводит меня на мысль о том, что чего-то не хватает в вашей концепции: какова структура доказательства?Я бы много думал о том, что вы собираетесь вернуть, потому что, если вам не нужна строка, вам нужно что-то, что вы можете пройти легче.Вероятно, в результате будет иметь древовидную структуру, аналогичную той, что делает Пролог (за исключением случаев, когда нет ветвей с ошибками).Таким образом, я ожидаю, что он будет иметь некоторую степень вложенности, и он, безусловно, может каким-то образом «напоминать» стек вызовов, хотя я ожидаю, что это ограничит его полезность для вас (как вы собираетесь бесполезно обходить это дерево для общего запроса?).

Давайте рассмотрим ваш базовый случай.Это, вероятно, что-то вроде этого:

prove(true, true) :- !.

Истинно истинно, потому что оно истинно.

Следующий случай, который меня заинтересует, это "и".

prove((G1, G2), (P1, P2)) :- 
   !,
   prove(G1, P1), 
   prove(G2, P2).

Это выглядит довольно тавтологически, но ключевая идея на самом деле заключается в том, что мы объединяем доказательства G1 и G2 с (P1, P2) в доказательстве.

Следующий случай будет "или", вероятно:

prove((G1;_), P1) :- prove(G1, P1).
prove((_;G2), P2) :- !, prove(G2, P2).

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

Наконец, мы должны обработать встроенные функции и пользовательские предикаты, за вопрос, который я задал некоторое время назад :

prove(H, subproof(H, Subproof)) :- clause(H, Body), prove(Body, Subproof).
prove(H, builtin(H)) :- call(H).

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

mortal(X) :- man(X).
man(socrates).

Вот запрос:

?- prove((member(X, [bread,socrates]), mortal(X)), Proof).
X = socrates,
Proof =  (builtin(member(socrates, [bread, socrates])), 
          subproof(mortal(socrates), 
                   subproof(man(socrates), true))) 

По причинам, которые я пока не понимаю, использованиеmember/2 будет бомбить второй запрос.Я открыл вопрос об этом на форуме SWI и обновлю этот ответ, когда узнаю, что там происходит.

Обновление.Эта проблема связана с автозагрузкой library(lists), которая происходит при использовании member/2.При первом вызове member/2 не имеет предложений, поэтому он вводит call/1, который вызывает автозагрузчик, а затем вызывает его как встроенный.При следующей попытке у member/2 есть предложения, но их тела содержат предикаты в модуле lists, и этот метаинтерпретатор не обрабатывает модули должным образом.Быстрое и грязное решение состоит в том, чтобы заменить третий пункт следующим образом:

prove(H, subproof(H, Subproof)) :- 
   \+ predicate_property(H, imported_from(_)), 
   clause(H, Body), 
   prove(Body, Subproof).

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