% 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