For Ia students, please do the following Run this program and find that it produces the following output psolver(PRED("grandfather", [ VAR("X"), VAR("Y") ])); val it = (false, [], []) : bool * (string * pexp_t) list * 'b list Make the program work, so that it deduces that philip is the grandfather of harry and william. These facts are supposed to come out via the solns list. Ignore the other exercises. ------------ (* CBG SQUANDERER PROLOG http://www.cl.cam.ac.uk/users/djg/pubs/prolog.txt Notes: For those not familiar with Prolog, the process of unification is to establish a mapping between pairs of variables or variables and constants. Unification: In simple terms, X will unifiy with Y if 1. If X is a constant and Y is a variable, then Y takes on the value of X 2. If both X and Y are constants, we fail to unifiy if they are different 3. If both X and Y are variables, if one is not already bound then it takes on the value of the other (which may or may not be bound already). For example, we can unify P(x, 22, "cat") with Q(y, y, v) by setting x=y=22 and v="cat". Cut and fail: If the system encounters the FAIL term, the current rule fails outright. If the system encounters a CUT term while backtracking, the current rule fails. This means that, for example N(s,t), P(v), CUT, Q(v,r), S(v,r) will search out all possible values for r by re-evaluating Q and S, but if it has not succeeded in this search and needs to backtrack to find a new value for v, then it fails instead. List data types: For the prolog list data types, a constructor called 'cons' needs to be introduced as a new value that variables can range over. Cons takes a pair of values and binds them together. One is the head of a list and the other is the tail of a list. A new special value can also be used to mark the end of a list, such as 'nil'. Cons(X, Y) will unifiy with CONS(P, Q) iff X will unifiy with P and Y will unifiy with Q. *) (* -- *) (* * CBG Squander Prolog. * Simple prolog interpreter in SML. * (C) 2000 DJ Greaves. All rights reserved. * * Exercise 1: Complete the unification subroutine * Exercise 2: Implement CUT and FAIL * Exercise 3: Implement prolog's list data types. * Exercise 4: Use this prolog interpreter for an example that uses difference lists. * * Note: the first thing to do is to make the system return a result * of any sort, otherwise it will not load under ML. *) (* Datatypes used *) datatype pexp_t = INT of int | VAR of string | STRING of string ; datatype predicate_t = PRED of string * pexp_t list | CUT | FAIL ; datatype rule_t = RULE of string * pexp_t list * predicate_t list ; (* Code database for the example run *) val gf_r = RULE("grandfather", [ VAR("X"), VAR("Y")], [ PRED("father", [ VAR("X"), VAR("P") ]), PRED("father", [ VAR("P"), VAR("Y") ]) ]); val f1_r = RULE("father", [ STRING("charles"), STRING("william") ], []); val f2_r = RULE("father", [ STRING("charles"), STRING("harry") ], []); val f3_r = RULE("father", [ STRING("philip"), STRING("charles") ], []); (* Note that prolog is sensitive to the order of the rules. *) val rules = [ f1_r, f2_r, f3_r, gf_r ]; (* Now the interpreter *) fun lookup(id, nil) = NONE | lookup(id, (v,e)::t) = if (id=v) then SOME(e) else lookup(id, t) ; (* * Unification algorithm... needs a bit more work *) fun unif(INT(n), INT(v), env) = (n=v, env) | unif(STRING(n), STRING(v), env) = (n=v, env) | unif(x, VAR(v), env) = let val vv = lookup(v, env) in if (vv=NONE) then (true, (v, x)::env) else (valOf(vv)=x, env) end | unif(VAR(v), x, env) = unif(x, VAR(v), env) ; fun unif_list(nil, nil, env) = (true, env) | unif_list(h::t, hh::tt, env) = let val (okf, env') = unif(h, hh, env) in if (okf) then unif_list(t, tt, env') else (false, env) end ; fun psolve(g, env, nil, rules, solns) = (false, env, solns) | psolve(PRED(name, args), env, RULE(name', args', subgoals)::tr, rules, solns) = let val (okf, env') = if (name=name') then unif_list(args, args', env) else (false, env) val (okf2, env2) = if (okf) then psolve_list(subgoals, env', rules) else (okf, env') in if (okf2) then (true, env2, solns) else psolve(PRED(name, args), env, tr, rules, solns) end and psolve_list(nil, env, rules) = (true, env) | psolve_list(h::t, env, rules) = let val (okf, env', _) = psolve(h, env, rules, rules, []) in if (okf) then psolve_list(t, env, rules) else (false, env) end ; fun psolver(g) = psolve(g, nil, rules, rules, []); psolver(PRED("grandfather", [ VAR("X"), VAR("Y") ]));