Initial import of files for Cardboard Prolog.
Chris Pressey
1 year, 5 months 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)))))))) |