In previous question, we built a simple forward chaining in Prolog together with the user slago, and solved some problems about it. Code for forward chaining:
:- op(1100, xfx, if).
:- op(1000, xfy, or).
:- op(900, xfy, and).
forward(Facts) :-
fixed_point(nil, [true], Facts). % Start with the base with only true
fixed_point(Base, Base, Base) :- !. % Reached a fixpoint
fixed_point(_, Base, Facts) :- % Base =/= Facts => not a fixpoint
setof(Fact, derived(Fact, Base), NewFacts), % Derive new facts
ord_union(NewFacts, Base, NewBase), % Add new facts to base
fixed_point(Base, NewBase, Facts). % Repeat with new base
derived(Fact, Base) :-
rule(Fact if Condition), % Match a rule
satisfy(Base, Condition). % Verify if condition is satisfied given base
satisfy(Base, G and Gs) :- % Condition is a conjunction
!,
member(G, Base),
satisfy(Base, Gs).
satisfy(Base, G or Gs) :- % Condition is a disjunction
!,
( member(G, Base)
; satisfy(Base, Gs) ).
satisfy(_, callp(X)) :- % Condition is a callable fact
!,
call(X).
satisfy(Base, Condition) :- % Condition is an atomic proposition
member(Condition, Base).
Simple knowledge base to test it:
rule(eats_flies(fritz) if true).
rule(croaks(fritz) if true).
rule(eats_flies(frotz) if true).
rule(croaks(frotz) if true).
rule(sings(tweety) if true).
rule(chips(tweety) if true).
rule(has_wings(tweety) if true).
rule(croaks(krogr) if true).
rule(chips(kroger) if true).
rule(canary(X) if and(sings(X),chips(X),has_wings(X))).
rule(frog(X) if and(croaks(X),eats_flies(X))).
rule(green(X) if frog(X)).
rule(yellow(X) if canary(X)).
rule(node(a) if true).
rule(node(b) if true).
rule(node(c) if true).
rule(node(d) if true).
rule(node(e) if true).
rule(connected(a,b) if true).
rule(connected(b,c) if true).
rule(connected(c,d) if true).
rule(connected(d,e) if true).
rule(funny(c,d) if true).
rule(wonderful(X,Y) if or(nice(X,Y),funny(X,Y))).
rule(connected(X,Z) if and(connected(X,Y),connected(Y,Z))).
rule(path([Node|[]]) if node(Node)).
rule(path([Node, NextNode|Nodes]) if and(connected(Node, NextNode),path([NextNode|Nodes]))).
rule(int(1) if true).
rule(int(0) if true).
rule(int(2) if true).
rule(iszero(X) if and(int(X), callp(X = 0))).
rule(has_at_least_n([_|Tail], 0) if true).
rule(has_at_least_n([X|Tail], N) if and(node(X), callp(NewN is N-1), has_at_least_n(Tail, NewN))).
rule(has_at_least_n([X|Tail], N) if and(has_at_least_n(Tail, N))).
Now I would like to solve a problem with the last rules about lists. I would like to be able to count the elements of a list. So I would like to be able to say, for example, that the list:
[a,b,c,d,e]
has at least 5 nodes, and a list like:
[a,x,y,c,d]
has not 5 nodes
with the rule I built, the forward loops itself by finding every time a fact like:
has_at_least_n([_|_], 0)
since every time it can unify that _ with anything.
Any tips on how should I handle this case? How can I have rules on lists avoiding infinite loops?
Still my forward is not able to find any other rule different from the dummy one with the has_at_least_n([_|_], 0).
Using gtrace for debugging, I found out that, if the and or the or have more than two facts inside the brackets, it is not recognized as satisfy(Base, G and Gs) / satisfy(Base, G or Gs), but only satisfy(Base, Condition), and of course the member(Condition, Base) is false since and(..., ..., ..., ...) is not in Base.
When there are just two facts, instead, I see in the debugger that they have a different representation : fact1 and fact2
And this matches the rule.
As I suggested before, a possible solution is as follows:
:- op(1100, xfx, if).
:- op(1000, xfy, or).
:- op(900, xfy, and).
forward(Steps, FinalBase) :-
forward_iteration(Steps, nil, [true], FinalBase). % Current base is [true]
forward_iteration(Steps, PreviousBase, CurrentBase, FinalBase) :-
( ( Steps = 0 % Reached max iterations
; PreviousBase = CurrentBase ) % Reached a fixed point
-> FinalBase = CurrentBase
; setof(Fact, derived(Fact, CurrentBase), NewFacts), % Derive new facts
ord_union(NewFacts, CurrentBase, NewBase), % Add new facts into current base
succ(Steps0, Steps),
forward_iteration(Steps0, CurrentBase, NewBase, FinalBase) ). % Repeat with new base
derived(Fact, Base) :-
rule(Fact if Condition), % Match a rule
satisfy(Base, Condition). % Condition holds in current base
satisfy(Base, G and Gs) :- % Condition is a conjunction
!,
member(G, Base),
satisfy(Base, Gs).
satisfy(Base, G or Gs) :- % Condition is a disjunction
!,
( member(G, Base)
; satisfy(Base, Gs) ).
satisfy(_Base, call(Fact)) :- % Condition is a callable fact
!,
call(Fact).
satisfy(Base, Condition) :- % Condition is an atomic proposition
member(Condition, Base).
Note that and is a binary operator, not an arbitrary arity functor! So, for example, we can define len/2 as:
rule(item(X) if call(member(X, [a,b,c]))).
rule(len([], 0) if true).
rule(len([H|T], N) if len(T,M) and item(H) and call(succ(M,N))).
Running examples:
?- forward(1, FinalBase), maplist(writeln, FinalBase).
true
item(a)
item(b)
item(c)
len([],0)
FinalBase = [true, item(a), item(b), item(c), len([], 0)].
?- forward(2, FinalBase), maplist(writeln, FinalBase).
true
item(a)
item(b)
item(c)
len([],0)
len([a],1)
len([b],1)
len([c],1)
FinalBase = [true, item(a), item(b), item(c), len([], 0), len([a], 1), len([b], 1), len([...], 1)].
?- forward(3, FinalBase), maplist(writeln, FinalBase).
true
item(a)
item(b)
item(c)
len([],0)
len([a],1)
len([a,a],2)
len([a,b],2)
len([a,c],2)
len([b],1)
len([b,a],2)
len([b,b],2)
len([b,c],2)
len([c],1)
len([c,a],2)
len([c,b],2)
len([c,c],2)
FinalBase = [true, item(a), item(b), item(c), len([], 0), len([a], 1), len([a|...], 2), len([...|...], 2), len(..., ...)|...].