I'm writing a trivial metainterpreter in Prolog for self-education. Basically I want to carry along the "probability" of a given solution. To do this I just declare the probability of my clause being correct. I expect if this works I will extend it with a better foundation but for now I'm just interested in solving the immediate problem, which is that my metainterpreter loops:
Code:
fuzzy_prove(true, 1.0) :- !.
fuzzy_prove(probability(P), P) :- !.
fuzzy_prove((A,B), Prob) :-
fuzzy_prove(A, P1),
fuzzy_prove(B, P2),
Prob is P1 * P2.
fuzzy_prove(A, P) :-
clause(A, B), fuzzy_prove(B, P).
father(dave, jean).
father(dave, don) :- probability(0.5).
father(don, claudia).
father(don, jimmy) :- probability(0.5).
father(jean, davey).
grandfather(Grandpop, Babs) :-
father(Grandpop, Dad),
father(Dad, Babs).
My queries seem at first to work:
?- fuzzy_prove(grandfather(X, Z), Prob).
X = dave,
Z = davey,
Prob = 1.0 ;
X = dave,
Z = claudia,
Prob = 0.5 ;
X = dave,
Z = jimmy,
Prob = 0.25 ;
When I ask for the next solution, I get crazy looping. If I interrupt it, it looks like this:
continue (trace mode)
Call: (3,973,299) fuzzy_prove(call((father(_G3, _G28), father(_G28, _G4))), _G5) ?
^ Call: (3,973,300) clause(call((father(_G3, _G28), father(_G28, _G4))), _G2044) ?
^ Exit: (3,973,300) clause(call((father(_G3, _G28), father(_G28, _G4))), call((father(_G3, _G28), father(_G28, _G4)))) ?
Call: (3,973,300) fuzzy_prove(call((father(_G3, _G28), father(_G28, _G4))), _G5) ?
^ Call: (3,973,301) clause(call((father(_G3, _G28), father(_G28, _G4))), _G2051) ?
^ Exit: (3,973,301) clause(call((father(_G3, _G28), father(_G28, _G4))), call((father(_G3, _G28), father(_G28, _G4)))) ?
Call: (3,973,301) fuzzy_prove(call((father(_G3, _G28), father(_G28, _G4))), _G5) ?
^ Call: (3,973,302) clause(call((father(_G3, _G28), father(_G28, _G4))), _G2058) ?
^ Exit: (3,973,302) clause(call((father(_G3, _G28), father(_G28, _G4))), call((father(_G3, _G28), father(_G28, _G4)))) ?
Call: (3,973,302) fuzzy_prove(call((father(_G3, _G28), father(_G28, _G4))), _G5) ?
^ Call: (3,973,303) clause(call((father(_G3, _G28), father(_G28, _G4))), _G2065) ?
^ Exit: (3,973,303) clause(call((father(_G3, _G28), father(_G28, _G4))), call((father(_G3, _G28), father(_G28, _G4)))) ?
Call: (3,973,303) fuzzy_prove(call((father(_G3, _G28), father(_G28, _G4))), _G5) ?
^ Call: (3,973,304) clause(call((father(_G3, _G28), father(_G28, _G4))), _G2072) ?
^ Exit: (3,973,304) clause(call((father(_G3, _G28), father(_G28, _G4))), call((father(_G3, _G28), father(_G28, _G4)))) ?
I'm sure I'm doing something obviously stupid but I'm having trouble seeing what it is.
Your clause with (,) functors matches twice: both the 3rd and 4th clauses of fuzzy_prove, when it matches the 4th clause it will eventually loop infinitely because the clause body is itself an and and cannot be simplified.
This query will demonstrate what is happening:
clause(grandfather(A,B), C0), clause(C0, C1), clause(C1, C2).
On my interpreter at least C1 = C2, and we have an infinite loop.
You need at least to check that the functor of your clause body is not (,) before recursing. I suspect there will be other corner cases like this so it may in fact be better to work out how to handle the call functor correctly.