%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                                      %
%   Prolog programs from Chapter 9 of the book         %
%   SIMPLY LOGICAL: Intelligent reasoning by example   %
%   (c) Peter A. Flach/John Wiley & Sons, 1994.        %
%                                                      %
%   Predicates: induce/2,3                             %
%               theta_subsumes/2                       %
%               anti_unify/3                           %
%               theta_lgg/3                            %
%                                                      %
%   NB. This file needs predicates defined in          %
%   the file 'library'.                                %
%                                                      %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%% 9.1  Generalisation and specialisation %%%

theta_subsumes((H1:-B1),(H2:-B2)):-
	\+((H1=H2,ground(B2),
	     \+(subset(B1,B2)))).

ground(Term):-
	numbervars(Term,0,N).


:-op(600,xfx,'<-').

anti_unify(Term1,Term2,Term):-
	anti_unify(Term1,Term2,Term,[],S1,[],S2).

anti_unify(Term1,Term2,Term1,S1,S1,S2,S2):-
	Term1 == Term2,!.
anti_unify(Term1,Term2,V,S1,S1,S2,S2):-
	subs_lookup(S1,S2,Term1,Term2,V),!.
anti_unify(Term1,Term2,Term,S10,S1,S20,S2):-
	nonvar(Term1),nonvar(Term2),
	functor(Term1,F,N),functor(Term2,F,N),!,
	functor(Term,F,N),
	anti_unify_args(N,Term1,Term2,Term,S10,S1,S20,S2).
anti_unify(Term1,Term2,V,S10,[Term1<-V|S10],S20,[Term2<-V|S20]).

anti_unify_args(0,Term1,Term2,Term,S1,S1,S2,S2).
anti_unify_args(N,Term1,Term2,Term,S10,S1,S20,S2):-
	N>0,N1 is N-1,
	arg(N,Term1,Arg1),
	arg(N,Term2,Arg2),
	arg(N,Term,Arg),
	anti_unify(Arg1,Arg2,Arg,S10,S11,S20,S21),
	anti_unify_args(N1,Term1,Term2,Term,S11,S1,S21,S2).

subs_lookup([T1<-V|Subs1],[T2<-V|Subs2],Term1,Term2,V):-
	T1 == Term1,
	T2 == Term2,!.
subs_lookup([S1|Subs1],[S2|Subs2],Term1,Term2,V):-
	subs_lookup(Subs1,Subs2,Term1,Term2,V).

% ?-anti_unify(2*2=2+2,3*2=3+3,T,[],S1,[],S2).
% T = X*2=X+X
% S1 = [2<-X]
% S2 = [3<-X]



theta_lgg((H1:-B1),(H2:-B2),(H:-B)):-
	anti_unify(H1,H2,H,[],S10,[],S20),
	theta_lgg_bodies(B1,B2,[],B,S10,S1,S20,S2).

theta_lgg_bodies([],B2,B,B,S1,S1,S2,S2).
theta_lgg_bodies([L|B1],B2,B0,B,S10,S1,S20,S2):-
	theta_lgg_literal(L,B2,B0,B00,S10,S11,S20,S21),
	theta_lgg_bodies(B1,B2,B00,B,S11,S1,S21,S2).

theta_lgg_literal(L1,[],B,B,S1,S1,S2,S2).
theta_lgg_literal(L1,[L2|B2],B0,B,S10,S1,S20,S2):-
	same_predicate(L1,L2),
	anti_unify(L1,L2,L,S10,S11,S20,S21),
	theta_lgg_literal(L1,B2,[L|B0],B,S11,S1,S21,S2).
theta_lgg_literal(L1,[L2|B2],B0,B,S10,S1,S20,S2):-
	\+(same_predicate(L1,L2)),
	theta_lgg_literal(L1,B2,B0,B,S10,S1,S20,S2).

%%% same_predicate/2: see file 'library'

% theta_lgg((element(c,[b,c]):-[element(c,[c])]),
%           (element(d,[b,c,d]):-[element(d,[c,d]),element(d,[d])]),
%           C).
% C = element(X,[b,c|Y]):-[element(X,[X]),element(X,[c|Y])]

