-
Notifications
You must be signed in to change notification settings - Fork 0
/
logic.clj
119 lines (98 loc) · 3.65 KB
/
logic.clj
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
(ns tardis.logic
(:refer-clojure :exclude [==])
(:use [clojure.core.logic]))
(defne undo-double-negationo [pre post]
([['not ['not post]]
post]))
(defne pass-neg-through-exo [pre post]
([['not ['exists ['lambda [var] body]]]
['forall ['lambda [var] ['not body]]]]))
(defne make-implicationo [pre post]
([['not [['and A] ['not B]]]
[['impl A] B]])
([['not [['and A] [['and B] C]]]
post]
(make-implicationo ['not [['and [['and A] B]] C]] post)))
(defn use-forallo [pre post]
(fresh [step var body body']
(pass-neg-through-exo pre step)
(== step ['forall ['lambda [var] body]])
(== post ['forall ['lambda [var] body']])
(conde [(make-implicationo body body')]
[(undo-double-negationo body body')]
[(use-forallo body body')])))
(defne introduce-binderso [pre post]
([[quantifier ['lambda [var] body]]
[quantifier [var] body]]
(membero quantifier ['exists 'forall])))
(defne uncurryo [pre post]
([[[F X] Y . Z] [F X Y . Z]]))
(defn -all [step-rel]
(letfn [(step-rel-all [pre post]
(conde [(step-rel pre post)]
[(step-rel-list pre post)]))
(step-rel-list [pre post]
(fresh [pre-head pre-tail post-head post-tail]
(== pre (lcons pre-head pre-tail))
(== post (lcons post-head post-tail))
(conde [(step-rel-all pre-head post-head)
(== pre-tail post-tail)]
[(step-rel-list pre-tail post-tail)
(== pre-head post-head)])))]
step-rel-all))
(defn fix [f]
(fn fix-f [x]
(let [fx (f x)]
(if (= x fx)
x
(fix-f fx)))))
(defn -* [step-rel]
(letfn [(step-fn [in]
(or (first (run 1 [out] (step-rel in out)))
in))]
(fix step-fn)))
(def clean
(comp (-> uncurryo -all -*)
(-> introduce-binderso -all -*)
(-> use-forallo -all -*)
(-> undo-double-negationo -all -*)))
(def render-hiero (-> (make-hierarchy)
(derive 'and :binary-op)
(derive 'or :binary-op)
(derive 'impl :binary-op)
(derive '= :binary-op)
(derive 'part-of :binary-op)
(derive 'not :unary-op)
(derive 'lambda :binder)
(derive 'exists :binder)
(derive 'forall :binder)))
(def symbol-table {'and "∧"
'or "∨"
'impl "→"
'= "="
'part-of "⊆"
'not "¬"
'lambda "λ"
'exists "∃"
'forall "∀"})
(defmulti render
(fn [form]
(if (coll? form)
(first form)
:terminal))
:hierarchy #'render-hiero)
(defmethod render :terminal [v]
(str v))
(defmethod render :binary-op [[op x y]]
(str "(" (render x) " " (symbol-table op) " " (render y) ")"))
(defmethod render :unary-op [[op x]]
(str "(" (symbol-table op) (render x) ")"))
(defmethod render :binder [[binder [var] body]]
(str (symbol-table binder) (render var) "." "(" (render body) ")"))
(defmethod render :default [[pred & args]]
(str (render pred) "(" (apply str (interpose "," (map render args))) ")"))
(def ^:sonic-screwdriver simplify-sexp-formula
"Simplifies an s-expression-encoded logical formula by removing double
negations, introducing restricted universal quantification (∀x. Px → Qx),
treating quantifiers as binders and uncurrying applications."
(comp render clean read-string))