Невозможно остановить создание узлов Prolog путем кэширования/запоминания
Как я могу запомнить термины на дереве в Прологе?
Я думал, что мои рассуждения в порядке, но такие узлы, как коммутация, продолжают добавлять новые узлы с тем же предыдущим значением, программа работает, но я хотел бы остановить создание этих узлов.
name(Term,X) :- Term=..[X|_].
prop(eq,commutative).
prop(and,commutative).
prop(and,associative).
prop(Op,P):-compound(Op),name(Op,Opname),prop(Opname,P).
identity(A,A). %checks if both are the same, or returns the same in any parameter
commute(A,B):- A=..[N,X,Y], B=..[N,Y,X]. %true if B is commutation of A, or B outputs commutation of A
associate(X,Y):- X=..[N,A,B],B=..[N,BA,BB], Y=..[N,C,BB],C=..[N,A,BA].
:- dynamic proofcache/1.
proof(_,Steps) :- Steps<1, !, false.
proof(eq(A,B),Steps) :- identity(A,B),writeln(["id",A," = ",B,Steps]),!,true.
proof(eq(A,B),Steps) :- prop(A,commutative), (proofcache(eq(A,B));asserta(proofcache(eq(A,B))), commute(A,R),writeln(["comm",A," = ",R,Steps]), proof(eq(R,B),Steps-1)).
proof(eq(A,B),Steps) :- prop(A,associative), (proofcache(eq(A,B));asserta(proofcache(eq(A,B))), associate(A,R),writeln(["assoc",A," = ",R,Steps]), proof(eq(R,B),Steps-1)).
пример запроса:
proof( eq( and(t,and(t,f)), and(and(t,t),f) ) ,6).
Если вы можете получить доступ к книге Срок переписывания и все такое Баадера и Нипкова, это должно заполнить пробелы. Вы также можете попробовать перенести это на сайт КС,
Поиск термин, переписывающий пролог обнаружил это с загружаемым кодом Prolog. Не делается так, как вы это делали, поэтому вам придется научиться его использовать, но это может вам помочь.
Если вы не можете получить Term rewriting and all that, взгляните на Вкус переписываемых систем
У меня возникает соблазн назначить за это награду в 500 баллов, но не думаю, что кто-то, кто часто посещает тег, ответит на это, и я потеряю 500 баллов. Ответ для очков должен был бы реализовать систему перезаписи терминов на Прологе, чтобы решить эту проблему.
Термин «система перезаписи» должен быть слитным и заканчиваться во всех случаях или объяснять, почему это невозможно для данных правил. Ответ о простом исправлении Пролога не будет принят. Он также должен работать с SWI-Prolog 8.x.
спасибо @GuyCoder Я думаю, что моя проблема была как-то связана с оператором cut, который я только что научился прологировать, и я предполагал, что запятые и точки с запятой каким-то образом работают как короткозамкнутые ands и ors, но, видимо, это не так, это могло бы быть хорошо, если бы они существовали в формах других операторов и не нужно полагаться на оператора разреза, еще раз спасибо, Гай.
Пожалуйста, опубликуйте свой ответ, я хотел бы его увидеть.
конечно, если таких ошибок больше не будет, я буду редактировать, когда буду больше изучать язык.
Опубликуйте то, что у вас есть в вашем вопросе, и мы можем посмотреть на него на наличие возможных ошибок.
Ответы 1
По-видимому, проблема в том, что я предполагал, что точки с запятой будут сокращены, как || в коде C++, в результате чего термины после ; оценивались, даже если предыдущие предложения были оценены как ложные, поэтому добавление оператора cut решило проблему.
Поскольку я новичок в языке, могут появляться другие ошибки, вот пример решения, writeln сообщения помогли увидеть проблему, trace тоже могли бы помочь.
proof(eq(A,B),Steps) :- prop(A,commutative),
(proofcache(eq(A,B),comm), writeln(["comm was cached",eq(A,B),Steps]), !;
asserta(proofcache(eq(A,B),comm)), writeln(["comm was not cached",eq(A,B),Steps]),
commute(A,R), writeln(["comm",A," = ",R,Steps]),
proof(eq(R,B),Steps-1)).
Это скорее предположение или куда бы я лично посмотрел, если бы это был мой комментарий о проблеме, но лучше, чем ничего. Это пахнет проблемой типа Абстрактная система перезаписи, а не проблемой Пролога. Я хочу сказать, что это проблема слияние, но, не углубляясь в это, это не кажется правильным для того, что вы описываете.