blob: f7a64250cc4ab2304eed4555bc8bf26c3be2be34 (
about) (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
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))))
|
