From c3b18da12dd6f6510f960edb66669733ccdeb694 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Thu, 22 Jul 2021 10:49:02 +0900
Subject: リストモナドがモナド則を満たすことを示す
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 list-monad.lisp | 102 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 102 insertions(+)
 create mode 100644 list-monad.lisp

(limited to 'list-monad.lisp')

diff --git a/list-monad.lisp b/list-monad.lisp
new file mode 100644
index 0000000..f7a6425
--- /dev/null
+++ b/list-monad.lisp
@@ -0,0 +1,102 @@
+;;; 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
+(defmacro apply-function (f x)
+  `(cdr (assoc-equal ,x ,f)))
+
+;;; リストモナドの定義
+(defmacro 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)))))
+
+;; 定義域 s で unit ととして振舞う関数を作成する
+(defun make-unit-function (s)
+  (cond
+    ((endp s) nil)
+    (t (acons (car s)
+              (unit (car s))
+              (make-unit-function (cdr s))))))
+
+;; make-unit-function が定義域 s で
+;; unit ととして振舞うことを示す定理
+(defthm theorem-of-make-unit-function
+  (implies (member e s)
+           (equal (apply-function (make-unit-function s) e)
+                  (unit e))))
+
+;; 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)))))
+
+;; 定義域 s で
+;; (lambda (x) (bind (apply-function g x) h))
+;; を表現する関数
+(defun make-apply-and-bind-function (s g h)
+  (if (endp s)
+      nil
+      (acons (car s)
+             (bind (apply-function g (car s)) h)
+             (make-apply-and-bind-function (cdr s) g h))))
+
+;; 定義域 s で
+;; (lambda (x) (bind (apply-function g x) h))
+;; ととして振舞うことを示す定理
+(defthm theorem-of-make-apply-and-bind-function
+  (implies (and (member x s)
+                (to-list-function-p g)
+                (to-list-function-p h))
+           (equal (apply-function (make-apply-and-bind-function s g h) x)
+                  (bind (apply-function g x) h))))
+
+;; associativity-of-bind の補助定理
+(defthm associativity-of-bind-lemma
+  (implies (and (to-list-function-p g)
+                (to-list-function-p h)
+                (member e s))
+           (equal (cdr (assoc-equal e (make-apply-and-bind-function s g h)))
+                  (bind (cdr (assoc-equal e g)) h))))
+
+;;; モナド則
+;;  unit x >>= f ≡ f x
+(defthm left-identity
+  (implies (to-list-function-p f)
+           (equal (bind (unit x) f)
+                  (apply-function f x))))
+
+;;  m >>= unit ≡ m
+(defthm right-identity
+  (implies (and (true-listp m)
+                (subsetp m s))
+           (equal (bind m (make-unit-function s))
+                  m)))
+
+;; m >>= (\x -> g x >>= h) ≡ (m >>= g) >>= h
+(defthm associativity-of-bind
+  (implies (and (true-listp m)
+                (to-list-function-p g)
+                (to-list-function-p h)
+                (subsetp m s))
+           (equal (bind m (make-apply-and-bind-function s g h))
+                  (bind (bind m g) h))))
-- 
cgit v1.2.3