diff options
Diffstat (limited to 'minikanren')
| -rw-r--r-- | minikanren/sequentcalc.scm | 112 |
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))) |