/*==================================================================*/

%%% 9.2  Bottom-up induction %%%

induce_rlgg(Exs,Clauses):-
	pos_neg(Exs,Poss,Negs),
	bg_model(BG),
	append(Poss,BG,Model),
	induce_rlgg(Poss,Negs,Model,Clauses).

induce_rlgg(Poss,Negs,Model,Clauses):-
	covering(Poss,Negs,Model,[],Clauses).

% split positive and negative examples
pos_neg([],[],[]).
pos_neg([+E|Exs],[E|Poss],Negs):-
	pos_neg(Exs,Poss,Negs).
pos_neg([-E|Exs],Poss,[E|Negs]):-
	pos_neg(Exs,Poss,Negs).

% covering algorithm
covering(Poss,Negs,Model,H0,H):-
	construct_hypothesis(Poss,Negs,Model,Hyp),!,
	remove_pos(Poss,Model,Hyp,NewPoss),
	covering(NewPoss,Negs,Model,[Hyp|H0],H).
covering(P,N,M,H0,H):-
	append(H0,P,H).	% add uncovered examples to hypothesis

% remove covered positive examples
remove_pos([],M,H,[]).
remove_pos([P|Ps],Model,Hyp,NewP):-
	covers_ex(Hyp,P,Model),!,
	write('Covered example: '),write(P),nl,
	remove_pos(Ps,Model,Hyp,NewP).
remove_pos([P|Ps],Model,Hyp,[P|NewP]):-
	remove_pos(Ps,Model,Hyp,NewP).


% extensional coverage, relative to a ground model
covers_ex((Head:-Body),Example,Model):-
	try((Head=Example,forall(element(L,Body),element(L,Model)))).

% construct a clause by means of RLGG
construct_hypothesis([E1,E2|Es],Negs,Model,Clause):-
	write('RLGG of '),write(E1),write(' and '),write(E2),write(' is'),
	rlgg(E1,E2,Model,Cl),
	reduce(Cl,Negs,Model,Clause),!,
	nl,write('  '),write(Clause),nl.
construct_hypothesis([E1,E2|Es],Negs,Model,Clause):-
	write(' too general'),nl,
	construct_hypothesis([E2|Es],Negs,Model,Clause).


% rlgg(E1,E2,M,C) <- C is RLGG of E1 and E2 relative to M
rlgg(E1,E2,M,(H:-B)):-
	anti_unify(E1,E2,H,[],S10,[],S20),
	varsin(H,V),	% determine variables in head of clause
	rlgg_bodies(M,M,[],B,S10,S1,S20,S2,V).

rlgg_bodies([],B2,B,B,S1,S1,S2,S2,V).
rlgg_bodies([L|B1],B2,B0,B,S10,S1,S20,S2,V):-
	rlgg_literal(L,B2,B0,B00,S10,S11,S20,S21,V),
	rlgg_bodies(B1,B2,B00,B,S11,S1,S21,S2,V).

rlgg_literal(L1,[],B,B,S1,S1,S2,S2,V).
rlgg_literal(L1,[L2|B2],B0,B,S10,S1,S20,S2,V):-
	same_predicate(L1,L2),
	anti_unify(L1,L2,L,S10,S11,S20,S21),
        varsin(L,Vars),
        var_proper_subset(Vars,V),   % no new variables in literal
	!,rlgg_literal(L1,B2,[L|B0],B,S11,S1,S21,S2,V).
rlgg_literal(L1,[L2|B2],B0,B,S10,S1,S20,S2,V):-
	rlgg_literal(L1,B2,B0,B,S10,S1,S20,S2,V).

% remove redundant literals
reduce((H:-B0),Negs,M,(H:-B)):-
        reduce_ground(B0,M,B1),
/*	setof0(L,(element(L,B0),not(var_element(L,M))),B1), */
	reduce_negs(H,B1,[],B,Negs,M).

