### Relatively Short Propositional Formulas and Symbols Instead of Pointers and Tables.

 ; 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]

---