summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMasaya Tojo <masaya@tojo.tokyo>2021-07-22 10:49:02 +0900
committerMasaya Tojo <masaya@tojo.tokyo>2021-07-22 10:49:02 +0900
commit086cbd344e702fecf6de144c2313e824a4aa075a (patch)
treea70ae73cfe17052983f4bd0fb9b8fc8fc449d59b
parent658812d37e3be083623a63c9839ac056451df1cd (diff)
リストモナドがモナド則を満すことを示す
-rw-r--r--list-monad.lisp94
1 files changed, 94 insertions, 0 deletions
diff --git a/list-monad.lisp b/list-monad.lisp
new file mode 100644
index 0000000..b30ab62
--- /dev/null
+++ b/list-monad.lisp
@@ -0,0 +1,94 @@
+;;; list-monad.lisp
+;;; ACL2 でリストモナドがモナド則を満していることを示す
+
+;; ACL2 では第一級の関数は使えないため、値としての関数は連想リストで表現する
+;; ACL2 には apply$ という限定的な高階関数を実現する機能があるがよく分かってい
+;; ないので今回は使用しない
+;; https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/ACL2____APPLY_42?path=3463/6113/3222/31/23
+(defun apply-function (f x)
+ (cdr (assoc-equal x f)))
+
+(defun unit (x)
+ (list x))
+
+(defun bind (x f)
+ (cond
+ ((endp x) nil)
+ (t
+ (append (apply-function f (car x))
+ (bind (cdr x) f)))))
+
+;; リストを返す関数かどうかを確認する
+(defun to-list-function-p (x)
+ (if (endp x)
+ t
+ (and (true-listp (cdar x))
+ (to-list-function-p (cdr x)))))
+
+;; モナド則その 1
+(defthm left-identity
+ (implies (to-list-function-p f)
+ (equal (bind (unit x) f)
+ (apply-function f x))))
+
+;; 定義域 x で unit ととして振舞う関数を作成する
+(defun make-unit-function (x)
+ (cond
+ ((endp x) nil)
+ (t (acons (car x)
+ (unit (car x))
+ (make-unit-function (cdr x))))))
+
+;; 定義域 x で unit ととして振舞うことを示す定理
+(defthm theorem-of-make-unit-function
+ (implies (member e x)
+ (equal (apply-function (make-unit-function x) e)
+ (unit e))))
+
+;; モナド則その2
+;; (bind m f) のとき関数 f には m の要素のみが与えられると仮定を置いている
+;; そのため、make-unit-function の unit の定義域には m を
+;; 部分集合とする集合 s を与えている
+;; この仮定は下記の定理が証明できることからきっと正しい
+;; (それでいいのか?)
+(defthm right-identity
+ (implies (and (true-listp m)
+ (subsetp m s))
+ (equal (bind m (make-unit-function s))
+ m)))
+
+;; 定義域 s で
+;; (lambda (x) (bind (apply-function g x) h))
+;; を表現する関数
+(defun make-bind-function (s g h)
+ (if (endp s)
+ nil
+ (acons (car s)
+ (bind (apply-function g (car s)) h)
+ (make-bind-function (cdr s) g h))))
+
+;; append したものを bind するのと
+;; bind したものを append するのは同値である
+(defthm bind-append
+ (implies (to-list-function-p g)
+ (equal (bind (append x y) g)
+ (append (bind x g)
+ (bind y g)))))
+
+;; associativity-of-bind の補助定理
+(defthm associativity-of-bind-lemma
+ (implies (and (true-listp m)
+ (to-list-function-p g)
+ (to-list-function-p h)
+ (member e s))
+ (equal (bind (cdr (assoc-equal e g)) h)
+ (cdr (assoc-equal e (make-bind-function s g h))))))
+
+;; モナド則その3
+(defthm associativity-of-bind
+ (implies (and (true-listp m)
+ (to-list-function-p g)
+ (to-list-function-p h)
+ (subsetp m s))
+ (equal (bind (bind m g) h)
+ (bind m (make-bind-function s g h)))))