Env = ^ Binding; Binding = record id :alfa; index :integer; v:tree; next:Env end; {\fB Environment Type. \fP} function bind( x :tree; val :tree; e :Env ) :Env; var b :Env; begin new(b); b^.id := x^.vid; b^.index := x^.index; b^.v := val; b^.next := e; bind := b end; function bound( x :tree; var val :tree; e :Env ) :boolean; begin if e=nil then bound := false else if (e^.id=x^.vid) and (e^.index=x^.index) then begin val := e^.v; bound := true end else bound := bound( x, val, e^.next ) end; {\fB Manipulate Environments. \fP}The interpreter attempts to prove or satisfy the query in a program using the given facts. If it fails it prints `no'. It prints all solutions that it finds, if any.
procedure execute(prog :tree); type mode = (PrintAll, Silent); {search mode} var index :integer; { used for renaming } #include "unify.P" { unify two predicates } #include "rename.P" { rename variables in a rule } #include "prove.P" { proof strategy } begin {execute} index := 0; if not Prove(PrintAll, prog^.query, prog^.facts, nil) then writeln(' no') end {execute}; {\fB Interpreter. \fP}The proof strategy defined here is a simple top-down left-to-right strategy. It attempts to prove a query by proving each literal in turn. It tries to prove an atom by unifying it with the left hand side of some rule. If unification succeeds, the right hand side of the rule plus the remainder of the query must then be proven. An environment is maintained during this process and unification may add to it. The proof of a negated atom relies on negation by failure; the proof of the (positive) atom must fail. If this is the case, the remainder of the query must then be proven.
function Prove( search:mode; query, facts :tree; e :Env) :boolean; label 99; {success escape for Silent mode} var Satisfied :boolean; procedure ProveList( query, facts :tree; e :Env ); procedure ProveLiteral(p, f :tree; e :Env); var newe :Env; begin if p^.tag = negate then { negated atom eg. not l(...) } begin {negation by failure: not p(...) succeeds iff p(...) fails} if not Prove(Silent, cons(p^.l, nil), f, e) then ProveList(query^.tl, f, e) {rest of query} {else do nothing at all} end else { positive atom eg. p(...) } if f <> nil then begin if unify(p, rename(f^.hd^.lhs, index), newe, e) then ProveList(append(rename(f^.hd^.rhs, index), {RHS of rule} query^.tl), {plus rest of query} facts, newe); ProveLiteral(p, f^.tl, e) {also try for other solutions} end end {ProveLiteral}; begin {ProveList} if query = nil then {nothing more to prove - success} case search of PrintAll:{print ALL solutions to query} begin printtree(prog^.query, e); writeln(' yes'); Satisfied:=true end; Silent: {esp' for negation by failure, only need one success} begin Satisfied := true; goto 99 {!!! once is enough} end end else begin index:=index+1; ProveLiteral(query^.hd, facts, e) end end {ProveList}; begin { Prove } Satisfied := false; ProveList( query, facts, e); 99: Prove := Satisfied end { Prove }; {\fB Depth-First, Left-to-Right Proof Strategy. \fP} {Do not remove: Main.p, env*P, execute.P, unify.P, rename.P, prove.P, lex*P, } { syntax*P, tree.P are released under Gnu `copyleft' General Public Licence } { - L. Allison, CSSE, Monash Uni., .au, 7/2003. }Negation by failure need only detect a single proof of the atom and need not print it. For this reason the proof strategy operates in one of two modes. In `PrintAll' mode, all solutions are sought and printed. In `Silent' mode, one solution is sought and not printed.
When a rule is used, a copy containing renamed variables is used so as to prevent name clashes between different instances of the rule. Renaming is based on a recursive tree traversal much like the tree print routine.
function rename(t :tree; index :integer) :tree; var r :tree; function copynode :tree; var c :tree; begin c:=newnode(t^.tag); c^:=t^; copynode:=c end; begin{rename} if t = nil then r := nil else case t^.tag of variable:begin r:=copynode; r^.index:=index end; constant:r := t; intcon: r := t; predicate, func: begin r := copynode; r^.params := rename(t^.params, index) end; negate: begin r := copynode; r^.l := rename(t^.l, index) end; rule: begin r := copynode; r^.lhs := rename(t^.lhs, index); r^.rhs := rename(t^.rhs, index) end; list: begin r := copynode; r^.hd := rename(t^.hd, index); r^.tl := rename(t^.tl, index) end; end{case}; rename := r end{rename}; {\fB Rename Variables in a Tree. \fP}The unification routine attempts to find bindings for variables so as to make two atoms syntactically identical. It is heavily based on a recursive tree-equality function. For example, two constants are the same if and only if they are the same constant! Two function terms are the same if and only if they have the same function identifier and their parameters are the same.
A variable may be bound or unbound in the current environment. If a variable is bound to a value, the variable unifies with a term if and only if its value unifies with the term. On the other hand, an unbound variable unifies with any term and the variable is bound to the term in an extended environment. In this way the environment can grow. Strictly speaking, a variable should not bind with a term that contains the variable. A test to this effect is known as the occurs check. The occurs check is usually not implemented on efficiency grounds but this may cause the interpreter to loop in some cases.
If two atoms unify, the set of bindings discovered is known as the most general unifier (MGU) in the sense that any other set of bindings unifying the atoms would be a special case of the MGU.
function unify( a, b :tree; var newenv :Env; oldenv :Env) :boolean; var e2 :Env; v :tree; begin {unify} newenv := oldenv; if (a = nil) or (b=nil) then unify := a=b else { a<>nil and b<>nil } if a^.tag = b^.tag then case a^.tag { = b^.tag } of variable: if bound(a, v, oldenv) then unify := unify(v, b, newenv, oldenv) else if bound(b, v, oldenv) then unify := unify(a, v, newenv, oldenv) {both unbound} else if (a^.vid=b^.vid) and (a^.index=b^.index) then unify := true else {2 different, unbound vars} begin newenv := bind(a, b, oldenv); unify := true end; constant: unify := a^.cid = b^.cid; { m : n } intcon: unify := a^.n = b^.n; { x : y } func, predicate: { a(...) : b(...) } if a^.id = b^.id then unify := unify(a^.params, b^.params, newenv, oldenv) else unify := false; { ahd.atl : bhd.btl } list: if unify(a^.hd, b^.hd, e2, oldenv) then unify := unify(a^.tl, b^.tl, newenv, e2) else unify := false end {case} else { a^.tag <> b^.tag } if a^.tag = variable then { X : f(...) } if bound(a, v, oldenv) then unify := unify(v, b, newenv, oldenv) else begin newenv := bind(a, b, oldenv); unify := true end else if b^.tag = variable then { f(...) : X } unify := unify(b, a, newenv, oldenv) else unify := false end {unify}; {\fB Unification Algorithm. \fP} {Do not remove: Main.p, env*P, execute.P, unify.P, rename.P, prove.P, lex*P, } { syntax*P, tree.P are released under Gnu `copyleft' General Public Licence } { - L. Allison, CSSE, Monash Uni., .au, 7/2003. }