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?
Shriram: Yes.
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.
Implementing Prolog
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 unifye1
withe2
(succeeds at most once) -
(=var (v ...) e)
: binds all of the(v ...)
to fresh logic variables and evaluatese
in 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 thee ...
expressions -
(=and e ...)
: searches for variable assignments that satisfy all of thee ...
expressions
=succeed
,
=fail
, ==
, =or
, and
=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 toe
; each solution is a list of variable bindings (one binding for each of thev ...
), 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 toe
, as in(findall ...)
from above, except that search is bounded to at mostn
solutions (this allows us to test on queries with infinite solutions)
Note that there is nothing special about the variables bound by
=find-all
and =find-some
. They are simply the
logic variables whose values the user is interested in (v ...).
Data Types
There 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 =list
:
(define =list (lambda args (if (empty? args) '() (=cons (first args) (apply =list (rest args))))))Your definition of
=cons
should 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 Testing
These 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-value
accesses 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.
Testing
Please 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)]))
Notes
- 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
y
is unbound, it should have a unique symbol as its value. Ifx
andy
are 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
=cons
is 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 variableX
to, say,(=cons 1 '())
, the test case should check that the result equals(cons 1 '())
or'(1)
rather than(=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 =and
and
=or
with success and failure (no logic variables). In
this restricted setting, there are a couple of useful properties:
namely, if e1
succeeds in n1 ways, e2
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
=or
succeeds in three
ways, the second =or
succeeds in two ways, and the
=and
combines them in all possible ways.
Likewise,
(=or (=and =succeed =succeed) (=and =fail =succeed =succeed) (=and =succeed))succeeds in two ways. The first and third
=and
s each
succeed in one way, and the =or
explores 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)))
Hand In
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.