/* For Poplog Prolog */
reduce_ground([],_,[]) :- !.
reduce_ground([L|T],M,V) :- var_element(L,M), !, reduce_ground(T,M,V).
reduce_ground([L|T],M,[L|V]) :- reduce_ground(T,M,V).

% reduce_negs(H,B1,B0,B,N,M) <- B is a subsequence of B1
%                               such that H:-B does not
%                               cover elements of N
reduce_negs(H,[L|B0],In,B,Negs,M):-
	append(In,B0,Body),
	\+(covers_neg((H:-Body),Negs,M,N)),!,
	reduce_negs(H,B0,In,B,Negs,M).
reduce_negs(H,[L|B0],In,B,Negs,M):-
	reduce_negs(H,B0,[L|In],B,Negs,M).
reduce_negs(H,[],Body,Body,Negs,M):-
	\+(covers_neg((H:-Body),Negs,M,N)).

covers_neg(Clause,Negs,Model,N):-
	element(N,Negs),
	covers_ex(Clause,N,Model).

/*==================================================================*/
%%% 9.3  Top-down induction %%%

induce_spec(Examples,Clauses):-
  process_examples([],[],Examples,Clauses).

% process the examples
process_examples(Clauses,Done,[],Clauses).
process_examples(Cls1,Done,[Ex|Exs],Clauses):-
  process_example(Cls1,Done,Ex,Cls2),
  process_examples(Cls2,[Ex|Done],Exs,Clauses).

% process one example
process_example(Clauses,Done,+Example,Clauses):-
  covers(Clauses,Example).
process_example(Cls,Done,+Example,Clauses):-
  \+(covers(Cls,Example)),
  generalise(Cls,Done,Example,Clauses).
process_example(Cls,Done,-Example,Clauses):-
  covers(Cls,Example),
  specialise(Cls,Done,Example,Clauses).
process_example(Clauses,Done,-Example,Clauses):-
  \+(covers(Clauses,Example)).


% covers(Clauses,Ex) <- Ex can be proved from Clauses and
%                       background theory in max. 10 steps
covers(Clauses,Example):-
	prove_d(10,Clauses,Example).

prove_d(D,Cls,true):-!.
prove_d(D,Cls,(A,B)):-!,
	prove_d(D,Cls,A),
	prove_d(D,Cls,B).
prove_d(D,Cls,A):-
	D>0,D1 is D-1,
	copy_element((A:-B),Cls),	% make copy of clause
	prove_d(D1,Cls,B).
prove_d(D,Cls,A):-
	prove_bg(A).

prove_bg(true):-!.
prove_bg((A,B)):-!,
	prove_bg(A),
	prove_bg(B).
prove_bg(A):-
	bg((A:-B)),
	prove_bg(B).


% Specialisation by removing a refuted clause
specialise(Cls,Done,Example,Clauses):-
	false_clause(Cls,Done,Example,C),
	remove_one(C,Cls,Cls1),
	write('     ...refuted: '),write(C),nl,
	process_examples(Cls1,[],[-Example|Done],Clauses).

% false_clause(Cs,E,E,C) <- C is a false clause in the proof of E (or ok)
false_clause(Cls,Exs,true,ok):-!.
false_clause(Cls,Exs,(A,B),X):-!,
	false_clause(Cls,Exs,A,Xa),
	( Xa = ok   -> false_clause(Cls,Exs,B,X)
	; otherwise -> X = Xa
	).
false_clause(Cls,Exs,E,ok):-
	element(+E,Exs),!.
false_clause(Cls,Exs,A,ok):-
	bg((A:-B)),!.
false_clause(Cls,Exs,A,X):-
	copy_element((A:-B),Cls),
	false_clause(Cls,Exs,B,Xb),
	( \+(Xb = ok)		-> X = Xb
	; otherwise		-> X = (A:-B)
	).


% Generalisation by adding a covering clause
generalise(Cls,Done,Example,Clauses):-
	search_clause(Done,Example,Cl),
	write('Found clause: '),write(Cl),nl,
	process_examples([Cl|Cls],[],[+Example|Done],Clauses).


