Initial import of files for Cardboard Prolog.
Chris Pressey
4 years ago
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)))))))) |