Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
(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
You can’t perform that action at this time.