Program HYPER (Hypothesis Refiner) for learning in logicn
Source: PROLOG programming for artificial intelligence, 3rd Edition, Harlow, 2001, ISBN 0-201-40375-7.
Program source code: hyper_hypothesis_refiner.pl
% Figure 19.7 The HYPER program. % Program HYPER (Hypothesis Refiner) for learning in logic :- op( 500, xfx, :). :- op( 900, fy, not). % not Goal): negation as failure; % Note: This is often available as a built-in predicate, % often written as prefix operator "\+", e.g. \+ likes(mary,snakes) not Goal :- Goal, !, fail ; true. % induce( Hyp): % induce a consistent and complete hypothesis Hyp by gradually % refining start hypotheses induce( Hyp) :- init_counts, !, % Initialise counters of hypotheses start_hyps( Hyps), % Get starting hypotheses best_search( Hyps, _:Hyp). % Specialised best-first search % best_search( CandidateHyps, FinalHypothesis) best_search( [Hyp | Hyps], Hyp) :- show_counts, % Display counters of hypotheses Hyp = 0:H, % cost = 0: H doesn't cover any neg. examples complete(H). % H covers all positive examples best_search( [C0:H0 | Hyps0], H) :- write('Refining hypo with cost '), write( C0), write(:), nl, show_hyp(H0), nl, all_refinements( H0, NewHs), % All refinements of H0 add_hyps( NewHs, Hyps0, Hyps), !, add1( refined), % Count refined hypos best_search( Hyps, H). all_refinements( H0, Hyps) :- findall( C:H, ( refine_hyp(H0,H), % H new hypothesis once(( add1( generated), % Count generated hypos complete(H), % H covers all pos. exampl. add1( complete), % Count complete hypos eval(H,C) % C is cost of H )) ), Hyps). % add_hyps( Hyps1, Hyps2, Hyps): % merge Hyps1 and Hyps2 in order of costs, giving Hyps add_hyps( Hyps1, Hyps2, Hyps) :- mergesort( Hyps1, OrderedHyps1), merge( Hyps2, OrderedHyps1, Hyps). complete( Hyp) :- % Hyp covers all positive examples not ( ex( P), % A positive example once( prove( P, Hyp, Answ)), % Prove it with Hyp Answ \== yes). % Possibly not proved % eval( Hypothesis, Cost): % Cost of Hypothesis = Size + 10 * # covered negative examples eval( Hyp, Cost) :- size( Hyp, S), % Size of hypothesis covers_neg( Hyp, N), % Number of covered neg. examples ( N = 0, !, Cost is 0; % No covered neg. examples Cost is S + 10*N). % size( Hyp, Size): % Size = k1*#literals + k2*#variables in hypothesis; % Settings of parameters: k1=10, k2=1 size( [], 0). size( [Cs0/Vs0 | RestHyp], Size) :- length(Cs0, L0), length( Vs0, N0), size( RestHyp, SizeRest), Size is 10*L0 + N0 + SizeRest. % covers_neg( H, N): % N is number of neg. examples possibly covered by H % Example possibly covered if prove/3 returns 'yes' or 'maybe' covers_neg( Hyp, N) :- % Hyp covers N negative examples findall( 1, (nex(E), once(prove(E,Hyp,Answ)), Answ \== no), L), length( L, N). % unsatisfiable( Clause, Hyp): % Clause can never be used in any proof, that is: % Clause's body cannot be proved from Hyp unsatisfiable( [Head | Body], Hyp) :- once( prove( Body, Hyp, Answ)), Answ = no. start_hyps( Hyps) :- % Set of starting hypotheses max_clauses( M), setof( C:H, (start_hyp(H,M), add1(generated), complete(H), add1(complete), eval(H,C)), Hyps). % start_hyp( Hyp, MaxClauses): % A starting hypothesis with no more than MaxClauses start_hyp( [], _). start_hyp( [C | Cs], M) :- M > 0, M1 is M-1, start_clause( C), % A user-defined start clause start_hyp( Cs, M1). % refine_hyp( Hyp0, Hyp): % refine hypothesis Hyp0 into Hyp refine_hyp( Hyp0, Hyp) :- choose_clause( Hyp0, Clause0/Vars0, Clauses1, Clauses2), % Choose a clause conc( Clauses1, [Clause/Vars | Clauses2], Hyp), % New hypothesis refine( Clause0, Vars0, Clause, Vars), % Refine chosen clause non_redundant( Clause), % No redundancy in Clause not unsatisfiable( Clause, Hyp). % Clause not unsatisfiable choose_clause( Hyp, Clause, Clauses1, Clauses2) :- % Choose Clause from Hyp conc( Clauses1, [Clause | Clauses2], Hyp), % Choose a clause nex(E), % A negative example E prove( E, [Clause], yes), % Clause itself covers E ! % Clause must be refined ; conc( Clauses1, [Clause | Clauses2], Hyp). % Otherwise choose any clause % refine( Clause, Args, NewClause, NewArgs): % refine Clause with variables Args giving NewClause with NewArgs % Refine by unifying arguments refine( Clause, Args, Clause, NewArgs) :- conc( Args1, [A | Args2], Args), % Select a variable A member( A, Args2), % Match it with another one conc( Args1, Args2, NewArgs). % Refine a variable to a term refine( Clause, Args0, Clause, Args) :- del( Var:Type, Args0, Args1), % Delete Var:Type from Args0 term( Type, Var, Vars), % Var becomes term of type Type conc( Args1, Vars, Args). % Add variables in the new term % Refine by adding a literal refine( Clause, Args, NewClause, NewArgs) :- length( Clause, L), max_clause_length( MaxL), L < MaxL, backliteral( Lit, InArgs, RestArgs), % Background knowledge literal conc( Clause, [Lit], NewClause), % Add literal to body of clause connect_inputs( Args, InArgs), % Connect literal's inputs to other args. conc( Args, RestArgs, NewArgs). % Add rest of literal's arguments % non_redundant( Clause): Clause has no obviously redundant literals non_redundant( [_]). % Single literal clause non_redundant( [Lit1 | Lits]) :- not literal_member( Lit1, Lits), non_redundant( Lits). literal_member( X, [X1 | Xs]) :- % X literally equal to member of list X == X1, ! ; literal_member( X, Xs). % show_hyp( Hypothesis): % Write out Hypothesis in readable form with variables names A, B, ... show_hyp( []) :- nl. show_hyp( [C/Vars | Cs]) :- nl, copy_term( C/Vars, C1/Vars1), name_vars( Vars1, ['A','B','C','D','E','F','G','H','I','J','K','L','M','N']), show_clause( C1), show_hyp( Cs), !. show_clause( [Head | Body]) :- write( Head), ( Body = []; write( ':-' ), nl ), write_body( Body). write_body( []) :- write('.'), !. write_body( [G | Gs]) :- !, tab( 2), write( G), ( Gs = [], !, write('.'), nl ; write(','), nl, write_body( Gs) ). name_vars( [], _). name_vars( [Name:Type | Xs], [Name | Names]) :- name_vars( Xs, Names). % connect_inputs( Vars, Inputs): % Match each variable in list Outputs with a variable in list Vars connect_inputs( _, []). connect_inputs( S, [X | Xs]) :- member( X, S), connect_inputs( S, Xs). % merge( L1, L2, L3), all lists sorted merge( [], L, L) :- !. merge( L, [], L) :- !. merge( [X1|L1], [X2|L2], [X1|L3]) :- X1 @=< X2, !, % X1 "lexicographically precedes" X2 (built-in predicate) merge( L1, [X2|L2], L3). merge( L1, [X2|L2], [X2|L3]) :- merge( L1, L2, L3). % mergesort( L1, L2): sort L1 giving L2 mergesort( [], []) :- !. mergesort( [X], [X]) :- !. mergesort( L, S) :- split( L, L1, L2), mergesort( L1, S1), mergesort( L2, S2), merge( S1, S2, S). % split( L, L1, L2): split L into lists of approx. equal length split( [], [], []). split( [X], [X], []). split( [X1,X2 | L], [X1|L1], [X2|L2]) :- split( L, L1, L2). % Counters of generated, complete and refined hypotheses init_counts :- retract( counter(_,_)), fail % Delete old counters ; assert( counter( generated, 0)), % Init. counter 'generated' assert( counter( complete, 0)), % Init. counter 'complete' assert( counter( refined, 0)). % Init. counter 'refined' add1( Counter) :- retract( counter( Counter, N)), !, N1 is N+1, assert( counter( Counter, N1)). show_counts :- counter(generated, NG), counter( refined, NR), counter( complete, NC), nl, write( 'Hypotheses generated: '), write(NG), nl, write( 'Hypotheses refined: '), write(NR), ToBeRefined is NC - NR, nl, write( 'To be refined: '), write( ToBeRefined), nl. % Parameter settings max_proof_length( 6). % Max. proof length, counting calls to preds. in hypothesis max_clauses( 4). % Max. number of clauses in hypothesis max_clause_length( 5). % Max. number of literals in a clause prove( Goal, Hypo, Answer) :- max_proof_length( D), prove( Goal, Hypo, D, RestD), (RestD >= 0, Answer = yes % Proved ; RestD < 0, !, Answer = maybe % Maybe, but it looks like inf. loop ). prove( Goal, _, no). % Otherwise Goal definitely cannot be proved % prove( Goal, Hyp, MaxD, RestD): % MaxD allowed proof length, RestD 'remaining length' after proof; % Count only proof steps using Hyp prove( G, H, D, D) :- D < 0, !. % Proof length overstepped prove( [], _, D, D) :- !. prove( [G1 | Gs], Hypo, D0, D) :- !, prove( G1, Hypo, D0, D1), prove( Gs, Hypo, D1, D). prove( G, _, D, D) :- prolog_predicate( G), % Background predicate in Prolog? call( G). % Call of background predicate prove( G, Hyp, D0, D) :- D0 =< 0, !, D is D0-1 % Proof too long ; D1 is D0-1, % Remaining proof length member( Clause/Vars, Hyp), % A clause in Hyp copy_term( Clause, [Head | Body] ), % Rename variables in clause G = Head, % Match clause's head with goal prove( Body, Hyp, D1, D). % Prove G using Clause