summaryrefslogtreecommitdiff
path: root/minikanren
diff options
context:
space:
mode:
Diffstat (limited to 'minikanren')
-rw-r--r--minikanren/sequentcalc.scm112
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)))