mportant notes about grading: 1. Compiler errors:All code you submit must compile. Programs that do not compile will receive an automatic zero. If you run out of time, it is better to comment out the parts that do not compile, than hand in a more complete file that does not compile. 2. Late assignments:You must submit your code before the deadline. Verify on Sakai that you have submitted the correct version. If you submit the incorrect version before the deadline and realize that you have done so after the deadline, we will only grade the version received before the deadline. A Prolog interpreter In this project, you will implement a Prolog interpreter inOCaml. If you want to implement the project inPython, download the source codehereand follow the README file. Parsing functions and test-cases are provided. Pseudocode Your main task is to implement thenon-deterministicabstract interpreter covered in the lectureControl in Prolog. Thepseudocodeof the abstract interpreter is in the lecture note. Bonus There is also a bonus task for implementing adeterministicProlog interpreter with support for backtracking (recover from bad choices) and choice points (produce multiple results). Please refer to the lecture notesProgramming with ListsandControl in Prologfor more details about this algorithm.Bonus will only be added to projects implmented in OCaml. How to Start (OCaml): 1. Download the source codehere. 2. You will need to implement your code infinal/src/final.ml. We give detailed instructions on the functions that you need to implement below. You only need to implement functions withraise (Failure “Not implemented”). Delete this line after implementation is done. 3. The test-cases (also seen below) are provided infinal/test/public.ml(if usingDune) andfinal/main.ml(if usingMake). 4. To compile and run your implementation, we provide two options: Option (1): UsingDune: typedune runtest -fin the command-line window underfinaldirectory. Option (2): UsingMake: First, to compile the code, typemakein the command-line window underfinaldirectory. Second, to run the code, type./main.bytein the command-line window underfinaldirectory. Randomness Because randomness is the key to the success of the non-deterministic abstract interpreter (please see the lecture noteControl in Prologto find why), we first initialize the randomness generator with a random seed chosen in a system-dependent way. In[]: open Stdlib let _ = Random.self_init () Abstract Syntax Tree To implement the abstract interpreter, we will start with the definition of prolog terms (i.e. abstract syntax tree). In[]: type term = | Constant of string (* Prolog constants, e.g., rickard, ned, robb, a, b, … *) | Variable of string (* Prolog variables, e.g., X, Y, Z, … *) | Function of string * term list (* Prolog functions, e.g., append(X, Y, Z), father(rickard, ned), ancestor(Z, Y), cons (H, T) abbreviated as [H|T] in SWI-Prolog, … The first component of Function is the name of the function, whose parameters are in a term list, the second component of Function.*) A Prologprogramconsists ofclausesandgoals. Aclausecan be either afactor arule. A Prologruleis in the shape ofhead :- body. For example, ancestor(X, Y) :- father(X, Z), ancestor(Z, Y). In the above rule (also called a clause),ancestor(X, Y)is theheadof the rule, which is a PrologFunctiondefined in the typetermabove. The rule’sbodyis a list of terms:father(X, Z)andancestor(Z, Y). Both are PrologFunctions. A Prologfactis simply aFunctiondefined in the typeterm. For example, father(rickard, ned). In the above fact (also a clause), we say rickard is ned’s father. A Prolog goal (also called a query) is a list of PrologFunctions, which is typed as a list of terms. For example, ?- ancestor(rickard, robb), ancestor(X, robb). In the abovegoal, we are interested in two queries which are PrologFunctions:ancestor(rickard, robb)andancestor(X, robb). In[]: type head = term (* The head of a rule is a Prolog Function *) type body = term list (* The body of a rule is a list of Prolog Functions *) type clause = Fact of head | Rule of head * body (* A rule is in the shape head :- body *) type program = clause list (* A program consists of a list of clauses in which we have either rules or facts. *) type goal = term list (* A goal is a query that consists of a few functions *) The following stringification functions should help you debug the interpreter. In[]: let rec string_of_f_list f tl = let _, s = List.fold_left (fun (first, s) t –<
let prefix = if first then "" else s ^ ", " in
false, prefix ^ (f t)) (true,"") tl in s (* This function converts a Prolog term (e.g. a constant, variable or function) to a string *) let rec string_of_term t = match t with | Constant c -< c | Variable v -< v | Function (f,tl) -< f ^ "(" ^ (string_of_f_list string_of_term tl) ^ ")" (* This function converts a list of Prolog terms, separated by commas, to a string *) let string_of_term_list fl = string_of_f_list string_of_term fl (* This function converts a Prolog goal (query) to a string *) let string_of_goal g = "?- " ^ (string_of_term_list g) (* This function converts a Prolog clause (e.g. a rule or a fact) to a string *) let string_of_clause c = match c with | Fact f -< string_of_term f ^ "." | Rule (h,b) -< string_of_term h ^ " :- " ^ (string_of_term_list b) ^ "." (* This function converts a Prolog program (a list of clauses), separated by \n, to a string *) let string_of_program p = let rec loop p acc =
match p with
| [] -< acc
| [c] -< acc ^ (string_of_clause c)
| c::t -< loop t (acc ^ (string_of_clause c) ^ "\n") in loop p "" Below are more helper functions for you to easily construct a Prolog program using the defined data types: In[]: let var v = Variable v (* helper function to construct a Prolog Variable *) let const c = Constant c (* helper function to construct a Prolog Constant *) let func f l = Function (f,l)
(* helper function to construct a Prolog Function *) let fact f = Fact f (* helper function to construct a Prolog Fact *) let rule h b = Rule (h,b) (* helper function to construct a Prolog Rule *) Problem 1 In this problem, you will implement the function: occurs_check : term -< term -< bool occurs_check v treturnstrueif the PrologVariablevoccurs int. Please see the lecture noteControl in Prologto revisit the concept of occurs-check. Hint: You don't need to use pattern matching to deconstructv(typeterm) to compare the string value ofvwith that of another variable. You can compare twoVariables via structural equality, e.g.Variable "s" = Variable "s". Therefore,iftis a variable, it suffices to usev = tto make the equality checking. Note that you should use=rather than==for testing structural equality. In[]: let rec occurs_check v t = (* YOUR CODE HERE *)
raise (Failure "Not implemented") Examples and test-cases. In[]: assert (occurs_check (var "X") (var "X")) assert (not (occurs_check (var "X") (var "Y"))) assert (occurs_check (var "X") (func "f" [var "X"])) assert (occurs_check (var "E") (func "cons" [const "a"; const "b"; var "E"])) The last test-case above was taken from the example we used to illustrate the occurs-check problem in the lecture noteControl in Prolog. ?- append([], E, [a,b | E]). Here theoccurs_checkfunction asks whether theVariableE appears on theFunctiontermfunc "cons" [const "a"; const "b"; var "E"]. The return value should betrue. Problem 2 Implement the following functions which return the variables contained in a term or a clause (e.g. a rule or a fact): variables_of_term : term -< VarSet.t variables_of_clause
: clause -< VarSet.t The result must be saved in a data structure of typeVarSetthat is instantiated from OCaml Set module. The type of each element (a PrologVariable) in the set istermas defined above (VarSet.t = term). You may want to useVarSet.singleton tto return a singletion set containing only one elementt, useVarSet.emptyto represent an empty variable set, and useVarSet.union t1 t2to merge two variable setst1andt2. In[]: module VarSet = Set.Make(struct type t = term let compare = Stdlib.compare end) (* API Docs for Set : https://caml.inria.fr/pub/docs/manual-ocaml/libref/Set.S.html *) let rec variables_of_term t = (* YOUR CODE HERE *)
raise (Failure "Not implemented") let variables_of_clause c = (* YOUR CODE HERE *)
raise (Failure "Not implemented") Examples and test-cases: In[]: (* The variables in a function f (X, Y, a) is [X; Y] *) assert (VarSet.equal (variables_of_term (func "f" [var "X"; var "Y"; const "a"])) (VarSet.of_list [var "X"; var "Y"])) (* The variables in a Prolog fact p (X, Y, a) is [X; Y] *) assert (VarSet.equal (variables_of_clause (fact (func "p" [var "X"; var "Y"; const "a"]))) (VarSet.of_list [var "X"; var "Y"])) (* The variables in a Prolog rule p (X, Y, a) :- q (a, b, a) is [X; Y] *) assert (VarSet.equal (variables_of_clause (rule (func "p" [var "X"; var "Y"; const "a"]) [func "q" [const "a"; const "b"; const "a"]])) (VarSet.of_list [var "X"; var "Y"])) Problem 3 The value of typeterm Substitution.tis a OCaml map whose key is of typetermand value is of typeterm. It is a map from variables to terms. Implement substitution functions that takes aterm Substitution.tand uses that to perform the substitution: substitute_in_term : term Substitution.t -< term -< term substitute_in_clause : term Substitution.t -< clause -< clause See the lecture noteControl in Prologto revisit the concept of substitution. For example,휎={푋/푎,푌/푍,푍/푓(푎,푏)}σ={X/a,Y/Z,Z/f(a,b)}is substitution. It is a map from variablesX, Y, Zto termsa, Z, f(a,b). Given a term퐸=푓(푋,푌,푍)E=f(X,Y,Z), the substitution퐸휎Eσis푓(푎,푍,푓(푎,푏))f(a,Z,f(a,b)). You may want to use theSubstitution.find_opt t sfunction. The function takes a term (variable)tand a substitution mapsas input and returnsNoneiftis not a key in the mapsor otherwise returnsSome t'wheret' = s[t]. In[]: module Substitution = Map.Make(struct type t = term let compare = Stdlib.compare end) (* See API docs for OCaml Map: https://caml.inria.fr/pub/docs/manual-ocaml/libref/Map.S.html *) (* This funtion converts a substitution to a string (for debugging) *) let string_of_substitution s = "{" ^ (
Substitution.fold ( fun v t s -< match v with | Variable v -< s ^ "; " ^ v ^ " -< " ^ (string_of_term t) | Constant _ -< assert false (* Note: substitution maps a variable to a term! *) | Function _ -< assert false (* Note: substitution maps a variable to a term! *)
) s "" ) ^ "}" let rec substitute_in_term s t = (* YOUR CODE HERE *)
raise (Failure "Not implemented") let substitute_in_clause s c = (* YOUR CODE HERE *)
raise (Failure "Not implemented") Examples and test-cases: In[]: (* We create a substitution map s = [Y/0, X/Y] *) let s = Substitution.add (var "Y") (const "0") (Substitution.add (var "X") (var "Y") Substitution.empty) (* Function substitution - f (X, Y, a) [Y/0, X/Y] = f (Y, 0, a) *) assert (substitute_in_term s (func "f" [var "X"; var "Y"; const "a"]) = func "f" [var "Y"; const "0"; const "a"]) (* Fact substitution - p (X, Y, a) [Y/0, X/Y] = p (Y, 0, a) *) assert (substitute_in_clause s (fact (func "p" [var "X"; var "Y"; const "a"])) = (fact (func "p" [var "Y"; const "0"; const "a"]))) (* Given a Prolog rule, p (X, Y, a) :- q (a, b, a), after doing substitution [Y/0, X/Y], we have p (Y, 0, a) :- q (a, b, a) *) assert (substitute_in_clause s (rule (func "p" [var "X"; var "Y"; const "a"]) [func "q" [const "a"; const "b"; const "a"]]) = (rule (func "p" [var "Y"; const "0"; const "a"]) [func "q" [const "a"; const "b"; const "a"]])) Problem 4 Implementing the function: unify : term -< term -< term Substitution.t The function returns a unifier of the given terms. The function should raise the exceptionraise Not_unfifiable, if the given terms are not unifiable (Not_unfifiableis a declared exception infinal.ml). You may find thepseudocodeofunifyin the lecture noteControl in Prologuseful. As in problem 3, you will need to usemodule Substitutionbecause unification is driven by subsititution. (See API docs for OCaml Map:https://caml.inria.fr/pub/docs/manual-ocaml/libref/Map.S.html) You may want to usesubstitute_in_termto implement the first and second lines of the pseudocode. You may want to useSubstitution.emptyfor an empty subsitution map,Substitution.singleton v tfor creating a new subsitution map that contains a single substitution[v/t], andSubstitution.add v t sto add a new substitution[v/t]to an existing substitution maps(this function may help implement the∪∪operation in the pseudocode). You may also want to useSubstitution.mapfor the휃θ[X/Y]operation in the pseudocode. This operation applies the subsitition[X/Y]to each term in thevaluesof the substitution map휃θ(thekeysof the substitution map휃θremain unchanged).Subsitution.map f sreturns a new substitution map with the same keys as the input substitution maps, where the associated termtfor each key ofshas been replaced by the result of the application offtot. UseList.fold_left2to implement thefold_leftfunction in the pseudocode (https://caml.inria.fr/pub/docs/manual-ocaml/libref/List.html). In[]: exception Not_unifiable let unify t1 t2 = (* YOUR CODE HERE *)
raise (Failure "Not implemented") Examples and test-cases: In[]: (* A substitution that can unify variable X and variable Y: {X-