bs9o

task4

May 13th, 2022 (edited)
629
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. (ns task4.core)
  2.  
  3. ;порождение константы
  4. (defn constant [num]
  5.   {:pre [(or (= num 1) (= num 0))]}
  6.   (list ::const num))
  7.  
  8. ;проверка типа для константы
  9. (defn constant? [c]
  10.   (= (first c) ::const))
  11.  
  12. ;взятие значения константы
  13. (defn constant-value [c]
  14.   (second c))
  15.  
  16. ;порождение переменной
  17. (defn variable [name]
  18.   {:pre [(keyword? name)]}
  19.   (list ::var name))
  20.  
  21. ;проверка типа для переменной
  22. (defn variable? [v]
  23.   (= (first v) ::var))
  24.  
  25. ;взятие имени переменной
  26. (defn variable-name [v]
  27.   (second v))
  28.  
  29. ;проверка двух переменных на равенство
  30. (defn same-variables? [v1 v2]
  31.   (and
  32.     (variable? v1)
  33.     (variable? v2)
  34.     (= (variable-name v1)
  35.        (variable-name v2))))
  36.  
  37. ;порождение конъюкции
  38. (defn && [expr & rest]
  39.   (if (empty? rest)
  40.     expr
  41.     (cons ::conj (cons expr rest))))
  42.  
  43. ;проверка типа для конъюкции
  44. (defn &&? [expr]
  45.   (= ::conj (first expr)))
  46.  
  47. ;порождение дизъюнкции
  48. (defn || [expr & rest]
  49.   (if (empty? rest)
  50.     expr
  51.     (cons ::disj (cons expr rest))))
  52.  
  53. ;проверка типа для дизъюнкции
  54. (defn ||? [expr]
  55.   (= ::disj (first expr)))
  56.  
  57. ;порождение импликации
  58. (defn -> [expr & rest]
  59.   (if (empty? rest)
  60.     expr
  61.     (cons ::impl (cons expr rest))))
  62.  
  63. ;проверка типа для импликации
  64. (defn ->? [expr]
  65.   (= ::impl (first expr)))
  66.  
  67. ;порождение отрицания
  68. (defn neg [expr]
  69.   (if (= ::neg (first expr))
  70.     (rest expr)
  71.     (cons ::neg expr)))
  72.  
  73. ;проверка типа для отрицания выражения
  74. (defn neg? [expr]
  75.   (= ::neg (first expr)))
  76.  
  77. ;взятие аргументов выражения
  78. (defn args [expr]
  79.   (rest expr))
  80.  
  81. ;проверка типа для отрицания переменной
  82. (defn neg-variable? [expr]
  83.   (and (= ::neg (first expr)) (variable? (args expr))))
  84.  
  85. ;подстановка значения вместо переменной
  86. (defn sub-val [expr v val]
  87.   {:pre [(and (variable? v) (or (= val 0) (= val 1)))]}
  88.   (let [sub-rules (list
  89.                     [(fn [expr] (same-variables? expr v))
  90.                      (fn [_] (constant val))]
  91.                     [(fn [expr] (not (or (constant? expr) (variable? expr))))
  92.                      (fn [expr] (cons (first expr) (map (fn [x] (sub-val x v val)) (args expr))))]
  93.                     [(fn [_] true) (fn [expr] expr)])]
  94.     ((some (fn [rule]
  95.              (if ((first rule) expr)
  96.                (second rule)
  97.                false))
  98.            sub-rules)
  99.      expr)))
  100.  
  101. ;элиминация импликации
  102. (defn impl-elim [expr]
  103.   (let [elim-rules (list
  104.                      [->? (fn [expr] (||
  105.                                        (neg (impl-elim (first (args expr))))
  106.                                        (impl-elim (second (args expr)))))]
  107.                      [neg? (fn [expr] (neg (impl-elim (args expr))))]
  108.                      [(fn [expr] (not (or (constant? expr) (variable? expr) (neg-variable? expr))))
  109.                       (fn [expr] (cons (first expr) (map impl-elim (args expr))))]
  110.                      [(fn [_] true) (fn [expr] expr)])]
  111.     ((some (fn [rule]
  112.              (if ((first rule) expr)
  113.                (second rule)
  114.                false))
  115.            elim-rules)
  116.      expr)))
  117.  
  118. ;применение законов де Моргана для раскрытия отрицаний
  119. (defn de-morgans-laws [expr]
  120.   (let [de-morgans-rules (list
  121.                            [(fn [expr] (and (neg? expr) (not (variable? (args expr)))))
  122.                             (fn [expr] (cond
  123.                                          (||? (args expr))
  124.                                          (&& (de-morgans-laws (neg (first (args (args expr)))))
  125.                                              (de-morgans-laws (neg (second (args (args expr))))))
  126.                                          (&&? (args expr))
  127.                                          (|| (de-morgans-laws (neg (first (args (args expr)))))
  128.                                              (de-morgans-laws (neg (second (args (args expr))))))
  129.                                          true (neg (de-morgans-laws (args expr)))))]
  130.                            [(fn [expr] (not (or (constant? expr)
  131.                                                 (variable? expr)
  132.                                                 (variable? (args expr)))))
  133.                             (fn [expr] (cons (first expr) (map de-morgans-laws (args expr))))]
  134.                            [(fn [_] true) (fn [expr] expr)])]
  135.     ((some (fn [rule]
  136.              (if ((first rule) expr)
  137.                (second rule)
  138.                false))
  139.            de-morgans-rules)
  140.      expr)))
  141.  
  142. ;вспомогательная функция:
  143. ;проверка наличия дизъюнкции в выражении
  144. (defn no-disj [expr]
  145.   (cond
  146.     (or (variable? expr) (neg-variable? expr)) true
  147.     (||? expr) false
  148.     true (every? no-disj (args expr))))
  149.  
  150. ;применение свойства дистрибутивности
  151. (defn distributive-pr [expr]
  152.   (let [distr-rules (list
  153.                       [&&? (fn [expr] (cond
  154.                                         (||? (first (args expr)))
  155.                                         (distributive-pr (||
  156.                                                            (distributive-pr
  157.                                                              (&&
  158.                                                                (first (args (first (args expr))))
  159.                                                                (second (args expr))))
  160.                                                            (distributive-pr
  161.                                                              (&&
  162.                                                                (second (args (first (args expr))))
  163.                                                                (second (args expr))))))
  164.                                         (||? (second (args expr)))
  165.                                         (distributive-pr (||
  166.                                                            (distributive-pr
  167.                                                              (&&
  168.                                                                (first (args expr))
  169.                                                                (first (args (second (args expr))))))
  170.                                                            (distributive-pr
  171.                                                              (&&
  172.                                                                (first (args expr))
  173.                                                                (second (args (second (args expr))))))))
  174.                                         true (if (no-disj expr)
  175.                                                expr
  176.                                                (distributive-pr
  177.                                                  (cons (first expr)
  178.                                                        (map distributive-pr (args expr)))))))]
  179.                       [(fn [expr] (not (or (constant? expr) (variable? expr) (neg-variable? expr))))
  180.                        (fn [expr] (cons (first expr) (map distributive-pr (args expr))))]
  181.                       [(fn [_] true) (fn [expr] expr)])]
  182.     ((some (fn [rule]
  183.              (if ((first rule) expr)
  184.                (second rule)
  185.                false))
  186.            distr-rules)
  187.      expr)))
  188.  
  189. ;вспомогательная функция:
  190. ;раскрытие скобок по свойству ассоциативности для связки conn1 и применение к аргументам связки conn2
  191. (defn associativity-pr1 [args conn1 conn2]
  192.   (apply conn2 (reverse (reduce
  193.                           (fn [acc arg] (if (conn1 arg)
  194.                                           (concat acc (rest arg)) (conj acc arg)))
  195.                           '()
  196.                           args))))
  197.  
  198. ;применение свойства ассоциативности
  199. (defn associativity-pr [expr]
  200.   (let [assoc-rules (list
  201.                       [||? (fn [expr] (apply || (args (associativity-pr1
  202.                                                         (map associativity-pr (args expr))
  203.                                                         ||?
  204.                                                         ||))))]
  205.                       [&&? (fn [expr] (apply && (args (associativity-pr1
  206.                                                         (map associativity-pr (args expr))
  207.                                                         &&?
  208.                                                         &&))))]
  209.                       [(fn [expr] (not (or (constant? expr) (variable? expr) (neg-variable? expr))))
  210.                        (fn [expr] (cons (first expr) (map associativity-pr (args expr))))]
  211.                       [(fn [_] true) (fn [expr] expr)])]
  212.     ((some (fn [rule]
  213.              (if ((first rule) expr)
  214.                (second rule)
  215.                false))
  216.            assoc-rules)
  217.      expr)))
  218.  
  219. ;применение свойства идемпотентности
  220. (defn idempotence-pr [expr]
  221.   (let [idemp-rules (list
  222.                       [||? (fn [expr] (apply || (map idempotence-pr (distinct (args expr)))))]
  223.                       [&&? (fn [expr] (apply && (map idempotence-pr (distinct (args expr)))))]
  224.                       [(fn [expr] (not (or (constant? expr) (variable? expr) (neg-variable? expr))))
  225.                        (fn [expr] (cons (first expr) (map idempotence-pr (args expr))))]
  226.                       [(fn [_] true) (fn [expr] expr)])]
  227.     ((some (fn [rule]
  228.              (if ((first rule) expr)
  229.                (second rule)
  230.                false))
  231.            idemp-rules)
  232.      expr)))
  233.  
  234. ;вспомогательная функция:
  235. ;провека того, что одно выражение есть отрицание второго
  236. (defn neg-exprs? [expr]
  237.   (if (or (variable? expr) (neg-variable? expr))
  238.     false
  239.     (some (fn [x] (some (fn [y] (or (= y (neg x)) (= x (neg y)))) expr)) expr)))
  240.  
  241. ;замена тождественно истинных подформул на константу 1, а тождественно ложных на константу 0
  242. (defn taut-contr-elim [expr]
  243.   (let [taut-contr-elim-rules (list
  244.                                 [||? (fn [expr] (if (neg-exprs? (args expr))
  245.                                                   (constant 1)
  246.                                                   (apply || (map taut-contr-elim (args expr)))))]
  247.                                 [&&? (fn [expr] (if (neg-exprs? (args expr))
  248.                                                   (constant 0)
  249.                                                   (apply && (map taut-contr-elim (args expr)))))]
  250.                                 [(fn [expr] (not (or (constant? expr) (variable? expr) (neg-variable? expr))))
  251.                                  (fn [expr] (cons (first expr) (map taut-contr-elim (args expr))))]
  252.                                 [(fn [_] true) (fn [expr] expr)])]
  253.     ((some (fn [rule]
  254.              (if ((first rule) expr)
  255.                (second rule)
  256.                false))
  257.            taut-contr-elim-rules)
  258.      expr)))
  259.  
  260. ;приведение к ДНФ
  261. (defn transform-to-dnf [expr]
  262.   (taut-contr-elim
  263.     (idempotence-pr
  264.     (associativity-pr
  265.       (distributive-pr
  266.         (de-morgans-laws
  267.           (impl-elim expr)))))))
  268.  
  269. --------------------------------
  270.  
  271. (variable :x) == x
  272. (&& (variable :x3) (variable :x2) (variable :x1)) == x_3 & x_2 & x_1
  273. (&& (neg (variable :x3)) (variable :x4)) == (not x_3) v x_4
  274. (&& (variable :x1) (|| (variable :x3) (variable :x4) (variable :x6) (variable :x5)) (variable :x2)) == x_1 & (x_3 v x_4 v x_6 v x_5 v x_2)
  275.  
  276. ;таким образом генерируешь формулы ИВ и потом их подставляешь в функции (вместо аргумента expr)
  277.  
RAW Paste Data Copied