Learning Peano successor/ predeessor functions.

:-module(pred_succ, [background_knowledge/2
                    ,metarules/2
                    ,positive_example/2
                    ,negative_example/2
                    ]).

/** <module> Learning Peano successor and predecessor functions.

Learning queries:

==
?- learn(s/2).
s(0,s(A)).
s(A,B):-s_(A,B).
s(A,B):-s_(A,C),s(C,B).
true.

?- learn(p/2).
p(s(A),0).
p(A,B):-p_(A,B).
p(A,B):-p_(A,C),p(C,B).
true.
==

*/

% Eliminates left-recursive clauses that make it harder for Prolog to
% run the learned hypothesis.
configuration:metarule_constraints(M,fail):-
    M =.. [m,Id,P|Ps]
    ,Id \= projection
    ,left_recursive(P,Ps).

left_recursive(T,[T|_Ps]):-
    !.
left_recursive(T,[T,T|_Ps]):-
    !.


metarules(s/2, [identity,chain]).
metarules(p/2, [identity,chain]).

background_knowledge(s/2, [s_/2]).
background_knowledge(p/2, [p_/2]).

positive_example(s/2, E):-
        member(E,[s(0,s(_))
                 ,s(0,s(0))
                 ,s(s(0),s(s(s(s(0)))))
               ]).
positive_example(p/2, E):-
        member(E,[p(s(_),0)
                 ,p(s(0),0)
                 ,p(s(s(s(s(0)))),s(0))
               ]).

negative_example(s/2, _):-
    fail.
negative_example(p/2, _):-
        fail.

s_(N,s(N)).

p_(s(N),N).