You must complete this program with the same partner you had for "Type Inference". This is your final project with this partner.
A Brief History of Prolog at Brown
Student: Are you doing Prolog again this year?
Student: That was the hardest assignment I ever did at Brown—and I even did Weenix!
Shriram: Well, I was thinking of scaling it down this year....
Student: No! You can't do that. It's like a rite of passage.
In this assignment, you will implement Prolog-style logic variables and backtracking search using Scheme's macros and continuations. In particular, you must implement the following:
=succeed: succeeds exactly once
=fail: does not succeed
(== e1 e2): attempts to unify
e2(succeeds at most once)
(=var (v ...) e): binds all of the
(v ...)to fresh logic variables and evaluates
ein the extended environment
(_): returns a fresh anonymous variable (its binding always succeeds and affects nothing else)
(=or e ...): searches for variable assignments that satisfy any of the
(=and e ...): searches for variable assignments that satisfy all of the
=and) consume a failure continuation (to be invoked on failure) and, if successful, return a success continuation (to allow resumption of the search). This pattern prevents the Prolog embedding from communicating ordinary program answers through procedure return values. Instead it uses logic variables, which you will need to update imperatively, taking care to restore when backtracking. In addition to these linguistic extensions, you must also implement the following testing interface:
(=find-all (v ...) e): returns a list of all the solutions to
e; each solution is a list of variable bindings (one binding for each of the
v ...), and each variable binding is a two-element list consisting of the quoted variable name (a symbol) and its value. Note that if the value is a list, it should be returned as a Scheme list. The solutions should be returned in their order of discovery (by a left-to-right depth-first search), and each solution should list the variables in the order provided.
(=find-some n (v ...) e): returns a list of solutions to
e, as in
(findall ...)from above, except that search is bounded to at most
nsolutions (this allows us to test on queries with infinite solutions)
Note that there is nothing special about the variables bound by
=find-some. They are simply the
logic variables whose values the user is interested in (v ...).
Data TypesThere are two data types that you have to deal with in your unification process: flat types and cons types. Flat types (e.g. numbers, symbols, strings) can be bound directly to logic variables. Cons types are compound objects that may have other data types or even logic variables within them. You must implement
(=cons f r)which produces a cons of f and r. Essentially, this behaves exactly like cons except that it stores the data in a representation you define to facilitate unification. Here is a definition for
(define =list (lambda args (if (empty? args) '() (=cons (first args) (apply =list (rest args))))))Your definition of
=consshould behave nicely with this. Thus,
(show (x y) (== (=cons 1 (=cons (=cons 2 '()) '())) (=list x y)))should successfully find
x=1, y=(2). Note here that
y's value is not implementation specific; it is a standard Scheme list.
Interactive TestingThese are not requred by the assignment, but to aid in interactive testing (as shown in the examples below), you may find the following two definitions helpful:
(define resumer-box (box 'resumer)) (define (next) ((unbox resumer-box) 'dummy)) (define-syntax show (syntax-rules () [(show (vars ...) e) (=var (vars ...) (let/cc esc (let/cc fk (esc (let ([next (e fk)]) (set-box! resumer-box next) (printf "~a: ~a~n" (quote vars) (lv-value vars)) ... (void)))) 'fail))]))where
lv-valueaccesses the value stored in the given logic variable.
Please note that these definitions are very implementation specific. If you would like to use them for testing, we not only encourage you, but we expect you to modify them to make them work with your implementation.
TestingPlease use the following definitions to help you with your testing:
;; symbol -> boolean : returns true if and only if the given ;; symbol is an uninterned symbol (define (gensym? s) (not (equal? (string->symbol (symbol->string s)) s))) ;; list X list -> boolean : takes two bindings (for example, returned ;; from =find-all) and returns true if and only if the two variables ;; they bind are equal to the same thing. (define (binding-equal? b1 b2) (equal? (second b1) (second b2))) ;; Prolog-Expr X symbol X bool-Exprs ... -> Test result : Takes a ;; (=find-all ...) or (=find-some ...), an identifier, and a set of ;; expressions that evaluate to booleans when the identifier is bound ;; to the result of the given Prolog-expr. The test passes if and ;; only if all of the boolean expressions are true. (define-syntax test-prolog (syntax-rules (test-prolog) [(test-prolog find-expr result-id bool ...) (test (let ([result-id find-expr]) (and bool ...)) true)]))
- Please do not use global variables for this assignment. We expect your implementation to have the ability to do a query, capture the continuation returned, do a different query, and then invoke the first continuation with no trouble.
- Unbound variables should have a unique "value" in their output. That is, if
yis unbound, it should have a unique symbol as its value. If
yare dependently unbound, they should have the same unique symbol as their values.
- Remember that order counts. Please carefully read the definitions for =find-all and =find-some. Even if your results are correct, if they are in the wrong order or format, they will be marked as incorrect.
- Remember that
=consis a construct that you use to make lists with logic variables in them; it's not necessarily a list itself. That's why if you are making a test which should bind the logic variable
(=cons 1 '()), the test case should check that the result equals
(cons 1 '())or
(=cons 1 '())to build the result.
- Remember to implement the occurs check during unification.
Example 1: Simple Search
You might want to start by just testing
=or with success and failure (no logic variables). In
this restricted setting, there are a couple of useful properties:
e1 succeeds in n1 ways,
succeeds in n2 ways, etc., then
(=or e1 e2 ...)
succeeds in n1 + n2 + ... ways, and
(=and e1 e2
...) succeeds in n1 * n2 * ... ways. For instance,
(=and (=or =succeed =succeed =fail =succeed) (=or =fail =succeed =succeed))succeeds in six ways. The first
=orsucceeds in three ways, the second
=orsucceeds in two ways, and the
=andcombines them in all possible ways. Likewise,
(=or (=and =succeed =succeed) (=and =fail =succeed =succeed) (=and =succeed))succeeds in two ways. The first and third
=ands each succeed in one way, and the
=orexplores both of them.
You can use
show (with an empty variable list) and
next to count how many times a query succeeds. You can
also use the following test-prolog expression:
(test-prolog (=find-all () (=or (=and =succeed =succeed) (=and =fail =succeed =succeed) (=and =succeed))) result (= (length result) 2))
Example 2: Family Trees
As a more complicated example, suppose we have the following definitions:
(define (=parent c p) (=or (=and (== c 'vito) (== p 'dom)) (=and (== c 'sonny) (== p 'vito)) (=and (== c 'michael) (== p 'vito)) (=and (== c 'fredo) (== p 'vito)) (=and (== c 'sophia) (== p 'michael)) (=and (== c 'tony) (== p 'michael)))) (define (=ancestor X Y) (=or (=parent X Y) (=var (Z) (=and (=parent X Z) (=ancestor Z Y)))))Then we get the following query results:
> (show (x) (=ancestor x 'vito)) x: sonny > (next) x: michael > (next) x: fredo > (next) x: sophia > (next) x: tony > (next) 'fail > (find-all (x) (=parent x 'michael)) (list (list (list 'x 'sophia)) (list (list 'x 'tony))) > (find-some 3 (x y) (=ancestor x y)) (list (list (list 'x 'vito) (list 'y 'dom)) (list (list 'x 'sonny) (list 'y 'vito)) (list (list 'x 'michael) (list 'y 'vito)))
This assignment will be war graded. You should be used to the procedure for this by now. You will also turn in a final copy: from the directory containing the files you wish to hand in, execute
/course/cs173/bin/cs173handin prologA single member of your group should submit the .ss files for the implementation and a readme. The readme file should contain the names of the members of the group.