Execution.

The interpreter walks the parse tree of a program and executes it. As it does so values are bound to variables and these bindings are kept in an environment:

     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.                              }



[Previous Page] [Next Page] [Index] © L. Allison, Dept. Computer Science, Monash University