% search_clause(Exs,E,C) <- C is a clause covering E and
%                           not covering negative examples
%                           (iterative deepening search)
search_clause(Exs,Example,Clause):-
	literal(Head,Vars),
	try((Head=Example)),
	search_clause(3,a((Head:-true),Vars),Exs,Example,Clause).

search_clause(D,Current,Exs,Example,Clause):-
	write(D),write('..'),
	search_clause_d(D,Current,Exs,Example,Clause),!.
search_clause(D,Current,Exs,Example,Clause):-
	D1 is D+1,
	!,search_clause(D1,Current,Exs,Example,Clause).

search_clause_d(D,a(Clause,Vars),Exs,Example,Clause):-
	covers_ex1(Clause,Example,Exs),	% goal
	\+((element(-N,Exs),covers_ex1(Clause,N,Exs))),!.
search_clause_d(D,Current,Exs,Example,Clause):-
	D>0,D1 is D-1,
	specialise_clause(Current,Spec),
	search_clause_d(D1,Spec,Exs,Example,Clause).


% Extensional coverage
covers_ex1((Head:-Body),Example,Exs):-
        try((Head=Example,covers_ex(Body,Exs))).

covers_ex(true,Exs):-!.
covers_ex((A,B),Exs):-!,
	covers_ex(A,Exs),
	covers_ex(B,Exs).
covers_ex(A,Exs):-
	element(+A,Exs).
covers_ex(A,Exs):-
	prove_bg(A).


% specialise_clause(C,S) <- S is a minimal specialisation
%                           of C under theta-subsumption
specialise_clause(Current,Spec):-
	add_literal(Current,Spec).
specialise_clause(Current,Spec):-
	apply_subs(Current,Spec).

add_literal(a((H:-true),Vars),a((H:-L),Vars)):-!,
	literal(L,LVars),
	proper_subset(LVars,Vars).
add_literal(a((H:-B),Vars),a((H:-L,B),Vars)):-
	literal(L,LVars),
	proper_subset(LVars,Vars).

apply_subs(a(Clause,Vars),a(Spec,SVars)):-
	copy_term(a(Clause,Vars),a(Spec,Vs)),
	apply_subs1(Vs,SVars).

apply_subs1(Vars,SVars):-
	unify_two(Vars,SVars).
apply_subs1(Vars,SVars):-
	subs_term(Vars,SVars).

unify_two([X|Vars],Vars):-
	element(Y,Vars),
	X=Y.
unify_two([X|Vars],[X|SVars]):-
	unify_two(Vars,SVars).

subs_term(Vars,SVars):-
	remove_one(X,Vars,Vs),
	term(Term,TVars),
	X=Term,
	append(Vs,TVars,SVars).

/*=================== Utility predicates =========================*/

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                                      %
%   Prolog programs from Appendix A.2 of the book      %
%   SIMPLY LOGICAL: Intelligent reasoning by example   %
%   (c) Peter A. Flach/John Wiley & Sons, 1994.        %
%                                                      %
%   Predicates: element/2                              %
%               append/3                               %
%               remove_one/3                           %
%               subset/2                               %
%               proper_subset/2                        %
%               var_element/2                          %
%               var_remove_one/3                       %
%               var_proper_subset/2                    %
%               disj_element/2                         %
%               conj_append/3                          %
%               disj_append/3                          %
%               conj_remove_one/3                      %
%               copy_term/2                            %
%               copy_element/2                         %
%               try/1                                  %
%               setof0/3                               %
%               same_predicate/2                       %
%                                                      %
%   NB. In some Prologs, one or more of these          %
%   predicates may already be built-in. Such           %
%   built-in versions are typically more efficient.    %
%                                                      %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%



%%% Lists and sets

% element(X,Ys) <- X is an element of the list Ys
element(X,[X|Ys]).
element(X,[Y|Ys]):-
	element(X,Ys).

% append(Xs,Ys,Zs) <- list Zs is Xs followed by Ys
append([],Ys,Ys).
append([X|Xs],Ys,[X|Zs]):-
	append(Xs,Ys,Zs).

