git @ Cat's Eye Technologies Cardboard-Prolog / master
Initial import of files for Cardboard Prolog. Chris Pressey 1 year, 10 months ago
5 changed file(s) with 434 addition(s) and 0 deletion(s). Raw diff Collapse all Expand all
0 Cardboard Prolog
1 ================
2
3 This is a tiny inference engine (~120 lines of purely functional R5RS
4 Scheme) I wrote a while back, when I was refreshing myself on how a
5 Prolog interpreter works. I found several descriptions and examples
6 of Prolog interpreters online, but none were quite what I wanted.
7
8 Cardboard Prolog lacks all the amenties the Prolog language proper, and
9 it uses Scheme literals instead of Prolog syntax, but it does do the thing
10 that's at the core of Prolog execution: deduction based on Horn clauses.
11
12 There are no comments, but there is a suite of tests. You can run the
13 tests with (for example) Chicken Scheme, by running
14
15 csi -b test-cardboard-prolog.scm
16
17 I'll also try to briefly describe what's going on here.
18
19 ### Overview of the Design and Implementation
20
21 A term in Cardboard Prolog is represented by a Scheme list, where atoms
22 are symbols and variables are vectors of length 1 or 2. The first
23 entry of a variable vector is a symbol giving the variable name, and the
24 second entry is an index which is used to disambiguate different instances
25 of a variable.
26
27 `ground?` and `variable?` are predicates on terms.
28
29 `rename-term` takes a term and returns a new term which is the same as
30 the input term except that all variables are given new indexes. The
31 purpose is to obtain a "fresh" version of the term with no bound variables.
32
33 `collect-vars` takes a term and returns a list of all variables found
34 in it.
35
36 `match-var` and `unify` are mutually-recursive functions which implement
37 unification. `unify` takes two patterns (terms which may contain
38 variables) and returns a list of bindings if the each pattern matches
39 the other, or `#f` if they cannot be matched. Such a list of bindings
40 is called an "environment" (abbreviated `env`) in this code. Each binding
41 is a two-element list of a variable, and the subterm that it matched with,
42 which may itself be a variable, or contain variables.
43
44 Note that, for simplicitly, the unification algorithm here does not perform
45 an occurs check. For the sake of correctness, it should perform one, but
46 since it's very easy to implement and doesn't really add explanatory value
47 to the exposition, I left it out. You can undertake adding one as an
48 exercise, if you like.
49
50 `expand` takes a term and an environment and returns a new term which
51 is the same as the input term except that all variables are replaced
52 with the terms that they are bound to in the environment. `subst` is a
53 helper function used by `expand`.
54
55 During the search process, a variable like `#(X)` will be instantiated
56 to a variable like `#(X 2)` (where 2 indicates the depth of the search),
57 and it is `#(X 2)` that will match a term, but this information is
58 usually irrelevant to the user, for whom the report that `#(X)` matched
59 would be more meaningful. `collapse-env` (with its helper functions
60 `expand-env` and `expand-binding`) and `restrict-to-vars` are used clean
61 up the output of the engine, and make its results more presentable to
62 the user in this way.
63
64 `search` implements the core inference process. It is given a database
65 (a list of facts and rules, where a fact is simply a rule with no
66 premises), and a list of goals. It keeps track of the current
67 environment (list of bindings) and the current search depth.
68
69 `search` tries to `unify` each rule in the database with the first goal
70 of the current list of goals, under the current environment. If this
71 succeeds, it takes the unifying environment (which we now call a
72 "unifier"), `expand`s the consequent of the rule and the remaining goals
73 using the unifier, joins these together to obtain a new list of goals,
74 and recursively calls itself with the new list of goals and the new
75 environment, to continue to the search. If there are no more goals in
76 the list to satisfy, the search was a success and the final unifying
77 environment is returned.
78
79 But note that `search` might actually return to itself, because it
80 calls itself recursively. So it returns a list of unifying environments,
81 and collects these lists to ultimately return all of the successful searches
82 in the database.
83
84 A real Prolog interpreter would do this piecemeal, asking the user if they
85 want it to search for the next answer after each answer is found. For
86 simplicitly, Cardboard Prolog always returns all the answers, and
87 if there are infinitely many answers, this will simply not terminate.
88
89 (This design choice was for simplicitly, but it would certainly be
90 an interesting exercise to rewrite it to work in the fashion of Prolog.
91 Many of the descriptions I found online did describe how Prolog
92 interpreters accomplish this, but none of them phrased it in terms of
93 continuations, which is probably how you'd want to do it in Scheme.)
94
95 Finally, `match-all` is a driver function for `search`, and the main
96 interface to the inference engine. It takes a database and a list of
97 goals, and returns a list of comprehensible answers.
0 This is free and unencumbered software released into the public domain.
1
2 Anyone is free to copy, modify, publish, use, compile, sell, or
3 distribute this software, either in source code form or as a compiled
4 binary, for any purpose, commercial or non-commercial, and by any
5 means.
6
7 In jurisdictions that recognize copyright laws, the author or authors
8 of this software dedicate any and all copyright interest in the
9 software to the public domain. We make this dedication for the benefit
10 of the public at large and to the detriment of our heirs and
11 successors. We intend this dedication to be an overt act of
12 relinquishment in perpetuity of all present and future rights to this
13 software under copyright law.
14
15 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
16 EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
17 MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
18 IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY CLAIM, DAMAGES OR
19 OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
20 ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
21 OTHER DEALINGS IN THE SOFTWARE.
22
23 For more information, please refer to <http://unlicense.org/>
0 (define (foldl fun acc list)
1 (if (null? list) acc (foldl fun (fun (car list) acc) (cdr list))))
2
3 (define (ground? t)
4 (or (null? t) (symbol? t)))
5
6 (define (variable? v)
7 (vector? v))
8
9 (define (rename-variable v n)
10 (vector (vector-ref v 0) n))
11
12 (define (rename-term term n)
13 (cond
14 ((ground? term)
15 term)
16 ((variable? term)
17 (rename-variable term n))
18 (else
19 (map (lambda (t) (rename-term t n)) term))))
20
21 (define (collect-vars term acc)
22 (cond
23 ((ground? term)
24 acc)
25 ((variable? term)
26 (cons term acc))
27 (else
28 (foldl (lambda (t inner-acc) (collect-vars t inner-acc)) acc term))))
29
30 (define (match-var var pattern env)
31 (if (equal? var pattern)
32 env
33 (let* ( (binding (assoc var env)) )
34 (cond
35 (binding
36 (unify (cadr binding) pattern env))
37 (else
38 (cons (list var pattern) env))))))
39
40 (define (unify p1 p2 env)
41 (cond
42 ((equal? env #f)
43 #f)
44 ((variable? p1)
45 (match-var p1 p2 env))
46 ((variable? p2)
47 (match-var p2 p1 env))
48 ((or (ground? p1) (ground? p2))
49 (if (equal? p1 p2)
50 env
51 #f))
52 (else
53 (let* ( (head-env (unify (car p1) (car p2) env))
54 (tail-env (unify (cdr p1) (cdr p2) head-env)) )
55 tail-env))))
56
57 (define (expand term env)
58 (if (null? env)
59 term
60 (let* ( (binding (car env))
61 (var (car binding))
62 (bound-to (cadr binding)) )
63 (expand (subst var bound-to term) (cdr env)))))
64
65 (define (subst var replacement term)
66 (cond
67 ((ground? term)
68 term)
69 ((variable? term)
70 (if (equal? term var) replacement term))
71 (else
72 (map (lambda (t) (subst var replacement t)) term))))
73
74 (define (expand-binding binding env)
75 (cons (car binding) (expand (cdr binding) env)))
76
77 (define (expand-env e env)
78 (map (lambda (binding) (expand-binding binding env)) e))
79
80 (define (collapse-env env)
81 (let* ( (new-env (expand-env env env)) )
82 (if (equal? env new-env)
83 new-env
84 (collapse-env new-env))))
85
86 (define (restrict-to-vars env vars)
87 (if (null? env)
88 env
89 (let* ( (binding (car env)) )
90 (if (member (car binding) vars)
91 (cons binding (restrict-to-vars (cdr env) vars))
92 (restrict-to-vars (cdr env) vars)))))
93
94 (define (search database goals env depth)
95 (if (null? goals)
96 (list env)
97 (foldl (lambda (clause acc)
98 (let* ( (fresh-clause (rename-term clause depth))
99 (head (car fresh-clause))
100 (body (cdr fresh-clause))
101 (unifier (unify (car goals) head env)) )
102 (if unifier
103 (let* ( (expanded-goals (map (lambda (g) (expand g unifier)) (cdr goals)))
104 (expanded-body (map (lambda (t) (expand t unifier)) body))
105 (new-goals (append expanded-body expanded-goals))
106 (new-acc (append acc (search database new-goals unifier (+ 1 depth)))) )
107 new-acc)
108 acc))) '() database)))
109
110 (define (match-all database goals)
111 (let* ( (toplevel-vars (collect-vars goals '()))
112 (unifiers (search database goals '() 1))
113 (results (map (lambda (u) (collapse-env u)) unifiers)) )
114 (map (lambda (u) (restrict-to-vars u toplevel-vars)) results)))
0 (load "cardboard-prolog.scm")
1 (load "utils.scm")
2
3 (define database
4 '(
5 ((female alice))
6 ((male bob))
7 ((male dan))
8 ((female emily))
9 ((female fran))
10 ((child alice bob))
11 ((child dan bob))
12 ((child emily dan))
13 ((son #(X) #(Y)) (male #(X)) (child #(X) #(Y)))
14 ((daughter #(X) #(Y)) (female #(X)) (child #(X) #(Y)))
15 ((descendant #(X) #(Y)) (child #(X) #(Y)))
16 ((descendant #(X) #(Y)) (child #(X) #(Z)) (descendant #(Z) #(Y)))
17 )
18 )
19
20 ;-----------
21
22 (test rename-term-1
23 (rename-term '(descendant #(X) #(Y)) 1)
24 '(descendant #(X 1) #(Y 1))
25 )
26
27 (test rename-term-2
28 (rename-term '(descendant #(X 1) #(Y 1)) 2)
29 '(descendant #(X 2) #(Y 2))
30 )
31
32 (test collect-vars-1
33 (collect-vars '(descendant (son #(X)) #(Y)) '())
34 '(#(Y) #(X))
35 )
36
37 ;------------
38
39 (test unify-1
40 (unify '(child bob #(Y)) '(child #(X) alice) '())
41 '( (#(Y) alice) (#(X) bob) )
42 )
43
44 (test unify-2
45 (unify '(son #(X) zeke) '(son #(X) #(Y)) '())
46 '( (#(Y) zeke) )
47 )
48
49 (test unify-3
50 (unify '(son #(P) zeke) '(son #(X) #(Y)) '())
51 '( (#(Y) zeke) (#(P) #(X)) )
52 )
53
54 ;------------
55
56 (test expand-1
57 (expand '(child #(X) #(Y)) '( (#(Y) alice) (#(X) bob) ))
58 '(child bob alice)
59 )
60
61 ;------------
62
63 (test match-all-1
64 (match-all database '( (female alice) ))
65 '(()) ; list containing empty env ==> true
66 )
67
68 (test match-all-2
69 (match-all database '( (female foobar) ))
70 '() ; list containing no envs ==> false
71 )
72
73 (test match-all-3
74 (match-all database '( (female #(A)) ))
75 '(((#(A) alice)) ((#(A) emily)) ((#(A) fran)))
76 )
77
78 (test match-all-4
79 (match-all database '( (child dan bob) ))
80 '(())
81 )
82
83 (test match-all-5
84 (match-all database '( (child #(A) bob) ))
85 '(((#(A) alice)) ((#(A) dan)))
86 )
87
88 (test match-all-6
89 (match-all database '( (female #(A)) (child #(A) bob) ))
90 '(((#(A) alice)))
91 )
92
93 (test match-all-7
94 (match-all database '( (female #(A)) (child #(A) #(B)) ))
95 '(((#(B) bob) (#(A) alice)) ((#(B) dan) (#(A) emily)))
96 )
97
98 (test match-all-son-1
99 (match-all database '( (son dan bob) ))
100 '(())
101 )
102
103 (test match-all-son-2
104 (match-all database '( (son dan emily) ))
105 '()
106 )
107
108 (test match-all-son-3
109 (match-all database '( (son alice bob) ))
110 '()
111 )
112
113 (test match-all-son-3a
114 (match-all database '( (son #(X) bob) ))
115 '(((#(X) dan)))
116 )
117
118 (test match-all-son-3b
119 (match-all database '( (son #(P) bob) ))
120 '(((#(P) dan)))
121 )
122
123 (test match-all-son-4
124 (match-all database '( (son dan #(X)) ))
125 '(((#(X) bob)))
126 )
127
128 (test match-all-son-4a
129 (match-all database '( (son dan #(P)) ))
130 '(((#(P) bob)))
131 )
132
133 (test match-all-son-5
134 (match-all database '( (son #(X) #(Y)) ))
135 '(((#(Y) bob) (#(X) dan)))
136 )
137
138 (test match-all-son-5a
139 (match-all database '( (son #(P) #(Q)) ))
140 '(((#(Q) bob) (#(P) dan)))
141 )
142
143 (test match-all-descendant-1
144 (match-all database '( (descendant alice bob) ))
145 '(())
146 )
147
148 (test match-all-descendant-2
149 (match-all database '( (descendant alice emily) ))
150 '()
151 )
152
153 (test match-all-descendant-3
154 (match-all database '( (descendant emily bob) ))
155 '(())
156 )
157
158 (test match-all-descendant-4
159 (match-all database '( (descendant #(X) bob) ))
160 '(((#(X) alice)) ((#(X) dan)) ((#(X) emily)))
161 )
162
163 (test match-all-descendant-5
164 (match-all database '( (descendant emily #(X)) ))
165 '(((#(X) dan)) ((#(X) bob)))
166 )
0 (define-syntax print
1 (syntax-rules ()
2 ((print e)
3 (display e))
4 ((print e1 e2 ...)
5 (begin (display e1)
6 (print e2 ...)))))
7
8 (define-syntax println
9 (syntax-rules ()
10 ((println e)
11 (begin (display e)
12 (newline)))
13 ((println e1 e2 ...)
14 (begin (display e1)
15 (println e2 ...)))))
16
17 (define-syntax test
18 (syntax-rules ()
19 ((test test-name expr expected)
20 (begin
21 (print "Running test: " (quote test-name) "... ")
22 (let ((result expr))
23 (cond
24 ((equal? result expected)
25 (println "passed."))
26 (else
27 (println "FAILED!")
28 (println "Expected: " expected)
29 (println "Actual: " result))))))))