Sequence calculus in miniKanren

barfing out tautologies for free!

1 files changed, 112 insertions, 0 deletions

diff --git a/minikanren/sequentcalc.scm b/minikanren/sequentcalc.scm
new file mode 100644
index 0000000..e0099c0
--- /dev/null
+++ b/minikanren/sequentcalc.scm
@@ -0,0 +1,112 @@
+;; Sequence Calculus in miniKanren
+;;
+;; To run this, you will need a copy of
+;;   https://github.com/webyrd/miniKanren-with-symbolic-constraints
+;; (assumed to be in miniKanren from here on)
+;;
+;; To prove or disprove something:
+;;   guile -l miniKanren/mk-guile.scm -e prove -s sequentcalc.scm "'()" "'(or a (not b))"
+;;
+;; To query for valid statements, run the guile repl:
+;;   $ guile -l miniKanren/mk-guile.scm -l sequentcalc.scm
+;;   ;; what should q be to make ⇒ a ∧ ¬ q valid? (up to 10 results)
+;;   scheme@(guile-user)> (run 10 (q) (sequent '() `(or a (not ,q))))
+;;   ;; what could p,q be to make p ⇒ q true? (up to 10 results)
+;;   scheme@(guile-user)> (run 10 (p q) (sequent p q))
+;;
+;; Note that (run*) should usually be avoided, since it will almost
+;; always not terminate (as there are usually an infinite amount
+;; of possible completions).
+
+;; goal: is q a member of the list l?
+(define
+  (membero q l)
+  (fresh (x xs)
+         (== l `(,x . ,xs))
+         (conde
+          ((== q x))
+          ((membero q xs)))))
+
+;; goal: list l only contains q
+(define (onlo q l)
+  (conde ((== l '()))
+         ((fresh (x xs)
+                 (== l `(,x . ,xs))
+                 (== x q)
+                 (onlo q xs)))))
+
+;; goal: rest = l with all instances of q removed
+(define (removo q l rest)
+  (conde
+   ((== rest '()) (onlo q l))
+   ((absento q rest) (== rest l))
+   ((fresh (x xs r rs)
+           (== l `(,x . ,xs))
+           (== rest `(,r . ,rs))
+           (conde
+            ((== q x) (=/= q r) (removo q xs `(,r . ,rs)))
+            ((=/= q x) (== x r) (removo q xs rs)))))))
+
+(define (sequent gamma delta)
+  (conde
+   ;; the base axiom: a,Γ ⇒ a,Δ
+   ((fresh (a) (membero a gamma) (membero a delta)))
+   ;; the not axiom: ⊥,Γ ⇒ Δ
+   ((membero 'bottom gamma))
+   ;; the not left rule
+   ((fresh (f)
+           ;; there is ¬F on the left side
+           (membero `(not ,f) gamma)
+           ;; prove that Γ ⇒ F,Δ
+           (fresh (g) (removo `(not ,f) gamma g) (sequent g `(,f . ,delta)))))
+   ;; the not right rule
+   ((fresh (f)
+           (membero `(not ,f) delta)
+           (fresh (d) (removo `(not ,f) delta d) (sequent `(,f . ,gamma) d))))
+   ;; the and left rule
+   ((fresh (a b)
+           (membero `(and ,a ,b) gamma)
+           (fresh (g)
+                  (removo `(and ,a ,b) gamma g)
+                  (sequent `(,a . (,b . ,g)) delta))))
+   ;; the and right rule
+   ((fresh (a b)
+           (membero `(and ,a ,b) delta)
+           (fresh (d)
+                  (removo `(and ,a ,b) delta d)
+                  (sequent gamma `(,a . ,d))
+                  (sequent gamma `(,b . ,d)))))
+   ;; the left or rule
+   ((fresh (a b)
+           (membero `(or ,a ,b) gamma)
+           (fresh (g)
+                  (removo `(or ,a ,b) gamma g)
+                  (sequent `(,a . ,g) delta)
+                  (sequent `(,b . ,g) delta))))
+   ;; the right or rule
+   ((fresh (a b)
+           (membero `(or ,a ,b) delta)
+           (fresh (d)
+                  (removo `(or ,a ,b) delta d)
+                  (sequent gamma `(,a . (,b . ,d))))))
+   ;; the left arrow rule
+   ((fresh (a b)
+           (membero `(arrow ,a ,b) gamma)
+           (fresh (g)
+                  (removo `(arrow ,a ,b) gamma g)
+                  (sequent g `(,a . ,delta))
+                  (sequent `(,b . ,g) delta))))
+   ;; the right arrow rule
+   ((fresh (a b)
+           (membero `(arrow ,a ,b) delta)
+           (fresh (d)
+                  (removo `(arrow ,a ,b) delta d)
+                  (sequent `(a . ,gamma) `(,b . ,d)))))))
+
+(define (prove args)
+  (let ((gamma (eval-string (car (cdr args))))
+        (delta (eval-string (car (cdr (cdr args))))))
+    (if (equal? '() (run 1 (q) (sequent gamma delta)))
+        (display "does not follow from sequent calculus")
+        (display "follows from sequent calculus"))
+    (newline)))