/* Inductive Logic Programming in Picat v3. This is a port of the program HYPER (hyper.pl) in I. Bratko, "Prolog Programming for Artificial Intelligence", 4th edn., Pearson Education / Addison-Wesley 2012 Page 507ff (Figure 21.7 and 21.3) Changes: - some $ escaping - renamed :/2 to type/2 - conc/3 -> append/3 - findall/3 -> findall/3 - setof/3 -> findall/3 + sort_remove_dups - added del/3 from the book page 68 - length/2 -> bp.length/2 - assert/1 -> bp.assert , retract/1 -> bp.retract/1 - copy_term/2 -> bp.copy_term This Picat model was created by Hakan Kjellerstrand, hakank@gmail.com See also my Picat page: http://www.hakank.org/picat/ */ module hyper_v3. % import setof_okeefe_v3. % testing with set_of/3 but it don't work import util. % Figure 21.7 The HYPER program. The procedure prove/3 is as in Figure 21.3. % Program HYPER (Hypothesis Refiner) for learning in logic % hakank: replaced with colon/2 % :- op( 500, xfx, :). % 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, $type(_,Hyp)). % Specialised best-first search % best_search( CandidateHyps, FinalHypothesis) best_search( [Hyp | Hyps], Hyp) :- show_counts, % Display counters of hypotheses Hyp = $type(0,H), % cost = 0: H doesn't cover any neg. examples complete(H). % H covers all positive examples best_search( [type(C0,H0) | Hyps0], H) :- print('Refining hypo with cost '), print( C0), print(:), 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) :- % bp.findall( $type(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). % hakank: Hyps = findall( type(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 )) )). % 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 \+ ( $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) :- bp.length(Cs0, L0), bp.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 % bp.findall( 1, $(nex(E), once(prove(E,Hyp,Answ)), Answ \== no), L), L = findall( 1, (nex(E), once(prove(E,Hyp,Answ)), Answ \= no)), bp.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( $type(C,H), % $(start_hyp(H,M), add1(generated), % complete(H), add1(complete), eval(H,C)), % Hyps). % hakank: from setof_okeefe_v3 (this don't work!) % set_of($type(C,H), % $(start_hyp(H,M), add1(generated), % complete(H), add1(complete), eval(H,C) % ), % Hyps). % hakank: Hyps = findall(type(C,H), (start_hyp(H,M), add1(generated), complete(H), add1(complete), eval(H,C)) ).sort_remove_dups. % 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 append( Clauses1, $[Clause/Vars | Clauses2], Hyp), % New hypothesis refine( Clause0, Vars0, Clause, Vars), % Refine chosen clause non_redundant( Clause), % No redundancy in Clause \+ unsatisfiable( Clause, Hyp). % Clause not unsatisfiable choose_clause( Hyp, Clause, Clauses1, Clauses2) :- % Choose Clause from Hyp append( 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 ; append( 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) :- append( Args1, [A | Args2], Args), % Select a variable A member( A, Args2), % Match it with another one append( Args1, Args2, NewArgs). % Refine a variable to a term refine( Clause, Args0, Clause, Args) :- del( $type(Var,Type), Args0, Args1), % Delete Var:Type from Args0 term( Type, Var, Vars), % Var becomes term of type Type append( Args1, Vars, Args). % Add variables in the new term % Refine by adding a literal refine( Clause, Args, NewClause, NewArgs) :- bp.length( Clause, L), max_clause_length( MaxL), L < MaxL, backliteral( Lit, InArgs, RestArgs), % Background knowledge literal append( Clause, [Lit], NewClause), % Add literal to body of clause connect_inputs( Args, InArgs), % Connect literal's inputs to other args. append( Args, RestArgs, NewArgs). % Add rest of literal's arguments % From page 68 del(X, [X |Tail], Tail). del(X, [Y |Tail], [Y |Tail1]) :- del(X, Tail, Tail1). % non_redundant( Clause): Clause has no obviously redundant literals non_redundant( [_]). % Single literal clause non_redundant( [Lit1 | Lits]) :- \+ 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): % Print out Hypothesis in readable form with variables names A, B, ... show_hyp( []) :- nl. show_hyp( [C/Vars | Cs]) :- nl, bp.copy_term( $(C/Vars), $(C1/Vars1)), % 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]) :- Head1 = delete_all(Head.to_string(),'\''), print(Head1), ( Body = []; print( ':-' ), nl ), print_body( Body). print_body( []) :- print('.'), !. print_body( [G | Gs]) :- !, G1 = delete_all(G.to_string(),'\''), bp.tab( 2), print( G1), ( Gs = [], !, print('.'), nl ; print(','), nl, print_body( Gs) ). % From the book (frequent.pl) % copy_term( Term, Copy) :- % bp.asserta($term_to_copy( Term)), % bp.retract($term_to_copy( Copy)), !. name_vars( [], _). name_vars( [type(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) :- splitx( 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 splitx( [], [], []). splitx( [X], [X], []). splitx( [X1,X2 | L], [X1|L1], [X2|L2]) :- splitx( L, L1, L2). % Counters of generated, complete and refined hypotheses init_counts :- bp.retract( $counter(_,_)), fail % Delete old counters ; bp.assert( $counter( generated, 0)), % Init. counter 'generated' bp.assert( $counter( complete, 0)), % Init. counter 'complete' bp.assert( $counter( refined, 0)). % Init. counter 'refined' add1( Counter) :- bp.retract( $counter( Counter, N)), !, N1 is N+1, bp.assert( $counter( Counter, N1)). show_counts :- bp.counter(generated, NG), bp.counter( refined, NR), bp.counter( complete, NC), nl, print( 'Hypotheses generated: '), print(NG), nl, print( 'Hypotheses refined: '), print(NR), ToBeRefined is NC - NR, nl, print( 'To be refined: '), print( ToBeRefined), nl. % Parameter settings % hakank: moved to the examples % 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 % Figure 21.3 A loop-avoiding interpreter for hypotheses. % Interpreter for hypotheses % prove( Goal, Hypo, Answ): % Answ = yes, if Goal derivable from Hypo in at most D steps % Answ = no, if Goal not derivable % Answ = maybe, if search terminated after D steps inconclusively 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 bp.copy_term( Clause, [Head | Body] ), % Rename variables in clause % 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