; Boolean functions are functions from set {0, 1} to set {0, 1}.
; Our well known logical connectives and, or and not are such
; Boolean functions. In usual mathematical notation, it would be
; written:
;
; or(0,0)=0; or(0,1)=1; or(1,0)=1; or(1,1)=1.
;
; Frequently, Booleans functions are defined in the form of the
; "truth-table".
;
; a b (or a b)
; ---------------
; 0 0 0
; 0 1 1
; 1 0 1
; 1 1 1
;
; Boolean function is determined by third column, in this case,
; 0111. For each Boolean function, there are many possible formulas
; that define the function. In our example (or a b), but also
; (not (and a b)), (and (not a) (not b)), (-> (not a) b), and
; many others. Boolean functions and propositional formulas are very
; important, because computers are machines that calculate boolean
; functions, using physical realization of proposition formulas.
;
; The following program analyzes given list of all propositional
; formulas, and search for minimal between equivalent formulas.
;
; For all formulas f in list (f0 f1 ... fn),
;
; (i) Boolean function B defined with f is found
; (ii) it is tested whether f is a first formula that defines B,
; or it is shorter than other formulas defining B.
;
; The program builds data structure, defining and using symbols.
; For example, if list ((or a b) (not (and a b)) (-> (not a) b)) is
; given, the program would first found that (or a b) defines Boolean
; function given with column 0111 in truth table. Then it would define
; two symbols and values:
;
; [Boolean-function.0111] => ((or a b))
; [propositional-formulas.(or a b)] => [Boolean-function.0111]
;
; After that, (not (and a b)) is found to define same Boolean function,
; but it is longer than (or a b), so nothing changes. If some shorter
; formula defining same Boolean function is found, then
; value [Boolean-function.0111] would be redefined.
;
; In this program, symbols are used instead of hash tables, in some
; other languages, where syntax would be something like
; Boolean-function[0111] instead. One might be surprised with such
; use of the symbols, and think it is abuse of the symbols. But,
; I think it is actually apropriate use, because, in general case,
; there is no reasons for distinction between hash table name,
; and key.
;
; In following program, such procedure is applied on all formulas
; with seven or less "nodes", and finally, all defined Boolean
; functions, and shortest formulas defining these Boolean functions
; are printed.
(set '[println.supressed] true '[print.supressed] true)
(load "http://www.instprog.com/Instprog.default-library.lsp")
(set '[println.supressed] nil '[print.supressed] nil)
(set 'PF (apply append (map (lambda(x)(all-pf x '(true nil A B C)
'(not)
'(and or -> <->)))
(sequence 1 7))))
(box-standard "Generated " (length PF) " formulas.")
(set 'truth-column
(lambda(f)(let ((result '()))
(letex((L (propositional-variables f)))
(dolist-multi(L '(nil true))
(push (eval f) result -1))
result))))
(set 'truth-column01
(lambda(f)(apply string (map (lambda(x)(if x "1" "0"))
(truth-column f)))))
(set 'symexpr (lambda()
(let ((result "["))
(dolist(i (args))
(set 'result (append result (string i) ".")))
(setf (last result) "]")
(sym result))))
(dolist(formula PF)
(dolist(subformula (branches formula)) ; for formulas, branches are subformulas
(set 'canonized-subformula (canon subformula)) ; canon: variables occur in alphabetical order
(set 'canonized-subformula-symbol
(symexpr "propositional-formula" canonized-subformula))
(if (= (eval canonized-subformula-symbol) nil)
; new canonized subformula
(begin (set 'Boolean-function-symbol
(symexpr "Boolean-function" (truth-column01 canonized-subformula)))
(set canonized-subformula-symbol Boolean-function-symbol)
(if (= (eval Boolean-function-symbol) nil)
; new category
(set Boolean-function-symbol (list canonized-subformula))
; old category
(if (< (size canonized-subformula) ;new formula is leader of subcategory
(size (first (eval Boolean-function-symbol))))
; canonized subformula is the best represent of category
(set Boolean-function-symbol (list canonized-subformula))
; canonized subformula isn't the best represent of category
"do nothing")))
;old canonized subformula
"do nothing")))
(set 'counter 1)
(dolist(formula PF)
(when (= formula (canon formula))
(set 'propositional-formula-symbol (symexpr "propositional-formula" formula))
(set 'Boolean-function-symbol (symexpr "Boolean-function" (truth-column01 formula)))
(when (= formula (first (eval Boolean-function-symbol)))
(println counter ". " formula ", " Boolean-function-symbol)
(inc counter))))
(exit)
+------------------+
| Generated 287535 |
| formulas. |
+------------------+
1. true, [Boolean-function.1]
2. nil, [Boolean-function.0]
3. A, [Boolean-function.01]
4. (not A), [Boolean-function.10]
5. (and nil A), [Boolean-function.00]
6. (and A B), [Boolean-function.0001]
7. (or true A), [Boolean-function.11]
8. (or A B), [Boolean-function.0111]
9. (-> A B), [Boolean-function.1101]
10. (<-> A B), [Boolean-function.1001]
11. (not (and A B)), [Boolean-function.1110]
12. (not (or A B)), [Boolean-function.1000]
13. (not (-> A B)), [Boolean-function.0010]
14. (not (<-> A B)), [Boolean-function.0110]
15. (and (not A) B), [Boolean-function.0100]
16. (or A (not B)), [Boolean-function.1011]
17. (and nil (and A B)), [Boolean-function.0000]
18. (and A (and B C)), [Boolean-function.00000001]
19. (and A (or true B)), [Boolean-function.0011]
20. (and A (or B C)), [Boolean-function.00000111]
21. (and A (-> B C)), [Boolean-function.00001101]
22. (and A (<-> B C)), [Boolean-function.00001001]
23. (and (or true A) B), [Boolean-function.0101]
24. (and (or A B) C), [Boolean-function.00010101]
25. (and (-> A B) C), [Boolean-function.01010001]
26. (and (<-> A B) C), [Boolean-function.01000001]
27. (or true (and A B)), [Boolean-function.1111]
28. (or A (and B C)), [Boolean-function.00011111]
29. (or A (or B C)), [Boolean-function.01111111]
30. (or A (-> B C)), [Boolean-function.11011111]
31. (or A (<-> B C)), [Boolean-function.10011111]
32. (or (and A B) C), [Boolean-function.01010111]
33. (or (-> A B) C), [Boolean-function.11110111]
34. (or (<-> A B) C), [Boolean-function.11010111]
35. (-> A (and nil B)), [Boolean-function.1100]
36. (-> A (and B C)), [Boolean-function.11110001]
37. (-> A (-> B C)), [Boolean-function.11111101]
38. (-> A (<-> B C)), [Boolean-function.11111001]
39. (-> (or A B) C), [Boolean-function.11010101]
40. (-> (-> A B) C), [Boolean-function.01011101]
41. (-> (<-> A B) C), [Boolean-function.01111101]
42. (<-> A (and B C)), [Boolean-function.11100001]
43. (<-> A (or B C)), [Boolean-function.10000111]
44. (<-> A (-> B C)), [Boolean-function.00101101]
45. (<-> A (<-> B C)), [Boolean-function.01101001]
46. (<-> (and nil A) B), [Boolean-function.1010]
47. (<-> (and A B) C), [Boolean-function.10101001]
48. (<-> (or A B) C), [Boolean-function.10010101]
49. (<-> (-> A B) C), [Boolean-function.01011001]
50. (not (and A (and B C))), [Boolean-function.11111110]
51. (not (and A (or B C))), [Boolean-function.11111000]
52. (not (and A (-> B C))), [Boolean-function.11110010]
53. (not (and A (<-> B C))), [Boolean-function.11110110]
54. (not (and (or A B) C)), [Boolean-function.11101010]
55. (not (and (-> A B) C)), [Boolean-function.10101110]
56. (not (and (<-> A B) C)), [Boolean-function.10111110]
57. (not (or A (and B C))), [Boolean-function.11100000]
58. (not (or A (or B C))), [Boolean-function.10000000]
59. (not (or A (-> B C))), [Boolean-function.00100000]
60. (not (or A (<-> B C))), [Boolean-function.01100000]
61. (not (or (and A B) C)), [Boolean-function.10101000]
62. (not (or (-> A B) C)), [Boolean-function.00001000]
63. (not (or (<-> A B) C)), [Boolean-function.00101000]
64. (not (-> A (and B C))), [Boolean-function.00001110]
65. (not (-> A (-> B C))), [Boolean-function.00000010]
66. (not (-> A (<-> B C))), [Boolean-function.00000110]
67. (not (-> (or A B) C)), [Boolean-function.00101010]
68. (not (-> (-> A B) C)), [Boolean-function.10100010]
69. (not (-> (<-> A B) C)), [Boolean-function.10000010]
70. (not (<-> A (and B C))), [Boolean-function.00011110]
71. (not (<-> A (or B C))), [Boolean-function.01111000]
72. (not (<-> A (-> B C))), [Boolean-function.11010010]
73. (not (<-> A (<-> B C))), [Boolean-function.10010110]
74. (not (<-> (and A B) C)), [Boolean-function.01010110]
75. (not (<-> (or A B) C)), [Boolean-function.01101010]
76. (not (<-> (-> A B) C)), [Boolean-function.10100110]
77. (and A (and (not B) C)), [Boolean-function.00000100]
78. (and A (or B (not C))), [Boolean-function.00001011]
79. (and (not A) (and B C)), [Boolean-function.00010000]
80. (and (not A) (or B C)), [Boolean-function.01110000]
81. (and (not A) (-> B C)), [Boolean-function.11010000]
82. (and (not A) (<-> B C)), [Boolean-function.10010000]
83. (and (not (and A B)) C), [Boolean-function.01010100]
84. (and (not (or A B)) C), [Boolean-function.01000000]
85. (and (not (<-> A B)) C), [Boolean-function.00010100]
86. (and (or A (not B)) C), [Boolean-function.01000101]
87. (or A (not (and B C))), [Boolean-function.11101111]
88. (or A (not (or B C))), [Boolean-function.10001111]
89. (or A (not (-> B C))), [Boolean-function.00101111]
90. (or A (not (<-> B C))), [Boolean-function.01101111]
91. (or A (and (not B) C)), [Boolean-function.01001111]
92. (or A (or B (not C))), [Boolean-function.10111111]
93. (or (and A B) (not C)), [Boolean-function.10101011]
94. (or (-> A B) (not C)), [Boolean-function.11111011]
95. (or (<-> A B) (not C)), [Boolean-function.11101011]
96. (or (and (not A) B) C), [Boolean-function.01110101]
97. (-> A (and (not B) C)), [Boolean-function.11110100]
98. (<-> A (and (not B) C)), [Boolean-function.10110100]
99. (<-> A (or B (not C))), [Boolean-function.01001011]
100. (<-> (and (not A) B) C), [Boolean-function.10011010]
101. (<-> (or A (not B)) C), [Boolean-function.01100101]
102. (not (and (or A (not B)) C)), [Boolean-function.10111010]
103. (not (or A (and (not B) C))), [Boolean-function.10110000]
104. (not (or (and (not A) B) C)), [Boolean-function.10001010]
105. (and nil (and A (and B C))), [Boolean-function.00000000]
106. (and A (and B (or true C))), [Boolean-function.00000011]
107. (and A (and (or true B) C)), [Boolean-function.00000101]
108. (and A (or true (and B C))), [Boolean-function.00001111]
109. (and A (-> B (and nil C))), [Boolean-function.00001100]
110. (and A (<-> (and nil B) C)), [Boolean-function.00001010]
111. (and (or true A) (and B C)), [Boolean-function.00010001]
112. (and (or true A) (or B C)), [Boolean-function.01110111]
113. (and (or true A) (-> B C)), [Boolean-function.11011101]
114. (and (or true A) (<-> B C)), [Boolean-function.10011001]
115. (and (or A B) (or true C)), [Boolean-function.00111111]
116. (and (or A B) (or B C)), [Boolean-function.00110111]
117. (and (or A B) (-> A C)), [Boolean-function.00110101]
118. (and (or A B) (-> B C)), [Boolean-function.00011101]
119. (and (or A B) (-> C B)), [Boolean-function.00111011]
120. (and (or A B) (<-> A C)), [Boolean-function.00100101]
121. (and (or A B) (<-> B C)), [Boolean-function.00011001]
122. (and (-> A B) (or true C)), [Boolean-function.11110011]
123. (and (-> A B) (or A C)), [Boolean-function.01010011]
124. (and (-> A B) (or B C)), [Boolean-function.01110011]
125. (and (-> A B) (-> B C)), [Boolean-function.11010001]
126. (and (-> A B) (-> C A)), [Boolean-function.10100011]
127. (and (-> A B) (-> C B)), [Boolean-function.10110011]
128. (and (-> A B) (<-> A C)), [Boolean-function.10100001]
129. (and (-> A B) (<-> B C)), [Boolean-function.10010001]
130. (and (<-> A B) (or true C)), [Boolean-function.11000011]
131. (and (<-> A B) (or A C)), [Boolean-function.01000011]
132. (and (<-> A B) (-> A C)), [Boolean-function.11000001]
133. (and (<-> A B) (-> C A)), [Boolean-function.10000011]
134. (and (<-> A B) (<-> A C)), [Boolean-function.10000001]
135. (and (or true (and A B)) C), [Boolean-function.01010101]
136. (and (or A (and B C)) B), [Boolean-function.00010011]
137. (and (or A (or B C)) B), [Boolean-function.00110011]
138. (and (-> A (and nil B)) C), [Boolean-function.01010000]
139. (and (-> A (and B C)) B), [Boolean-function.00110001]
140. (and (<-> A (and B C)) B), [Boolean-function.00100001]
141. (and (<-> (and nil A) B) C), [Boolean-function.01000100]
142. (or true (and A (and B C))), [Boolean-function.11111111]
143. (or A (and (or true B) C)), [Boolean-function.01011111]
144. (or A (-> B (and nil C))), [Boolean-function.11001111]
145. (or A (<-> (and nil B) C)), [Boolean-function.10101111]
146. (or (and A B) (-> C B)), [Boolean-function.10111011]
147. (or (and A B) (<-> A C)), [Boolean-function.10100111]
148. (or (and A B) (<-> B C)), [Boolean-function.10011011]
149. (or (<-> A B) (and A C)), [Boolean-function.11000111]
150. (or (<-> A B) (and B C)), [Boolean-function.11010011]
151. (or (<-> A B) (<-> A C)), [Boolean-function.11100111]
152. (or (<-> A B) (<-> B C)), [Boolean-function.11011011]
153. (or (-> A (and nil B)) C), [Boolean-function.11110101]
154. (or (<-> A (or B C)) B), [Boolean-function.10110111]
155. (or (<-> A (<-> B C)) B), [Boolean-function.01111011]
156. (-> A (and nil (and B C))), [Boolean-function.11110000]
157. (-> A (-> B (and nil C))), [Boolean-function.11111100]
158. (-> A (<-> (and nil B) C)), [Boolean-function.11111010]
159. (-> (or A B) (and nil C)), [Boolean-function.11000000]
160. (-> (or A B) (and A C)), [Boolean-function.11000101]
161. (-> (or A B) (<-> A C)), [Boolean-function.11100101]
162. (-> (or A B) (<-> B C)), [Boolean-function.11011001]
163. (-> (-> A B) (<-> A C)), [Boolean-function.10101101]
164. (-> (-> A B) (<-> B C)), [Boolean-function.10011101]
165. (-> (<-> A B) (and nil C)), [Boolean-function.00111100]
166. (-> (<-> A B) (and A C)), [Boolean-function.00111101]
167. (-> (<-> A B) (<-> A C)), [Boolean-function.10111101]
168. (<-> A (and B (or A C))), [Boolean-function.11100011]
169. (<-> A (and (or true B) C)), [Boolean-function.10100101]
170. (<-> A (and (-> B A) C)), [Boolean-function.10110101]
171. (<-> A (and (<-> A B) C)), [Boolean-function.10110001]
172. (<-> A (or B (<-> A C))), [Boolean-function.01000111]
173. (<-> A (or (<-> A B) C)), [Boolean-function.00100111]
174. (<-> A (-> (-> B A) C)), [Boolean-function.10000101]
175. (<-> A (-> (<-> A B) C)), [Boolean-function.10001101]
176. (<-> A (<-> B (and A C))), [Boolean-function.00111001]
177. (<-> A (<-> B (or A C))), [Boolean-function.01100011]
178. (<-> A (<-> B (-> A C))), [Boolean-function.11001001]
179. (<-> A (<-> B (-> C A))), [Boolean-function.10010011]
180. (<-> A (<-> (and nil B) C)), [Boolean-function.01011010]
181. (<-> (and nil A) (and B C)), [Boolean-function.11101110]
182. (<-> (and nil A) (or B C)), [Boolean-function.10001000]
183. (<-> (and nil A) (-> B C)), [Boolean-function.00100010]
184. (<-> (and nil A) (<-> B C)), [Boolean-function.01100110]
185. (<-> (and A B) (and B C)), [Boolean-function.11101101]
186. (<-> (and A B) (or B C)), [Boolean-function.10001011]
187. (<-> (and nil (and A B)) C), [Boolean-function.10101010]
188. (<-> (and A (and B C)) B), [Boolean-function.11001101]
189. (<-> (and A (or B C)) B), [Boolean-function.11001011]
190. (<-> (or (<-> A B) C) B), [Boolean-function.00011011]
191. (<-> (-> A (and B C)) C), [Boolean-function.01011011]
---
