mirror of
https://github.com/correl/sicp.git
synced 2024-11-27 11:09:58 +00:00
899 lines
27 KiB
Org Mode
899 lines
27 KiB
Org Mode
#+TITLE: 4.4 - Logic Programming
|
|
#+STARTUP: indent
|
|
#+OPTIONS: num:nil
|
|
|
|
- [[file:4-4.org][Raw org source]]
|
|
- [[file:4-4.org.html][Htmlized org source]]
|
|
|
|
This section seems to describe all the cool things that turned me on
|
|
to Prolog.
|
|
* COMMENT Set up source file
|
|
#+BEGIN_SRC scheme :tangle yes
|
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
|
;; 4.4 - Logic Programming
|
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
|
|
|
(load "3-5.scheme") ;; Stream functions
|
|
(load "4-3.scheme") ;; All the things so far
|
|
|
|
#+END_SRC
|
|
* Deductive Information Retrieval
|
|
|
|
** A sample data base
|
|
#+name: knowledgebase
|
|
#+BEGIN_SRC scheme :tangle 4-4-1-kb.scheme
|
|
;; The personnel data base for Microshaft contains "assertions" about
|
|
;; company personnel. Here is the information about Ben Bitdiddle, the
|
|
;; resident computer wizard:
|
|
|
|
(address (Bitdiddle Ben) (Slumerville (Ridge Road) 10))
|
|
(job (Bitdiddle Ben) (computer wizard))
|
|
(salary (Bitdiddle Ben) 60000)
|
|
|
|
;; Each assertion is a list (in this case a triple) whose elements can
|
|
;; themselves be lists.
|
|
|
|
;; As resident wizard, Ben is in charge of the company's computer
|
|
;; division, and he supervises two programmers and one technician. Here
|
|
;; is the information about them:
|
|
|
|
(address (Hacker Alyssa P) (Cambridge (Mass Ave) 78))
|
|
(job (Hacker Alyssa P) (computer programmer))
|
|
(salary (Hacker Alyssa P) 40000)
|
|
(supervisor (Hacker Alyssa P) (Bitdiddle Ben))
|
|
|
|
(address (Fect Cy D) (Cambridge (Ames Street) 3))
|
|
(job (Fect Cy D) (computer programmer))
|
|
(salary (Fect Cy D) 35000)
|
|
(supervisor (Fect Cy D) (Bitdiddle Ben))
|
|
|
|
(address (Tweakit Lem E) (Boston (Bay State Road) 22))
|
|
(job (Tweakit Lem E) (computer technician))
|
|
(salary (Tweakit Lem E) 25000)
|
|
(supervisor (Tweakit Lem E) (Bitdiddle Ben))
|
|
|
|
;; There is also a programmer trainee, who is supervised by Alyssa:
|
|
|
|
(address (Reasoner Louis) (Slumerville (Pine Tree Road) 80))
|
|
(job (Reasoner Louis) (computer programmer trainee))
|
|
(salary (Reasoner Louis) 30000)
|
|
(supervisor (Reasoner Louis) (Hacker Alyssa P))
|
|
|
|
;; All of these people are in the computer division, as indicated by
|
|
;; the word `computer' as the first item in their job descriptions.
|
|
|
|
;; Ben is a high-level employee. His supervisor is the company's big
|
|
;; wheel himself:
|
|
|
|
(supervisor (Bitdiddle Ben) (Warbucks Oliver))
|
|
|
|
(address (Warbucks Oliver) (Swellesley (Top Heap Road)))
|
|
(job (Warbucks Oliver) (administration big wheel))
|
|
(salary (Warbucks Oliver) 150000)
|
|
|
|
;; Besides the computer division supervised by Ben, the company has an
|
|
;; accounting division, consisting of a chief accountant and his assistant:
|
|
|
|
(address (Scrooge Eben) (Weston (Shady Lane) 10))
|
|
(job (Scrooge Eben) (accounting chief accountant))
|
|
(salary (Scrooge Eben) 75000)
|
|
(supervisor (Scrooge Eben) (Warbucks Oliver))
|
|
|
|
(address (Cratchet Robert) (Allston (N Harvard Street) 16))
|
|
(job (Cratchet Robert) (accounting scrivener))
|
|
(salary (Cratchet Robert) 18000)
|
|
(supervisor (Cratchet Robert) (Scrooge Eben))
|
|
|
|
;; There is also a secretary for the big wheel:
|
|
|
|
(address (Aull DeWitt) (Slumerville (Onion Square) 5))
|
|
(job (Aull DeWitt) (administration secretary))
|
|
(salary (Aull DeWitt) 25000)
|
|
(supervisor (Aull DeWitt) (Warbucks Oliver))
|
|
|
|
;; The data base also contains assertions about which kinds of jobs can
|
|
;; be done by people holding other kinds of jobs. For instance, a
|
|
;; computer wizard can do the jobs of both a computer programmer and a
|
|
;; computer technician:
|
|
|
|
(can-do-job (computer wizard) (computer programmer))
|
|
(can-do-job (computer wizard) (computer technician))
|
|
|
|
;; A computer programmer could fill in for a trainee:
|
|
|
|
(can-do-job (computer programmer)
|
|
(computer programmer trainee))
|
|
|
|
;; Also, as is well known,
|
|
|
|
(can-do-job (administration secretary)
|
|
(administration big wheel))
|
|
#+END_SRC
|
|
|
|
*** Prolog
|
|
#+name: gen-pl-knowledgebase
|
|
#+BEGIN_SRC emacs-lisp :noweb yes :exports none
|
|
(defun pl-symbol (symbol)
|
|
(->> symbol
|
|
symbol-name
|
|
s-downcase
|
|
(s-replace "-" "_")))
|
|
|
|
(defun pl-sequence (sequence)
|
|
(s-join ", " (mapcar #'pl-term sequence)))
|
|
|
|
(defun pl-list (sequence)
|
|
(s-concat "["
|
|
(pl-sequence sequence)
|
|
"]"))
|
|
|
|
(defun pl-term (term)
|
|
(cond ((symbolp term) (pl-symbol term))
|
|
((listp term) (pl-list term))
|
|
(t (format "%s" term))))
|
|
|
|
(defun pl-fact (sequence)
|
|
(s-concat (pl-symbol (car sequence))
|
|
"("
|
|
(pl-sequence (cdr sequence))
|
|
")."))
|
|
|
|
(let ((facts (mapcar #'pl-fact (quote (
|
|
<<knowledgebase>>
|
|
)))))
|
|
(s-join "\n" (sort facts #'string-lessp)))
|
|
#+END_SRC
|
|
|
|
For the sake of having something to play with, the knowledgebase is
|
|
converted to prolog below:
|
|
|
|
#+name: pl-knowledgebase
|
|
#+caption: [[file:4-4-kb.pl]]
|
|
#+BEGIN_SRC prolog :noweb yes :tangle yes :exports code
|
|
%% -*- mode: prolog -*-
|
|
|
|
<<gen-pl-knowledgebase()>>
|
|
#+END_SRC
|
|
|
|
** Simple queries
|
|
|
|
Queries are performed by unifying patterns against known facts and
|
|
rules. Variables in patterns are bound as the pattern is matched, and
|
|
results are returned for all successful matches.
|
|
|
|
** Compound queries
|
|
|
|
#+BEGIN_QUOTE
|
|
Simple queries form the primitive operations of the query language.
|
|
In order to form compound operations, the query language provides
|
|
means of combination.
|
|
#+END_QUOTE
|
|
|
|
#+BEGIN_QUOTE
|
|
As for simple queries, the system processes a compound query by
|
|
finding all assignments to the pattern variables that satisfy the
|
|
query, then displaying instantiations of the query with those values.
|
|
#+END_QUOTE
|
|
|
|
*** Exercise 4.56
|
|
Formulate compound queries that retrieve the following information:
|
|
|
|
a. the names of all people who are supervised by Ben Bitdiddle,
|
|
together with their addresses;
|
|
|
|
----------------------------------------------------------------------
|
|
|
|
#+BEGIN_SRC scheme
|
|
(and (supervisor ?person (Bitdiddle Ben))
|
|
(address ?person ?where))
|
|
#+END_SRC
|
|
b. all people whose salary is less than Ben Bitdiddle's,
|
|
together with their salary and Ben Bitdiddle's salary;
|
|
|
|
----------------------------------------------------------------------
|
|
|
|
#+BEGIN_SRC scheme
|
|
(and (salary (Bitdiddle Ben) ?salary-ben)
|
|
(salary ?person ?salary-person)
|
|
(< ?salary-person ?salary-ben))
|
|
#+END_SRC
|
|
c. all people who are supervised by someone who is not in the
|
|
computer division, together with the supervisor's name and
|
|
job.
|
|
|
|
----------------------------------------------------------------------
|
|
|
|
#+BEGIN_SRC scheme
|
|
(and (supervisor ?person ?supervisor)
|
|
(job ?supervisor ?supervisor-job)
|
|
(not (job ?supervisor (computer . ?))))
|
|
#+END_SRC
|
|
|
|
** Rules
|
|
Rules are a tool for abstracting queries
|
|
|
|
#+BEGIN_SRC scheme
|
|
(rule (lives-near ?person-1 ?person-2)
|
|
(and (address ?person-1 (?town . ?rest-1))
|
|
(address ?person-2 (?town . ?rest-2))
|
|
(not (same ?person-1 ?person-2))))
|
|
#+END_SRC
|
|
|
|
The same rule would be expressed in Prolog as:
|
|
|
|
#+BEGIN_SRC prolog :tangle yes
|
|
lives_near(Person1, Person2) :-
|
|
address(Person1, [Town|_]),
|
|
address(Person2, [Town|_]),
|
|
Person1 \= Person2.
|
|
#+END_SRC
|
|
|
|
*** Exercise 4.57
|
|
Define a rule that says that person 1 can replace
|
|
person 2 if either person 1 does the same job as person 2 or
|
|
someone who does person 1's job can also do person 2's job, and if
|
|
person 1 and person 2 are not the same person. Using your rule,
|
|
give queries that find the following:
|
|
|
|
a. all people who can replace Cy D. Fect;
|
|
|
|
b. all people who can replace someone who is being paid more
|
|
than they are, together with the two salaries.
|
|
|
|
----------------------------------------------------------------------
|
|
|
|
#+BEGIN_SRC scheme
|
|
(rule (can-replace ?person-1 ?person-2)
|
|
(and (job ?person-1 ?job-1)
|
|
(job ?person-2 ?job-2)
|
|
(not (same ?person-1 ?person-2))
|
|
(or (same ?job-1 ?job-2)
|
|
(can-do-job ?job-1 ?job-2))))
|
|
|
|
(can-replace ?person (Cy D Fect))
|
|
|
|
(and (can-replace ?person-1 ?person-2)
|
|
(salary ?person-1 ?salary-1)
|
|
(salary ?person-2 ?salary-2)
|
|
(< ?salary-1 ?salary-2))
|
|
#+END_SRC
|
|
|
|
#+BEGIN_SRC prolog :tangle yes
|
|
can_replace(P1, P2) :-
|
|
job(P1, J1),
|
|
job(P2, J2),
|
|
(J1 == J2; can_do_job(J1, J2)),
|
|
P1 \= P2.
|
|
|
|
can_replace_for_cheap(P1, P2, S1, S2) :-
|
|
can_replace(P1, P2),
|
|
salary(P1, S1),
|
|
salary(P2, S2),
|
|
S1 > S2.
|
|
#+END_SRC
|
|
*** Exercise 4.58
|
|
Define a rule that says that a person is a "big shot" in a division if
|
|
the person works in the division but does not have a supervisor who
|
|
works in the division.
|
|
|
|
----------------------------------------------------------------------
|
|
|
|
#+BEGIN_SRC scheme
|
|
(rule (big-shot ?person)
|
|
(job ?person (?division . ?))
|
|
(supervisor ?person ?supervisor)
|
|
(not (job ?supervisor (?division . ?))))
|
|
#+END_SRC
|
|
|
|
#+BEGIN_SRC prolog
|
|
big_shot(Person) :-
|
|
job(Person, [Division|_]),
|
|
supervisor(Person, Supervisor),
|
|
job(Supervisor, [SDivision|_]),
|
|
Division \= SDivision.
|
|
#+END_SRC
|
|
|
|
*** Exercise 4.59
|
|
Ben Bitdiddle has missed one meeting too many.
|
|
Fearing that his habit of forgetting meetings could cost him his
|
|
job, Ben decides to do something about it. He adds all the weekly
|
|
meetings of the firm to the Microshaft data base by asserting the
|
|
following:
|
|
|
|
#+BEGIN_SRC scheme
|
|
(meeting accounting (Monday 9am))
|
|
(meeting administration (Monday 10am))
|
|
(meeting computer (Wednesday 3pm))
|
|
(meeting administration (Friday 1pm))
|
|
#+END_SRC
|
|
|
|
#+BEGIN_SRC prolog :tangle yes
|
|
meeting(accounting, [monday, '9am']).
|
|
meeting(administration, [monday, '10am']).
|
|
meeting(computer, [wednesday, '3pm']).
|
|
meeting(administration, [friday, '1pm']).
|
|
#+END_SRC
|
|
|
|
Each of the above assertions is for a meeting of an entire
|
|
division. Ben also adds an entry for the company-wide meeting
|
|
that spans all the divisions. All of the company's employees
|
|
attend this meeting.
|
|
|
|
#+BEGIN_SRC scheme
|
|
(meeting whole-company (Wednesday 4pm))
|
|
#+END_SRC
|
|
|
|
#+BEGIN_SRC prolog :tangle yes
|
|
meeting(whole_company, [wednesday, '4pm']).
|
|
#+END_SRC
|
|
|
|
a. On Friday morning, Ben wants to query the data base for all
|
|
the meetings that occur that day. What query should he use?
|
|
|
|
----------------------------------------------------------------------
|
|
|
|
#+BEGIN_SRC scheme
|
|
(meeting ?who (Friday ?when))
|
|
#+END_SRC
|
|
|
|
#+BEGIN_SRC prolog
|
|
meeting(Who, [friday, When]).
|
|
#+END_SRC
|
|
|
|
b. Alyssa P. Hacker is unimpressed. She thinks it would be much
|
|
more useful to be able to ask for her meetings by specifying
|
|
her name. So she designs a rule that says that a person's
|
|
meetings include all `whole-company' meetings plus all
|
|
meetings of that person's division. Fill in the body of
|
|
Alyssa's rule.
|
|
|
|
#+BEGIN_SRC scheme
|
|
(rule (meeting-time ?person ?day-and-time)
|
|
<RULE-BODY>)
|
|
#+END_SRC
|
|
|
|
----------------------------------------------------------------------
|
|
|
|
#+BEGIN_SRC scheme
|
|
(rule (meeting-time ?person ?day-and-time)
|
|
(and (job ?person (?department . ?))
|
|
(or (meeting whole-company ?day-and-time)
|
|
(meeting ?department ?day-and-time))))
|
|
#+END_SRC
|
|
|
|
#+BEGIN_SRC prolog :tangle yes
|
|
meeting_time(Person, DayAndTime) :-
|
|
job(Person, [Department|_]),
|
|
(meeting(whole_company, DayAndTime);
|
|
meeting(Department, DayAndTime)).
|
|
#+END_SRC
|
|
c. Alyssa arrives at work on Wednesday morning and wonders what
|
|
meetings she has to attend that day. Having defined the
|
|
above rule, what query should she make to find this out?
|
|
|
|
----------------------------------------------------------------------
|
|
|
|
#+BEGIN_SRC scheme
|
|
(meeting-time (Hacker Alyssa P) (Wednesday ?))
|
|
#+END_SRC
|
|
|
|
#+BEGIN_SRC prolog
|
|
meeting_time([hacker, alyssa, p], [wednesday, _]).
|
|
#+END_SRC
|
|
*** Exercise 4.60
|
|
By giving the query
|
|
|
|
#+BEGIN_SRC scheme
|
|
(lives-near ?person (Hacker Alyssa P))
|
|
#+END_SRC
|
|
|
|
Alyssa P. Hacker is able to find people who live near her, with
|
|
whom she can ride to work. On the other hand, when she tries to
|
|
find all pairs of people who live near each other by querying
|
|
|
|
#+BEGIN_SRC scheme
|
|
(lives-near ?person-1 ?person-2)
|
|
#+END_SRC
|
|
|
|
she notices that each pair of people who live near each other is
|
|
listed twice; for example,
|
|
|
|
#+BEGIN_SRC scheme
|
|
(lives-near (Hacker Alyssa P) (Fect Cy D))
|
|
(lives-near (Fect Cy D) (Hacker Alyssa P))
|
|
#+END_SRC
|
|
|
|
Why does this happen? Is there a way to find a list of people who
|
|
live near each other, in which each pair appears only once?
|
|
Explain.
|
|
|
|
** Logic as programs
|
|
#+BEGIN_SRC scheme
|
|
(rule (append-to-form () ?y ?y))
|
|
|
|
(rule (append-to-form (?u . ?v) ?y (?u . ?z))
|
|
(append-to-form ?v ?y ?z))
|
|
#+END_SRC
|
|
|
|
#+BEGIN_SRC prolog :tangle yes
|
|
append([], L, L).
|
|
append([H|T], L2, [H|L3]) :-
|
|
append(T, L2, L3).
|
|
#+END_SRC
|
|
|
|
* How the Query System Works
|
|
|
|
** Pattern matching
|
|
|
|
** Streams of frames
|
|
|
|
** Compound queries
|
|
|
|
** Unification
|
|
|
|
** Applying rules
|
|
|
|
** Simple queries
|
|
|
|
** The query evaluator and the driver loop
|
|
|
|
* Is Logic Programming Mathematical Logic?
|
|
|
|
** Infinite loops
|
|
|
|
** Problems with `not'
|
|
* Implementing the Query System
|
|
** The Driver Loop and Instantiation
|
|
#+BEGIN_SRC scheme :tangle yes
|
|
(define (query-driver-loop)
|
|
(prompt-for-input input-prompt)
|
|
(let ((q (query-syntax-process (read))))
|
|
(cond ((assertion-to-be-added? q)
|
|
(add-rule-or-assertion! (add-assertion-body q))
|
|
(newline)
|
|
(display "Assertion added to data base.")
|
|
(query-driver-loop))
|
|
(else
|
|
(newline)
|
|
(display output-prompt)
|
|
(display-stream
|
|
(stream-map
|
|
(lambda (frame)
|
|
(instantiate q
|
|
frame
|
|
(lambda (v f)
|
|
(contract-question-mark v))))
|
|
(qeval q (singleton-stream '()))))
|
|
(query-driver-loop)))))
|
|
#+END_SRC
|
|
#+BEGIN_SRC scheme :tangle yes
|
|
(define (instantiate exp frame unbound-var-handler)
|
|
(define (copy exp)
|
|
(cond ((var? exp)
|
|
(let ((binding (binding-in-frame exp frame)))
|
|
(if binding
|
|
(copy (binding-value binding))
|
|
(unbound-var-handler exp frame))))
|
|
((pair? exp)
|
|
(cons (copy (car exp)) (copy (cdr exp))))
|
|
(else exp)))
|
|
(copy exp))
|
|
#+END_SRC
|
|
** The Evaluator
|
|
#+BEGIN_SRC scheme :tangle yes
|
|
(define (qeval query frame-stream)
|
|
(let ((qproc (get (type query) 'qeval)))
|
|
(if qproc
|
|
(qproc (contents query) frame-stream)
|
|
(simple-query query frame-stream))))
|
|
#+END_SRC
|
|
*** Simple queries
|
|
#+BEGIN_SRC scheme :tangle yes
|
|
(define (simple-query query-pattern frame-stream)
|
|
(stream-flatmap
|
|
(lambda (frame)
|
|
(stream-append-delayed
|
|
(find-assertions query-pattern frame)
|
|
(delay (apply-rules query-pattern frame))))
|
|
frame-stream))
|
|
#+END_SRC
|
|
*** Compound queries
|
|
#+BEGIN_SRC scheme :tangle yes
|
|
(define (conjoin conjuncts frame-stream)
|
|
(if (empty-conjunction? conjuncts)
|
|
frame-stream
|
|
(conjoin (rest-conjuncts conjuncts)
|
|
(qeval (first-conjunct conjuncts)
|
|
frame-stream))))
|
|
|
|
(put 'and 'qeval conjoin)
|
|
#+END_SRC
|
|
#+BEGIN_SRC scheme :tangle yes
|
|
(define (disjoin disjuncts frame-stream)
|
|
(if (empty-disjunction? disjuncts)
|
|
the-empty-stream
|
|
(interleave-delayed
|
|
(qeval (first-disjunct disjuncts) frame-stream)
|
|
(delay (disjoin (rest-disjuncts disjuncts)
|
|
frame-stream)))))
|
|
|
|
(put 'or 'qeval disjoin)
|
|
#+END_SRC
|
|
*** Filters
|
|
#+BEGIN_SRC scheme :tangle yes
|
|
(define (negate operands frame-stream)
|
|
(stream-flatmap
|
|
(lambda (frame)
|
|
(if (stream-null? (qeval (negated-query operands)
|
|
(singleton-stream frame)))
|
|
(singleton-stream frame)
|
|
the-empty-stream))
|
|
frame-stream))
|
|
|
|
(put 'not 'qeval negate)
|
|
#+END_SRC
|
|
#+BEGIN_SRC scheme :tangle yes
|
|
(define (lisp-value call frame-stream)
|
|
(stream-flatmap
|
|
(lambda (frame)
|
|
(if (execute
|
|
(instantiate
|
|
call
|
|
frame
|
|
(lambda (v f)
|
|
(error "Unknown pat var -- LISP-VALUE" v))))
|
|
(singleton-stream frame)
|
|
the-empty-stream))
|
|
frame-stream))
|
|
|
|
(put 'lisp-value 'qeval lisp-value)
|
|
#+END_SRC
|
|
#+BEGIN_SRC scheme :tangle yes
|
|
(define (execute exp)
|
|
(apply (eval (predicate exp) user-initial-environment)
|
|
(args exp)))
|
|
#+END_SRC
|
|
#+BEGIN_SRC scheme :tangle yes
|
|
(define (always-true ignore frame-stream) frame-stream)
|
|
|
|
(put 'always-true 'qeval always-true)
|
|
#+END_SRC
|
|
** Finding Assertions by Pattern Matching
|
|
#+BEGIN_SRC scheme :tangle yes
|
|
(define (find-assertions pattern frame)
|
|
(stream-flatmap (lambda (datum)
|
|
(check-an-assertion datum pattern frame))
|
|
(fetch-assertions pattern frame)))
|
|
#+END_SRC
|
|
#+BEGIN_SRC scheme :tangle yes
|
|
(define (check-an-assertion assertion query-pat query-frame)
|
|
(let ((match-result
|
|
(pattern-match query-pat assertion query-frame)))
|
|
(if (eq? match-result 'failed)
|
|
the-empty-stream
|
|
(singleton-stream match-result))))
|
|
#+END_SRC
|
|
#+BEGIN_SRC scheme :tangle yes
|
|
(define (pattern-match pat dat frame)
|
|
(cond ((eq? frame 'failed) 'failed)
|
|
((equal? pat dat) frame)
|
|
((var? pat) (extend-if-consistent pat dat frame))
|
|
((and (pair? pat) (pair? dat))
|
|
(pattern-match (cdr pat)
|
|
(cdr dat)
|
|
(pattern-match (car pat)
|
|
(car dat)
|
|
frame)))
|
|
(else 'failed)))
|
|
#+END_SRC
|
|
#+BEGIN_SRC scheme :tangle yes
|
|
(define (extend-if-consistent var dat frame)
|
|
(let ((binding (binding-in-frame var frame)))
|
|
(if binding
|
|
(pattern-match (binding-value binding) dat frame)
|
|
(extend var dat frame))))
|
|
#+END_SRC
|
|
** Rules and Unification
|
|
#+BEGIN_SRC scheme :tangle yes
|
|
(define (apply-rules pattern frame)
|
|
(stream-flatmap (lambda (rule)
|
|
(apply-a-rule rule pattern frame))
|
|
(fetch-rules pattern frame)))
|
|
#+END_SRC
|
|
#+BEGIN_SRC scheme :tangle yes
|
|
(define (apply-a-rule rule query-pattern query-frame)
|
|
(let ((clean-rule (rename-variables-in rule)))
|
|
(let ((unify-result
|
|
(unify-match query-pattern
|
|
(conclusion clean-rule)
|
|
query-frame)))
|
|
(if (eq? unify-result 'failed)
|
|
the-empty-stream
|
|
(qeval (rule-body clean-rule)
|
|
(singleton-stream unify-result))))))
|
|
#+END_SRC
|
|
#+BEGIN_SRC scheme :tangle yes
|
|
(define (rename-variables-in rule)
|
|
(let ((rule-application-id (new-rule-application-id)))
|
|
(define (tree-walk exp)
|
|
(cond ((var? exp)
|
|
(make-new-variable exp rule-application-id))
|
|
((pair? exp)
|
|
(cons (tree-walk (car exp))
|
|
(tree-walk (cdr exp))))
|
|
(else exp)))
|
|
(tree-walk rule)))
|
|
#+END_SRC
|
|
#+BEGIN_SRC scheme :tangle yes
|
|
(define (unify-match p1 p2 frame)
|
|
(cond ((eq? frame 'failed) 'failed)
|
|
((equal? p1 p2) frame)
|
|
((var? p1) (extend-if-possible p1 p2 frame))
|
|
((var? p2) (extend-if-possible p2 p1 frame)) ; ***
|
|
((and (pair? p1) (pair? p2))
|
|
(unify-match (cdr p1)
|
|
(cdr p2)
|
|
(unify-match (car p1)
|
|
(car p2)
|
|
frame)))
|
|
(else 'failed)))
|
|
#+END_SRC
|
|
#+BEGIN_SRC scheme :tangle yes
|
|
(define (extend-if-possible var val frame)
|
|
(let ((binding (binding-in-frame var frame)))
|
|
(cond (binding
|
|
(unify-match
|
|
(binding-value binding) val frame))
|
|
((var? val) ; ***
|
|
(let ((binding (binding-in-frame val frame)))
|
|
(if binding
|
|
(unify-match
|
|
var (binding-value binding) frame)
|
|
(extend var val frame))))
|
|
((depends-on? val var frame) ; ***
|
|
'failed)
|
|
(else (extend var val frame)))))
|
|
#+END_SRC
|
|
#+BEGIN_SRC scheme :tangle yes
|
|
(define (depends-on? exp var frame)
|
|
(define (tree-walk e)
|
|
(cond ((var? e)
|
|
(if (equal? var e)
|
|
true
|
|
(let ((b (binding-in-frame e frame)))
|
|
(if b
|
|
(tree-walk (binding-value b))
|
|
false))))
|
|
((pair? e)
|
|
(or (tree-walk (car e))
|
|
(tree-walk (cdr e))))
|
|
(else false)))
|
|
(tree-walk exp))
|
|
#+END_SRC
|
|
** Maintaining the Data Base
|
|
#+BEGIN_SRC scheme :tangle yes
|
|
(define THE-ASSERTIONS the-empty-stream)
|
|
|
|
(define (fetch-assertions pattern frame)
|
|
(if (use-index? pattern)
|
|
(get-indexed-assertions pattern)
|
|
(get-all-assertions)))
|
|
|
|
(define (get-all-assertions) THE-ASSERTIONS)
|
|
|
|
(define (get-indexed-assertions pattern)
|
|
(get-stream (index-key-of pattern) 'assertion-stream))
|
|
#+END_SRC
|
|
#+BEGIN_SRC scheme :tangle yes
|
|
(define (get-stream key1 key2)
|
|
(let ((s (get key1 key2)))
|
|
(if s s the-empty-stream)))
|
|
#+END_SRC
|
|
#+BEGIN_SRC scheme :tangle yes
|
|
(define THE-RULES the-empty-stream)
|
|
|
|
(define (fetch-rules pattern frame)
|
|
(if (use-index? pattern)
|
|
(get-indexed-rules pattern)
|
|
(get-all-rules)))
|
|
|
|
(define (get-all-rules) THE-RULES)
|
|
|
|
(define (get-indexed-rules pattern)
|
|
(stream-append
|
|
(get-stream (index-key-of pattern) 'rule-stream)
|
|
(get-stream '? 'rule-stream)))
|
|
#+END_SRC
|
|
#+BEGIN_SRC scheme :tangle yes
|
|
(define (add-rule-or-assertion! assertion)
|
|
(if (rule? assertion)
|
|
(add-rule! assertion)
|
|
(add-assertion! assertion)))
|
|
|
|
(define (add-assertion! assertion)
|
|
(store-assertion-in-index assertion)
|
|
(let ((old-assertions THE-ASSERTIONS))
|
|
(set! THE-ASSERTIONS
|
|
(cons-stream assertion old-assertions))
|
|
'ok))
|
|
|
|
(define (add-rule! rule)
|
|
(store-rule-in-index rule)
|
|
(let ((old-rules THE-RULES))
|
|
(set! THE-RULES (cons-stream rule old-rules))
|
|
'ok))
|
|
#+END_SRC
|
|
#+BEGIN_SRC scheme :tangle yes
|
|
(define (store-assertion-in-index assertion)
|
|
(if (indexable? assertion)
|
|
(let ((key (index-key-of assertion)))
|
|
(let ((current-assertion-stream
|
|
(get-stream key 'assertion-stream)))
|
|
(put key
|
|
'assertion-stream
|
|
(cons-stream assertion
|
|
current-assertion-stream))))))
|
|
|
|
(define (store-rule-in-index rule)
|
|
(let ((pattern (conclusion rule)))
|
|
(if (indexable? pattern)
|
|
(let ((key (index-key-of pattern)))
|
|
(let ((current-rule-stream
|
|
(get-stream key 'rule-stream)))
|
|
(put key
|
|
'rule-stream
|
|
(cons-stream rule
|
|
current-rule-stream)))))))
|
|
#+END_SRC
|
|
#+BEGIN_SRC scheme :tangle yes
|
|
(define (indexable? pat)
|
|
(or (constant-symbol? (car pat))
|
|
(var? (car pat))))
|
|
#+END_SRC
|
|
#+BEGIN_SRC scheme :tangle yes
|
|
(define (index-key-of pat)
|
|
(let ((key (car pat)))
|
|
(if (var? key) '? key)))
|
|
#+END_SRC
|
|
#+BEGIN_SRC scheme :tangle yes
|
|
(define (use-index? pat)
|
|
(constant-symbol? (car pat)))
|
|
#+END_SRC
|
|
** Stream Operations
|
|
#+BEGIN_SRC scheme :tangle yes
|
|
(define (stream-append-delayed s1 delayed-s2)
|
|
(if (stream-null? s1)
|
|
(force delayed-s2)
|
|
(cons-stream
|
|
(stream-car s1)
|
|
(stream-append-delayed (stream-cdr s1) delayed-s2))))
|
|
|
|
(define (interleave-delayed s1 delayed-s2)
|
|
(if (stream-null? s1)
|
|
(force delayed-s2)
|
|
(cons-stream
|
|
(stream-car s1)
|
|
(interleave-delayed (force delayed-s2)
|
|
(delay (stream-cdr s1))))))
|
|
#+END_SRC
|
|
#+BEGIN_SRC scheme :tangle yes
|
|
(define (stream-flatmap proc s)
|
|
(flatten-stream (stream-map proc s)))
|
|
|
|
(define (flatten-stream stream)
|
|
(if (stream-null? stream)
|
|
the-empty-stream
|
|
(interleave-delayed
|
|
(stream-car stream)
|
|
(delay (flatten-stream (stream-cdr stream))))))
|
|
#+END_SRC
|
|
#+BEGIN_SRC scheme :tangle yes
|
|
(define (singleton-stream x)
|
|
(cons-stream x the-empty-stream))
|
|
#+END_SRC
|
|
** Query Syntax Procedures
|
|
#+BEGIN_SRC scheme :tangle yes
|
|
(define (type exp)
|
|
(if (pair? exp)
|
|
(car exp)
|
|
(error "Unknown expression TYPE" exp)))
|
|
|
|
(define (contents exp)
|
|
(if (pair? exp)
|
|
(cdr exp)
|
|
(error "Unknown expression CONTENTS" exp)))
|
|
#+END_SRC
|
|
#+BEGIN_SRC scheme :tangle yes
|
|
(define (assertion-to-be-added? exp)
|
|
(eq? (type exp) 'assert!))
|
|
|
|
(define (add-assertion-body exp)
|
|
(car (contents exp)))
|
|
#+END_SRC
|
|
#+BEGIN_SRC scheme :tangle yes
|
|
(define (empty-conjunction? exps) (null? exps))
|
|
(define (first-conjunct exps) (car exps))
|
|
(define (rest-conjuncts exps) (cdr exps))
|
|
|
|
(define (empty-disjunction? exps) (null? exps))
|
|
(define (first-disjunct exps) (car exps))
|
|
(define (rest-disjuncts exps) (cdr exps))
|
|
|
|
(define (negated-query exps) (car exps))
|
|
|
|
(define (predicate exps) (car exps))
|
|
(define (args exps) (cdr exps))
|
|
#+END_SRC
|
|
#+BEGIN_SRC scheme :tangle yes
|
|
(define (rule? statement)
|
|
(tagged-list? statement 'rule))
|
|
|
|
(define (conclusion rule) (cadr rule))
|
|
|
|
(define (rule-body rule)
|
|
(if (null? (cddr rule))
|
|
'(always-true)
|
|
(caddr rule)))
|
|
#+END_SRC
|
|
#+BEGIN_SRC scheme :tangle yes
|
|
(define (query-syntax-process exp)
|
|
(map-over-symbols expand-question-mark exp))
|
|
|
|
(define (map-over-symbols proc exp)
|
|
(cond ((pair? exp)
|
|
(cons (map-over-symbols proc (car exp))
|
|
(map-over-symbols proc (cdr exp))))
|
|
((symbol? exp) (proc exp))
|
|
(else exp)))
|
|
|
|
(define (expand-question-mark symbol)
|
|
(let ((chars (symbol->string symbol)))
|
|
(if (string=? (substring chars 0 1) "?")
|
|
(list '?
|
|
(string->symbol
|
|
(substring chars 1 (string-length chars))))
|
|
symbol)))
|
|
#+END_SRC
|
|
#+BEGIN_SRC scheme :tangle yes
|
|
(define (var? exp)
|
|
(tagged-list? exp '?))
|
|
|
|
(define (constant-symbol? exp) (symbol? exp))
|
|
#+END_SRC
|
|
#+BEGIN_SRC scheme :tangle yes
|
|
(define rule-counter 0)
|
|
|
|
(define (new-rule-application-id)
|
|
(set! rule-counter (+ 1 rule-counter))
|
|
rule-counter)
|
|
|
|
(define (make-new-variable var rule-application-id)
|
|
(cons '? (cons rule-application-id (cdr var))))
|
|
#+END_SRC
|
|
#+BEGIN_SRC scheme :tangle yes
|
|
(define (contract-question-mark variable)
|
|
(string->symbol
|
|
(string-append "?"
|
|
(if (number? (cadr variable))
|
|
(string-append (symbol->string (caddr variable))
|
|
"-"
|
|
(number->string (cadr variable)))
|
|
(symbol->string (cadr variable))))))
|
|
#+END_SRC
|
|
** Frames and Bindings
|
|
#+BEGIN_SRC scheme :tangle yes
|
|
(define (make-binding variable value)
|
|
(cons variable value))
|
|
|
|
(define (binding-variable binding)
|
|
(car binding))
|
|
|
|
(define (binding-value binding)
|
|
(cdr binding))
|
|
|
|
(define (binding-in-frame variable frame)
|
|
(assoc variable frame))
|
|
|
|
(define (extend variable value frame)
|
|
(cons (make-binding variable value) frame))
|
|
#+END_SRC
|