Różnice między wybraną wersją a wersją aktualną.
| — |
pl:prolog:pllib:rule_interpreter_2 [2019/06/27 15:50] (aktualna) |
||
|---|---|---|---|
| Linia 1: | Linia 1: | ||
| + | ====== Rule interpreter 2 ====== | ||
| + | {{tag>interpreter rules proof trees}} | ||
| + | ===== Description ===== | ||
| + | A two-level rule interpreter with proof trees | ||
| + | |||
| + | **Source**: The Art of Prolog | ||
| + | ===== Download ===== | ||
| + | Program source code: {{rule_interpreter_2.pl}} | ||
| + | ===== Listing ===== | ||
| + | <code prolog> | ||
| + | /* | ||
| + | monitor(Goal,Proof) :- | ||
| + | Succeeds if a result of yes is returned from solving Goal at the | ||
| + | solve level, in which case Proof is a proof tree representing the | ||
| + | successful computation, or when the end of the computation is reached, | ||
| + | in which case Proof is a list of failure branches since the last success. | ||
| + | */ | ||
| + | |||
| + | :- op( 900, fy, not). | ||
| + | :- op(40,xfy,&). | ||
| + | :- op(30,xf,is_true). | ||
| + | |||
| + | monitor(Goal,Proof) :- | ||
| + | set_search_tree, solve(Goal,Result,Proof), | ||
| + | filter(Result,Proof). | ||
| + | monitor(Goal,Proof) :- | ||
| + | collect_proof(P), reverse(P,P1), | ||
| + | Proof = failed(Goal,P1). | ||
| + | |||
| + | filter(yes,Proof) :- reset_search_tree. | ||
| + | filter(no,Proof) :- store_proof(Proof), fail. | ||
| + | |||
| + | /* | ||
| + | solve(Goal,Result,Proof) :- | ||
| + | Given a set of rules of the form rule(A,B,Name), Goal has | ||
| + | Result yes if it follows from the rules and no if it does not. | ||
| + | Proof is a proof tree if the result is yes and a failure branch | ||
| + | of the search tree if the result is no. | ||
| + | */ | ||
| + | :- op(40,xfy,because). | ||
| + | :- op(30,xfy,with). | ||
| + | |||
| + | solve(A,yes,Tree) :- fact(A), Tree = fact(A). | ||
| + | solve(A,Result,Tree) :- | ||
| + | rule(A,B,Name), solve_body(B,Result,Proof), | ||
| + | Tree = A because B with Proof. | ||
| + | solve(A,no,Tree) :- | ||
| + | not fact(A), not rule(A,B,Name), Tree = no_match(A). | ||
| + | |||
| + | solve_body(A&B,Result,Proof) :- | ||
| + | solve_body(A,ResultA,ProofA), | ||
| + | solve_and(ResultA,B,Result,ProofB), | ||
| + | Proof = ProofA & ProofB. | ||
| + | solve_body(A is_true,Result,Proof) :- solve(A,Result,Proof). | ||
| + | |||
| + | solve_and(no,A,no,unsearched). | ||
| + | solve_and(yes,B,Result,Tree) :- solve(B,Result,Tree). | ||
| + | |||
| + | % The following predicates use side effects to record and remove | ||
| + | % branches of the search tree. | ||
| + | |||
| + | collect_proof(Proof) :- retract('search tree'(Proof)). | ||
| + | |||
| + | store_proof(Proof) :- | ||
| + | retract('search tree'(Tree)), | ||
| + | assert('search tree'([ProofjTree])). | ||
| + | |||
| + | set_search_tree :- assert('search tree'([ ])). | ||
| + | |||
| + | reset_search_tree :- | ||
| + | retract('search tree'(Proof)), | ||
| + | assert('search tree'([ ])). | ||
| + | |||
| + | reverse([],[]). | ||
| + | reverse([X|Xs],Zs) :- reverse(Xs,Ys), append(Ys,[X],Zs). | ||
| + | |||
| + | % Program 17.21: A two-level rule interpreter with proof trees | ||
| + | </code> | ||
| + | ===== Comments ===== | ||