% remove_one(X,Ys,Zs) <- Zs is list Ys minus one occurrence of X
remove_one(X,[X|Ys],Ys).
remove_one(X,[Y|Ys],[Y|Zs]):-
	remove_one(X,Ys,Zs).

% subset(Xs,Ys) <- every element of list Xs occurs in list Ys
subset([],Ys).
subset([X|Xs],Ys):-
	element(X,Ys),
	subset(Xs,Ys).

% proper_subset(Xs,Ys) <- Xs is a subset of Ys, and Ys contains
%                         at least one element more
proper_subset([],Ys):-
	\+(Ys=[]).
proper_subset([X|Xs],Ys):-
	remove_one(X,Ys,Ys1),
	proper_subset(Xs,Ys1).

var_element(X,[Y|Ys]):-
	X == Y.	% syntactic identity
var_element(X,[Y|Ys]):-
	var_element(X,Ys).

var_remove_one(X,[Y|Ys],Ys):-
	X == Y.	% syntactic identity
var_remove_one(X,[Y|Ys],[Y|Zs]):-
	var_remove_one(X,Ys,Zs).

var_proper_subset([],Ys):-
	\+(Ys=[]).
var_proper_subset([X|Xs],Ys):-
	var_remove_one(X,Ys,Zs),
	var_proper_subset(Xs,Zs).


%%% Conjunctions and disjunctions.

disj_element(X,X):-	% single-element disjunction
	\+(X=false),
	\+(X=(One;TheOther)).
disj_element(X,(X;Ys)).
disj_element(X,(Y;Ys)):-
	disj_element(X,Ys).

conj_append(true,Ys,Ys).
conj_append(X,Ys,(X,Ys)):-	% single-element conjunction
	\+(X=true),
	\+(X=(One,TheOther)).
conj_append((X,Xs),Ys,(X,Zs)):-
	conj_append(Xs,Ys,Zs).

disj_append(false,Ys,Ys).
disj_append(X,Ys,(X;Ys)):-	% single-element disjunction
	\+(X=false),
	\+(X=(One;TheOther)).
disj_append((X;Xs),Ys,(X;Zs)):-
	disj_append(Xs,Ys,Zs).

conj_remove_one(X,X,true):-	% single-element conjunction
	\+(X=true),
	\+(X=(One,TheOther)).
conj_remove_one(X,(X,Ys),Ys).
conj_remove_one(X,(Y,Ys),(Y,Zs)):-
	conj_remove_one(X,Ys,Zs).


%%% Preventing variables from getting instantiated.

% copy_term(Old,New) <- New is a copy of Old with new variables
copy_term(Old,New):-
	asserta('$copy'(Old)),
	retract('$copy'(New)),!.
copy_term(Old,New):-	% in case Old and New donUt unify
	retract('$copy'(Old)),
	!,fail.

copy_element(X,Ys):-
	element(X1,Ys),
	copy_term(X1,X).

% try(Goal) <- Goal succeeds, but variables are not instantiated
try(Goal):-
	\+(\+(Goal)).


%%% Various.

% variant of setof/3 which succeeds with the empty list
% if no solutions can be found
setof0(X,G,L):-
  fast_setof(X,G,L),!.
setof0(X,G,[]).

% same_predicate(L1,L2) <- literals L1 and L2 have
%                          the same predicate and arity
same_predicate(L1,L2):-
	functor(L1,P,N),functor(L2,P,N).

varsin1(T,[]) :- atomic(T), !.
varsin1(V,[V]) :- var(V), !.
varsin1(T,Vars) :- T =.. [_|Args],
                  varsin_args(Args,Vars).

varsin_args([],[]).
varsin_args([A|T],V) :- varsin1(A,V1), !,
                        varsin_args(T,V2),
                        append(V1,V2,V).

varsin(T,V) :- varsin1(T,V1), single_out(V1,V).

single_out([],[]).
single_out([X|T],R) :- var_element(X,T), !, single_out(T,R).
single_out([X|T],[X|R]) :- single_out(T,R).

forall(G,C) :- \+((G,\+(C))).

otherwise.

