What're the constraints of mutual recursion in PI?
Closed this issue · 0 comments
yangdinglou commented
Hi, I'm learning something with mutual recursion. The force ordering at https://github.com/logic-and-learning-lab/Popper/blob/main/popper/lp/alan.pl#L714 is already commented out, but some valid mutual recursive programs are not found.
For example, a simple example of even/odd is here
%% intended
% even(X):- zero(X).
% even(X):- prev(X, Y), inv1(Y).
% inv1(X):- prev(X, Y), even(Y).
%% bias
max_vars(2).
max_body(2).
max_clauses(3).
enable_recursion.
enable_pi.
head_pred(even,1).
body_pred(zero,1).
body_pred(prev,2).
body_pred(succ,2).
:-
not clause(1).
:-
not clause(2).
:-
head_literal(0,P,_,_),
not head_literal(1,P,_,_).
:-
head_literal(1,P,_,_),
head_literal(2,P,_,_).
:-
not head_literal(2, _, 1, _).
%% bk
succ(A,B):-
B is A+1.
prev(A,B):-
B is A-1.
zero(0).
%% ex
pos(even(0)).
pos(even(2)).
pos(even(4)).
neg(even(1)).
Then no valid model is found. May I know what's the reason?