Skip to content

Instantly share code, notes, and snippets.

@kencoba
Forked from anonymous/prover.clj
Created February 19, 2011 04:49
Show Gist options
  • Star 2 You must be signed in to star a gist
  • Fork 1 You must be signed in to fork a gist
  • Save kencoba/834831 to your computer and use it in GitHub Desktop.
Save kencoba/834831 to your computer and use it in GitHub Desktop.
(ns
^{:doc
"Simple Theorem Prover 'Programming Language Theory and its Implementation' Michael J.C. Gordon"
:author "Kenichi Kobayashi"}
prover
(:use [clojure.test])
(:require [clojure.walk :as cw]))
(def constant #{'+ '- '< '<= '> '>= '* '= 'T 'F 'DIV 'not 'and 'or 'implies})
(defmacro third [x] `(first (rest (rest ~x))))
(defmacro variable? [x] `(not (or (nil? ~x) (number? ~x) (contains? constant ~x))))
(defn elem? [exp] (or (not (coll? exp)) (= exp '())))
(defn ^{:arglists '([pattern expression map-of-substitutions])}
matchfn [pat exp sub]
(if (elem? pat)
(if (and (not= pat '()) (variable? pat))
(if (contains? sub pat)
(if (= (sub pat) exp)
sub
(throw (Exception.)))
(assoc-in sub (list pat) exp))
(if (= pat exp) sub (throw (Exception.))))
(let [[p & px] pat
[e & ex] exp
s (matchfn p e sub)]
(recur px ex s))))
(defn match [pat exp]
(try (matchfn pat exp nil) (catch Exception e 'fail)) )
(def ^{:doc "trueの時にはrewrite1は等式の変換結果を表示する"}
*rewrite-flag* true)
(defn ^{:doc "等式の左辺と式を比較して同一の項の対応を取得し、変換した右辺を返す"
:arglists '([equation expression])}
rewrite1 [eqn exp]
(let [l (first eqn)
r (third eqn)]
(let [sub (match l exp)]
(if (= sub 'fail)
exp
(do
(if *rewrite-flag*
(println (cw/prewalk-replace sub eqn)))
(cw/prewalk-replace sub r))))))
(defn ^{:doc "複数の等式を受取り、変換した式を返す"}
rewrite [eqns exp]
(reduce #(rewrite1 %2 %1) exp eqns))
(defmacro
^{:doc "test if expression is the form of implies" }
imp? [exp]
`(and (coll? ~exp)
(= (count ~exp) 3)
(= (second ~exp) ~''implies)))
(defmacro mk-imp [p q]
`(list ~p ~''implies ~q))
(defmacro antecedant [exp] `(first ~exp))
(defmacro consequent [exp] `(third ~exp))
(defn ^{:doc "recursively substitute expression with implies rule" }
imp-subst-simp [exp]
(if (imp? exp)
(let [a (antecedant exp)
c (consequent exp)]
(mk-imp a (cw/prewalk-replace {a 'T} c)))
exp))
(defmacro
^{:doc "test if expression is the form of equation" }
eqn? [exp]
`(and (coll? ~exp)
(= (count ~exp) 3)
(= (second ~exp) ~''=)))
(defn imp-and-simp [exp]
(if (and (imp? exp) (eqn? (antecedant exp)))
(let [a (antecedant exp)
c (consequent exp)]
(mk-imp a (cw/prewalk-replace {(first a) (third a)} c)))
exp))
(defn imp-simp [exp]
(imp-and-simp (imp-subst-simp exp)))
(deftest test-variable?
(is (= false (variable? 1)))
(is (= false (variable? 'and)))
(is (= false (variable? nil)))
(is (= true (variable? 'x))))
(deftest test-matchfn
(is (= '{z 3, x 1} (matchfn '(x 2 z) '(1 2 3) nil)))
(is (= '{z 3, x 1} (matchfn '(x 2 z) '(1 2 3) '{x 1})))
(is (= '{y 1, x 3, z 3} (matchfn '((x + y) * (z * y)) '((3 + 1) * (3 * 1)) '{z 3})))
(is (= '{y 1, x x, z x} (matchfn '((x + y) * (z * y)) '((x + 1) * (x * 1)) '{z x})))
(is (thrown? Exception (matchfn '(x * y) '(1 + 2) nil))))
(deftest test-match
(is (= '{y 2, x 1} (match '(x + y) '(1 + 2))))
(is (= 'fail (match '(x + x) '(1 + 2))))
(is (= 'fail (match '(x * y) '(1 + 2)))))
(deftest test-rewrite1
(is (= '(1 * 2) (rewrite1 '((x + 0) = x) '((1 * 2) + 0))))
(is (= '((1 * 2) * 0) (rewrite1 '((x + 0) = x) '((1 * 2) * 0)))))
(deftest test-rewrite
(is (= 'X (rewrite '(((x + 0) = x) ((x * 1) = x)) '((X * 1) + 0)))))
(deftest test-mk-imp
(is (= '(x implies y) (mk-imp 'x 'y))))
(deftest test-antecedant
(is (= 'x (antecedant '(x implies y)))))
(deftest test-consequent
(is (= 'y (consequent '(x implies y)))))
(deftest test-imp?
(is (= false (imp? nil)))
(is (= false (imp? '())))
(is (= false (imp? '(x imp y))))
(is (= true (imp? '(x implies y))))
(is (= false (imp? '(x implies)))))
(deftest test-imp-subst-simp
(is (= '(P implies T) (imp-subst-simp (mk-imp 'P 'P))))
(is (= '(P implies (T and Q)) (imp-subst-simp (mk-imp 'P '(P and Q))))))
(defn repeat-apply [f exp]
(let [exp1 (f exp)]
(if (= exp exp1)
exp
(recur f exp1))))
(defn depth-imp-simp [exp]
(cw/postwalk
(fn [x] (imp-simp x))
exp))
(defn top-depth-rewrite [eqns exp]
(cw/prewalk
(fn [x] (rewrite eqns x))
exp))
(defn depth-rewrite [eqns exp]
(cw/postwalk
(fn [x] (rewrite eqns x))
exp))
(defn prove [eqns exp]
(repeat-apply
(fn [x] (top-depth-rewrite eqns (depth-imp-simp x)))
exp))
(def logic
'(
((T implies X) = X)
((F implies X) = T)
((X implies T) = T)
((X implies X) = T)
((T and X) = X)
((X and T) = X)
((F and X) = F)
((X and F) = F)
((X = X) = T)
(((X and Y) implies Z) = (X implies (Y implies Z)))))
(def arithmetic
'(
((X + 0) = X)
((0 + X) = X)
((X * 0) = 0)
((0 * X) = 0)
((X * 1) = X)
((1 * X) = X)
((not (X <= Y)) = (Y < X))
((not (X >= Y)) = (Y > X))
((not (X < Y)) = (X >= Y))
(((- X) >= (- Y)) = (X <= Y))
(((- X) >= Y) = (X <= (- Y)))
((- 0) = 0)
(((X < Y) implies (X <= Y)) = T)
((X - X) = 0)
(((X + Y) - Z) = (X + (Y - Z)))
(((X - Y) * Z) = ((X * Z) - (Y * Z)))
((X * (Y + Z)) = ((X * Y) + (X * Z)))
(((X + Y) * Z) = ((X * Z) + (Y * Z)))
(((X >= Y) implies ((X < Y) implies Z)) = T)
(((X <= Y) implies ((Y < X) implies Z)) = T)
((0 DIV X) = 0)
(((X DIV Y) + Z) = ((X + (Y * Z)) DIV Y))
(((X - Y) + Z) = (X + (Z - Y)))
((2 * X) = (X + X))
))
(def facts (concat logic arithmetic))
(deftest test-depth-imp-simp
(is (= '((x = 1) implies ((y = 1) implies (1 = z)))
(depth-imp-simp '((x = 1) implies ((y = x) implies (y = z)))))))
(deftest test-top-depth-rewrite
(is (= '(1 < 2)
(top-depth-rewrite
'(((not (x >= y)) = (x < y)) ((x >= y) = ((x = y) or (x > y))))
'(not (1 >= 2))))))
(deftest test-prove
(is (= 'T
(prove facts
'(((x = (((n - 1) * n) DIV 2)) and ((1 <= n) and (n <= m)))
implies
((x + n) = ((((n + 1) - 1) * (n + 1)) DIV 2)))))))
(defn treezip [c1 c2]
(if (not (coll? c1))
(list c1 c2)
(map treezip c1 c2)))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment