How can I memorize terms on a tree in Prolog?
I thought my reasoning was fine but nodes like commutation keeps adding creating more nodes with the same previous value, the program works but I would like to stop these nodes from being created.
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)).
example query:
proof( eq( and(t,and(t,f)), and(and(t,t),f) ) ,6).
Apparently the problem is that I was assuming semicolons to be shortcircuited like || in C++ code, in consequence the terms after the ; were being evaluated even if the previous propositions were evaluated to false, so prepending a cut operator fixed the problem.
More errors might appear as I am new to the language, here is an example of the solution, writeln messages helped to see the problem, trace could have helped too.
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)).