Mercurial > hg > Papers > 2023 > soto-master
changeset 19:76055a4c1dd2
Fix
| author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 03 Feb 2023 03:06:18 +0900 |
| parents | 1b000d9505f5 |
| children | bc0d518ed166 |
| files | DPP/ModelChecking.agda Paper/master_paper.out Paper/master_paper.pdf Paper/src/agda-term3.agda Paper/tex/agda.tex Paper/tex/cbc.tex Paper/tex/cbc_agda.tex Paper/tex/hoare.tex Paper/tex/intro.tex |
| diffstat | 9 files changed, 201 insertions(+), 150 deletions(-) [+] |
line wrap: on
line diff
--- a/DPP/ModelChecking.agda Thu Feb 02 21:20:08 2023 +0900 +++ b/DPP/ModelChecking.agda Fri Feb 03 03:06:18 2023 +0900 @@ -809,8 +809,7 @@ test-dead-lock-loop2 metaenv2 = branch-search-meta2 metaenv2 (λ me2 → step-meta2 me2 (λ me3 → testhoge me3 metaenv2 (λ me4 → test-dead-lock-loop me4) ) ) (λ e → check-and-judge-deadlock e (λ e1 → e1) ) test-step-c2 : List (List Env) -test-step-c2 = init-brute-force (record { - table = 0 ∷ 0 ∷ 0 ∷ [] +test-step-c2 = init-brute-force (record {table = 0 ∷ 0 ∷ 0 ∷ [] ; ph = record { pid = 1 ; left-hand = false
--- a/Paper/master_paper.out Thu Feb 02 21:20:08 2023 +0900 +++ b/Paper/master_paper.out Fri Feb 03 03:06:18 2023 +0900 @@ -7,32 +7,40 @@ \BOOKMARK [1][]{section.2.3}{\376\377\0002\000.\0003\000\040\000M\000e\000t\000a\000\040\000C\000o\000d\000e\000G\000e\000a\000r\000\040\000/\000\040\000M\000e\000t\000a\000\040\000D\000a\000t\000a\000G\000e\000a\000r}{chapter.2}% 6 \BOOKMARK [0][]{chapter.3}{\376\377\173\054\0003\172\340\000\040\133\232\164\006\212\074\146\016\145\057\143\364\174\373\212\000\212\236\000\040\000A\000g\000d\000a}{}% 7 \BOOKMARK [1][]{section.3.1}{\376\377\0003\000.\0001\000\040\000A\000g\000d\000a\060\156\127\372\147\054}{chapter.3}% 8 -\BOOKMARK [1][]{section.3.2}{\376\377\0003\000.\0002\000\040\000A\000g\000d\000a\060\153\060\210\060\213\133\232\164\006\212\074\146\016}{chapter.3}% 9 -\BOOKMARK [0][]{chapter.4}{\376\377\173\054\0004\172\340\000\040\000G\000e\000a\000r\000s\000A\000g\000d\000a\000\040\137\142\137\017\060\147\146\370\060\117\000\040\000A\000g\000d\000a}{}% 10 -\BOOKMARK [1][]{section.4.1}{\376\377\0004\000.\0001\000\040\000A\000g\000d\000a\000\040\060\153\060\210\060\213\000\040\000M\000e\000t\000a\000\040\000G\000e\000a\000r\000s}{chapter.4}% 11 -\BOOKMARK [0][]{chapter.5}{\376\377\173\054\0005\172\340\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\153\060\210\060\213\133\232\164\006\212\074\146\016}{}% 12 -\BOOKMARK [1][]{section.5.1}{\376\377\0005\000.\0001\000\040\000H\000o\000a\000r\000e\000\040\000L\000o\000g\000i\000c}{chapter.5}% 13 -\BOOKMARK [1][]{section.5.2}{\376\377\0005\000.\0002\000\040\000I\000n\000v\000a\000r\000i\000a\000n\000t\000\040\060\222\165\050\060\104\060\137\000\040\000H\000o\000a\000r\000e\000\040\000L\000o\000g\000i\000c\000\040\060\153\060\210\060\213\151\034\212\074\060\156\145\271\154\325\000\040}{chapter.5}% 14 -\BOOKMARK [1][]{section.5.3}{\376\377\0005\000.\0003\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\153\060\146\000\040\000H\000o\000a\000r\000e\000\040\000L\000o\000g\000i\000c\000\040\060\222\165\050\060\104\060\137\151\034\212\074\060\156\117\213}{chapter.5}% 15 -\BOOKMARK [2][]{subsection.5.3.1}{\376\377\0005\000.\0003\000.\0001\000\040\000W\000h\000i\000l\000e\000\040\000L\000o\000o\000p\000\040\060\156\133\237\210\305}{section.5.3}% 16 -\BOOKMARK [2][]{subsection.5.3.2}{\376\377\0005\000.\0003\000.\0002\000\040\000W\000h\000i\000l\000e\000\040\000L\000o\000o\000p\000\040\060\156\151\034\212\074}{section.5.3}% 17 -\BOOKMARK [1][]{section.5.4}{\376\377\0005\000.\0004\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\153\060\112\060\121\060\213\000\040\000B\000i\000n\000a\000r\000y\000\040\000T\000r\000e\000e\000\040\060\156\151\034\212\074}{chapter.5}% 18 -\BOOKMARK [2][]{subsection.5.4.1}{\376\377\0005\000.\0004\000.\0001\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\153\060\112\060\121\060\213\147\050\151\313\220\040\060\156\212\055\212\010}{section.5.4}% 19 -\BOOKMARK [2][]{subsection.5.4.2}{\376\377\0005\000.\0004\000.\0002\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\153\060\112\060\121\060\213\000\040\000B\000i\000n\000a\000r\000y\000\040\000T\000r\000e\000e\000\040\060\156\133\237\210\305}{section.5.4}% 20 -\BOOKMARK [2][]{subsection.5.4.3}{\376\377\0005\000.\0004\000.\0003\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\153\060\112\060\121\060\213\000\040\000B\000i\000n\000a\000r\000y\000\040\000T\000r\000e\000e\000\040\060\156\151\034\212\074}{section.5.4}% 21 -\BOOKMARK [0][]{chapter.6}{\376\377\173\054\0006\172\340\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\153\060\210\060\213\060\342\060\307\060\353\151\034\147\373}{}% 22 -\BOOKMARK [1][]{section.6.1}{\376\377\0006\000.\0001\000\040\060\342\060\307\060\353\151\034\147\373\060\150\060\157}{chapter.6}% 23 -\BOOKMARK [1][]{section.6.2}{\376\377\0006\000.\0002\000\040\000D\000i\000n\000i\000n\000g\000\040\000P\000h\000i\000l\000o\000s\000o\000p\000h\000e\000r\000s\000\040\000P\000r\000o\000b\000l\000e\000m}{chapter.6}% 24 -\BOOKMARK [1][]{section.6.3}{\376\377\0006\000.\0003\000\040\000S\000P\000I\000N\060\153\060\210\060\213\060\342\060\307\060\353\151\034\147\373}{chapter.6}% 25 -\BOOKMARK [1][]{section.6.4}{\376\377\0006\000.\0004\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\060\153\060\210\060\213\060\342\060\307\060\353\151\034\147\373\060\156\155\101\060\214}{chapter.6}% 26 -\BOOKMARK [1][]{section.6.5}{\376\377\0006\000.\0005\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\153\060\210\060\213\000D\000P\000P\060\156\133\237\210\305}{chapter.6}% 27 -\BOOKMARK [1][]{section.6.6}{\376\377\0006\000.\0006\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\153\060\210\060\213\000D\000P\000P\060\156\151\034\212\074}{chapter.6}% 28 -\BOOKMARK [1][]{section.6.7}{\376\377\0006\000.\0007\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\153\060\210\060\213\000\040\000l\000i\000v\000e\000\040\000l\000o\000c\000k\060\156\151\034\212\074\145\271\154\325\060\153\060\144\060\104\060\146}{chapter.6}% 29 -\BOOKMARK [1][]{section.6.8}{\376\377\0006\000.\0008\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\147\060\156\060\342\060\307\060\353\151\034\147\373\060\156\212\125\117\241}{chapter.6}% 30 -\BOOKMARK [0][]{chapter.7}{\376\377\173\054\0007\172\340\000\040\060\176\060\150\060\201\060\150\116\312\137\214\060\156\134\125\147\033}{}% 31 -\BOOKMARK [1][]{section.7.1}{\376\377\0007\000.\0001\000\040\116\312\137\214\060\156\212\262\230\114}{chapter.7}% 32 -\BOOKMARK [0][]{chapter*.7}{\376\377\213\035\217\236}{}% 33 -\BOOKMARK [0][]{chapter*.8}{\376\377\123\302\200\003\145\207\163\056}{}% 34 -\BOOKMARK [0][]{chapter*.8}{\376\377\116\330\223\062}{}% 35 -\BOOKMARK [0][]{appendix.A}{\376\377\116\330\000\040\223\062\000A\000\040\000\040\060\275\060\374\060\271\060\263\060\374\060\311\116\000\211\247}{}% 36 -\BOOKMARK [1][]{section.A.1}{\376\377\000A\000-\0001\000\040\170\024\172\166\117\032\166\172\210\150\214\307\145\231}{appendix.A}% 37 +\BOOKMARK [2][]{subsection.3.1.1}{\376\377\0003\000.\0001\000.\0001\000\040\225\242\145\160\060\156\133\237\210\305}{section.3.1}% 9 +\BOOKMARK [2][]{subsection.3.1.2}{\376\377\0003\000.\0001\000.\0002\000\040\116\214\230\005\157\024\173\227\133\120\060\156\133\237\210\305}{section.3.1}% 10 +\BOOKMARK [2][]{subsection.3.1.3}{\376\377\0003\000.\0001\000.\0003\000\040\000D\000a\000t\000a\000\040\127\213\060\156\133\237\210\305}{section.3.1}% 11 +\BOOKMARK [2][]{subsection.3.1.4}{\376\377\0003\000.\0001\000.\0004\000\040\000R\000e\000c\000o\000r\000d\000\040\127\213\060\156\133\237\210\305}{section.3.1}% 12 +\BOOKMARK [1][]{section.3.2}{\376\377\0003\000.\0002\000\040\147\054\212\326\060\147\117\177\165\050\060\131\060\213\000\040\000A\000g\000d\000a\000\040\060\156\212\030\154\325}{chapter.3}% 13 +\BOOKMARK [2][]{subsection.3.2.1}{\376\377\0003\000.\0002\000.\0001\000\040\000A\000g\000d\000a\060\156\167\001\165\145\212\030\154\325}{section.3.2}% 14 +\BOOKMARK [1][]{section.3.3}{\376\377\0003\000.\0003\000\040\000A\000g\000d\000a\060\153\060\210\060\213\133\232\164\006\212\074\146\016}{chapter.3}% 15 +\BOOKMARK [2][]{subsection.3.3.1}{\376\377\0003\000.\0003\000.\0001\000\040\201\352\161\066\145\160\060\153\0000\060\222\215\263\060\127\060\146\060\202\120\044\060\114\173\111\060\127\060\104\060\123\060\150\060\222\212\074\146\016\060\131\060\213\000A\000g\000d\000a}{section.3.3}% 16 +\BOOKMARK [2][]{subsection.3.3.2}{\376\377\0003\000.\0003\000.\0002\000\040\122\240\173\227\060\156\116\244\143\333\154\325\122\107\060\222\212\074\146\016\060\131\060\213\000A\000g\000d\000a}{section.3.3}% 17 +\BOOKMARK [0][]{chapter.4}{\376\377\173\054\0004\172\340\000\040\000G\000e\000a\000r\000s\000A\000g\000d\000a\000\040\137\142\137\017\060\147\146\370\060\117\000\040\000A\000g\000d\000a}{}% 18 +\BOOKMARK [1][]{section.4.1}{\376\377\0004\000.\0001\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\147\060\156\000\040\000M\000e\000t\000a\000\040\000G\000e\000a\000r\000s}{chapter.4}% 19 +\BOOKMARK [0][]{chapter.5}{\376\377\173\054\0005\172\340\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\153\060\210\060\213\133\232\164\006\212\074\146\016}{}% 20 +\BOOKMARK [1][]{section.5.1}{\376\377\0005\000.\0001\000\040\000H\000o\000a\000r\000e\000\040\000L\000o\000g\000i\000c}{chapter.5}% 21 +\BOOKMARK [1][]{section.5.2}{\376\377\0005\000.\0002\000\040\000I\000n\000v\000a\000r\000i\000a\000n\000t\000\040\060\222\165\050\060\104\060\137\000\040\000H\000o\000a\000r\000e\000\040\000L\000o\000g\000i\000c\000\040\060\153\060\210\060\213\151\034\212\074\060\156\145\271\154\325\000\040}{chapter.5}% 22 +\BOOKMARK [1][]{section.5.3}{\376\377\0005\000.\0003\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\153\060\146\000\040\000H\000o\000a\000r\000e\000\040\000L\000o\000g\000i\000c\000\040\060\222\165\050\060\104\060\137\151\034\212\074\060\156\117\213}{chapter.5}% 23 +\BOOKMARK [2][]{subsection.5.3.1}{\376\377\0005\000.\0003\000.\0001\000\040\000W\000h\000i\000l\000e\000\040\000L\000o\000o\000p\000\040\060\156\133\237\210\305}{section.5.3}% 24 +\BOOKMARK [2][]{subsection.5.3.2}{\376\377\0005\000.\0003\000.\0002\000\040\000W\000h\000i\000l\000e\000\040\000L\000o\000o\000p\000\040\060\156\151\034\212\074}{section.5.3}% 25 +\BOOKMARK [1][]{section.5.4}{\376\377\0005\000.\0004\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\153\060\112\060\121\060\213\000\040\000B\000i\000n\000a\000r\000y\000\040\000T\000r\000e\000e\000\040\060\156\151\034\212\074}{chapter.5}% 26 +\BOOKMARK [2][]{subsection.5.4.1}{\376\377\0005\000.\0004\000.\0001\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\153\060\112\060\121\060\213\147\050\151\313\220\040\060\156\212\055\212\010}{section.5.4}% 27 +\BOOKMARK [2][]{subsection.5.4.2}{\376\377\0005\000.\0004\000.\0002\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\153\060\112\060\121\060\213\000\040\000B\000i\000n\000a\000r\000y\000\040\000T\000r\000e\000e\000\040\060\156\133\237\210\305}{section.5.4}% 28 +\BOOKMARK [2][]{subsection.5.4.3}{\376\377\0005\000.\0004\000.\0003\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\153\060\112\060\121\060\213\000\040\000B\000i\000n\000a\000r\000y\000\040\000T\000r\000e\000e\000\040\060\156\151\034\212\074}{section.5.4}% 29 +\BOOKMARK [0][]{chapter.6}{\376\377\173\054\0006\172\340\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\153\060\210\060\213\060\342\060\307\060\353\151\034\147\373}{}% 30 +\BOOKMARK [1][]{section.6.1}{\376\377\0006\000.\0001\000\040\060\342\060\307\060\353\151\034\147\373\060\150\060\157}{chapter.6}% 31 +\BOOKMARK [1][]{section.6.2}{\376\377\0006\000.\0002\000\040\000D\000i\000n\000i\000n\000g\000\040\000P\000h\000i\000l\000o\000s\000o\000p\000h\000e\000r\000s\000\040\000P\000r\000o\000b\000l\000e\000m}{chapter.6}% 32 +\BOOKMARK [1][]{section.6.3}{\376\377\0006\000.\0003\000\040\000S\000P\000I\000N\060\153\060\210\060\213\060\342\060\307\060\353\151\034\147\373}{chapter.6}% 33 +\BOOKMARK [1][]{section.6.4}{\376\377\0006\000.\0004\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\060\153\060\210\060\213\060\342\060\307\060\353\151\034\147\373\060\156\155\101\060\214}{chapter.6}% 34 +\BOOKMARK [1][]{section.6.5}{\376\377\0006\000.\0005\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\153\060\210\060\213\000D\000P\000P\060\156\133\237\210\305}{chapter.6}% 35 +\BOOKMARK [1][]{section.6.6}{\376\377\0006\000.\0006\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\153\060\210\060\213\000D\000P\000P\060\156\151\034\212\074}{chapter.6}% 36 +\BOOKMARK [1][]{section.6.7}{\376\377\0006\000.\0007\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\153\060\210\060\213\000\040\000l\000i\000v\000e\000\040\000l\000o\000c\000k\060\156\151\034\212\074\145\271\154\325\060\153\060\144\060\104\060\146}{chapter.6}% 37 +\BOOKMARK [1][]{section.6.8}{\376\377\0006\000.\0008\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\147\060\156\060\342\060\307\060\353\151\034\147\373\060\156\212\125\117\241}{chapter.6}% 38 +\BOOKMARK [0][]{chapter.7}{\376\377\173\054\0007\172\340\000\040\060\176\060\150\060\201\060\150\116\312\137\214\060\156\134\125\147\033}{}% 39 +\BOOKMARK [1][]{section.7.1}{\376\377\0007\000.\0001\000\040\116\312\137\214\060\156\212\262\230\114}{chapter.7}% 40 +\BOOKMARK [0][]{chapter*.7}{\376\377\213\035\217\236}{}% 41 +\BOOKMARK [0][]{chapter*.8}{\376\377\123\302\200\003\145\207\163\056}{}% 42 +\BOOKMARK [0][]{chapter*.8}{\376\377\116\330\223\062}{}% 43 +\BOOKMARK [0][]{appendix.A}{\376\377\116\330\000\040\223\062\000A\000\040\000\040\060\275\060\374\060\271\060\263\060\374\060\311\116\000\211\247}{}% 44 +\BOOKMARK [1][]{section.A.1}{\376\377\000A\000-\0001\000\040\170\024\172\166\117\032\166\172\210\150\214\307\145\231}{appendix.A}% 45
--- a/Paper/src/agda-term3.agda Thu Feb 02 21:20:08 2023 +0900 +++ b/Paper/src/agda-term3.agda Fri Feb 03 03:06:18 2023 +0900 @@ -2,7 +2,7 @@ +-comm zero y rewrite (+zero {y}) = refl +-comm (suc x) y = let open ≡-Reasoning in begin - suc (x + y) ≡⟨⟩ + (suc x) + y ≡⟨⟩ suc (x + y) ≡⟨ cong suc (+-comm x y) ⟩ suc (y + x) ≡⟨ sym (+-suc {y} {x}) ⟩ y + suc x ∎
--- a/Paper/tex/agda.tex Thu Feb 02 21:20:08 2023 +0900 +++ b/Paper/tex/agda.tex Fri Feb 03 03:06:18 2023 +0900 @@ -2,126 +2,178 @@ Agda \cite{agda-wiki} \cite{Stump:2016:VFP:2841316} は純粋関数型言語である。 Agda は依存型という型システムを持ち、型を第一級オブジェクトとして扱う。 -また、もともとの Agda には自然数などの普遍的な定義すら存在しない。 +もともとの Agda には自然数などの普遍的な定義すら存在しない。 その実装ができることも本章で取り扱っているが、一般的には agda-standard-libralies \cite{agda-stdlib} を使用する。 本章ではAgdaの基本とAgdaによる定理証明の方法について述べる。 \section{Agdaの基本} -Agda の記述ではインデントが意味を持ち、スペースの有無もチェックされる。 -コメントは \verb/-- comment/ か \verb/{-- comment --}/ のように記述される。 -また、\verb/_/でそこに入りうるすべての値を示すことができ、 -\verb/?/でそこに入る値や型を不明瞭なままにしておくことができる。 +本節ではAgdaの基本事項についてソースコードを例に出しながら説明を行う。 + +\subsection{関数の実装} +Agdaでの関数の 定義方法について \coderef{plus} を例として解説する。 +基本事項として、$ \mathbb{N} $ というのは自然数 (Natulal Number) のことである。 +また - (ハイフン) が2つ連続して並んでいる部分はコメントアウトであり、 +ここでは関数を実行した際の例を記述している。 +したがって、これは2つの自然数を受け取って足す関数であることが推測できる。 + +\lstinputlisting[label=code:plus, caption=plusの実装] {src/agda/plus.agda.replaced} + +この関数の定義部分の説明をする。コードの1行目に : (セミコロン)がある。 +この : の前が関数名になり、その後ろがその関数の定義となる。 +: 以降の (x y : $ \mathbb{N} $) は関数は x, y の自然数2つを受けとるという意味になる。 +$ \rightarrow $ 以降は関数が返す型を記述している。 +まとめると、この関数 plus は、型が自然数である2つの変数 x, y を受け取り、 +自然数を返すという定義になる。 + +Agda では関数の定義をしたコードの直下で実装を行うのが常である。 +関数名を記述した後に引数を記述して受け取り、= (イコール) 以降で +引数に対応した実装をする。 -%% データについて -Agda では型をデータや関数に記述する必要がある。 -Agda における型指定は \verb/:/ を用いて \verb/name : type/ のように記述する。 -このとき \verb/name/ に 空白があってはいけない。 -データ型は、代数的なデータ構造で、その定義には \verb/data/ キーワードを用いる。 -\verb/data/ キーワードの後に \verb/data/ の名前と型を記述、 \verb/where/ 句を書きインデントを深くし、 -値にコンストラクタとその型を列挙する。 +今回の場合 plus x zero であれば +0 である為、そのまま x を返す。 +実装2行目の方で受け取った y の値を減らし、x の値を増やして再び plus の関数に +遷移している。 +受け取った y を +1 されていたとして y の値を減らしている。 + +関数の実装全体をまとめると、x と y の値を足す為に y から x に数値を1つずつ渡す。 +y が 0 になった際に計算が終了となっている。 +指折りでの足し算を実装していると捉えても良い。 -\coderef{agda-nat}は自然数の型である $\mathbb{N}$ (Natural Number)の例である。 +\subsection{二項演算子の実装} +\_ (アンダースコア) を用いることで入力を受け取る事ができる。 +これを用いることで、二項演算子を実装することができる。 +以下に、二項演算子を使用した \coderef{plus} と同義の関数の例を +以下 \coderef{plus2} 挙げる。 -\lstinputlisting[label=code:agda-nat, caption=自然数を表すデータ型 $\mathbb{N}$ の定義] {src/nat.agda.replaced} +\lstinputlisting[label=code:plus2, caption=二項演算子を用いたplusの実装, firstline=5] {src/agda/plus2.agda.replaced} -\verb/Nat/ では \verb/zero/ と \verb/suc/ の2つのコンストラクタを持つデータ型である。 -\verb/suc/ は $\mathbb{N}$ を受け取って $\mathbb{N}$ を返す再帰的なデータになっており、 -\verb/suc/ を連ねることで自然数全体を表現することができる。 +利点としては、直感的な記号論理の記述ができる。 +以下、記号論理は基本的に二項演算子を使用して記述する。 + +\begin{comment} +\subsection{Agdaにおけるラムダ計算} +\lambda +\end{comment} -$\mathbb{N}$ 自身の型は \verb/Set/ であり、これは Agda が組み込みで持つ「型集合の型」である。 -\verb/Set/ は階層構造を持ち、型集合の集合の型を指定するには \verb/Set1/ と書く。 -%% \verb/Level/ を用いることで異なる \verb/Set/ を表現できる。 +\subsection{Data 型の実装} +Deta 型とは分岐のことである。 +そのため、それぞれの動作について実装する必要がある。 +例として既出の Data 型である $ \mathbb{N} $ の実装を \coderef{Nat} に示す。 + +\lstinputlisting[label=code:Nat, caption=Natural の定義] {src/agda/Nat.agda.replaced} -Agda には C 言語における構造体に相当するレコード型というデータも存在する。 -例えば \verb/x/ と \verb/y/ の二つの自然数からなるレコード \verb/Point/ を定義する。\coderef{agda-record}のようになる。 -\lstinputlisting[label=code:agda-record, caption=Agdaにおけるレコード型の定義] {src/env.agda.replaced} -レコードを構築する際は \verb/record/ キーワード後の \verb/{}/ の内部に \verb/FieldName = value/ の形で値を列挙する。 -複数の値を列挙するには \verb/;/ で区切る必要がある。 +実装から、$ \mathbb{N} $ という型は zero と suc の2つのコンストラクタを持っていることが分かる。 +それぞれの仕様を見てみると、zeroは $ \mathbb{N} $ のみであるが、 +suc は (n : $ \mathbb{N} $ ) $ \rightarrow \ \mathbb{N} $ である。 +つまり、suc 自体の型は $ \mathbb{N} $ であるが、そこから $ \mathbb{N} $ に遷移するということである。 +そのため、suc からは suc か zero に遷移する必要があり、また zero に遷移することで停止する。 +したがって、数値は zero に遷移するまでの suc が遷移した数によって決定される。 + +Data型にはそれぞれの動作について実装する必要があると述べたが、 +言い換えればパターンマッチをする必要があると言える。 +これは puls 関数で suc 同士の場合と、zeroが含まれる場合の両方を実装していることの説明となる。 + +% \subsection{パターンマッチ} -%% 関数について -Agda での関数は型の定義と関数の定義をする必要がある。 -関数の型はデータと同様に \verb/:/ を用いて \verb/name : type/ と記述するが、入力を受け取り出力を返す型として記述される。または $\rightarrow$ を用いて \verb/input → output/ のように記述される。 -また \verb/_+_/のように関数名で\verb/_/を使用すると引数がその位置にあることを意味し、中間記法で関数を定義することもできる。 -関数の定義は型の定義より下の行に \verb/=/ を使い \verb/name input = output/ のように記述される。 +\subsection{Record 型の実装} +Record 型とはオブジェクトあるいは構造体ののようなものである。 +\coderef{Andの定義}は AND の関数となる。p1で前方部分が取得でき、p2で後方部分が取得できる。 + +\lstinputlisting[label=code:Andの定義, caption=Andの記述] {src/agda/And.agda.replaced} + +定義は「AならばB」かつ「BならばC」なら「AならばC」となる。 +\coderef{syllogism}を以下に示す。 + +\lstinputlisting[label=code:syllogism, caption=syllogism の記述] {src/agda/syllogism.agda.replaced} -例えば引数が型 \verb/A/ で返り値が型 \verb/B/ の関数は \verb/A → B/ のように書くことができる。 -また、複数の引数を取る関数の型は \verb/A → A → B/ のように書ける。 -例として任意の自然数$\mathbb{N}$を受け取り、それに1を加えた値を返す関数は\coderef{agda-function}のように定義できる。 -\lstinputlisting[label=code:agda-function, caption=Agda における関数定義] {src/agda-func.agda.replaced} +コードの解説をすると、引数として x と a が関数に与えられている。 +引数 x の中身は ((A $ \rightarrow $ B) ∧ (B $ \rightarrow $ C)) 、引数 a の中身 +は A である。したがって、(\_∧\_.p1 x a) で (A $ \rightarrow $ B) に A を与えて B を取得し、 +\_∧\_.p2 x で (B $ \rightarrow $ C) であるため、これに B を与えると C が取得できる。 +よって A を与えて C を取得することができたため、三段論法を定義できた。 + +\section{本論で使用する Agda の記法} +本論では、ソースコードを出し、それの実施内容について述べるが、 +特殊な記法を用いている場合があるので、前もって解説をする。 + +\subsection{Agdaの省略記法} +Recode が入力された場合のことを考える。この際、入力時に record を展開してしまうと、 +コードが長くなってしまい、煩雑になってしまう。 +これを防ぐために、withを使用し、必要な変数のみ取り出してパターンマッチを行う。 +例を \coderef{abridgement} に示す。 -引数は変数名で受けることもでき、具体的なコンストラクタを指定することでそのコンストラクタが渡された時の挙動を定義できる。 -これはパターンマッチと呼ばれ、コンストラクタで case 文を行なっているようなものである。 -例として自然数$\mathbb{N}$の加算を関数で書くと\coderef{agda-plus}のようになる。 - -\lstinputlisting[label=code:agda-plus, caption=自然数での加算の定義] {src/agda-plus.agda.replaced} -%% \lstinputlisting[label=agda-not, caption=Agdaにおける関数 not の定義] {src/AgdaNot.agda.replaced} +\lstinputlisting[label=code:abridgement, caption=入力を省略する Agda コードの例, firstline=5] {src/agda/abridgement.agda.replaced} -パターンマッチでは全てのコンストラクタのパターンを含む必要がある。 -例えば、自然数$\mathbb{N}$を受け取る関数では \verb/zero/ と \verb/suc/ の2つのパターンが存在する必要がある。 -なお、コンストラクタをいくつか指定した後に変数で受けることもでき、その変数では指定されたもの以外を受けることができる。 -例えば\coderef{agda-pattern}の減算では初めのパターンで2つ目の引数が\verb/zero/のすべてのパターンが入る。 - +patternmatch-default は入力されている record をそのまま展開することで、 +値を取得している。 -\lstinputlisting[label=code:agda-pattern, caption=自然数の減算によるパターンマッチの例] {src/agda-pattern.agda.replaced} - -Agda には$\lambda$計算が存在している。$\lambda$計算とは関数内で生成できる無名の関数であり、 -\verb/\arg1 arg2 → function/ または $\lambda$\verb/arg1 arg2 → function/ のように書くことができる。 -\coderef{agda-function} で例とした \verb/+1/ をラムダ計算で書くと\coderef{agda-lambda}の\verb/$\lambda$+1/ように書くことができる。この二つの関数は同一の動作をする。 +patternmatch-extraction では、with を使用して入力されているrecordの中から対象の +値だけ取得している。このように、入力時にrecordを展開せずに中の値を取得することも +できる。 -\lstinputlisting[label=code:agda-lambda, caption=Agda におけるラムダ計算] {src/AgdaLambda.agda.replaced} +patternmatch-extraction' では、入力が同じ場合に ... で省略ができることを使用し、 +さらに省略を行っている。 -Agda では特定の関数内のみで利用できる関数を \verb/where/ 句で記述できる。 -スコープは \verb/where/句が存在する関数内部のみであるため、名前空間が汚染させることも無い。 -例えば自然数3つを取ってそれぞれ3倍して加算する関数 \verb/f/ を定義するとき、 \verb/where/ を使うとリスト\coderef{agda-where} のように書ける。 -これは \verb/f'/ と同様の動作をする。 -\verb/where/ 句は利用したい関数の末尾にインデント付きで \verb/where/ キーワードを記述し、改行の後インデントをして関数内部で利用する関数を定義する。 - -\lstinputlisting[label=code:agda-where, caption=Agda における where 句] {src/AgdaWhere.agda.replaced} +今後のソースコードでは、必要な変数のみ取り出すことでコードを見やすくする。 -また Agda では停止性の検出機能が存在し、プログラム中に停止しない記述が存在するとコンパイル時にエラーが出る。 -\verb/{-# TERMINATING #-}/のタグを付けると停止しないプログラムをコンパイルすることができるがあまり望ましくない。 -\coderef{term} で書かれた、\verb/loop/ と \verb/stop/ は任意の自然数を受け取り、0になるまでループして0を返す関数である。 -\verb/loop/ では $\mathbb{N}$ の数を受け取り、 \verb/loop/ 自身を呼び出しながら 数を減らす関数 pred を呼んでいる。しかし、\verb/loop/の記述では関数が停止すると言えないため、定義するには\verb/{-# TERMINATING #-}/のタグが必要である。 -\verb/stop/ では自然数がパターンマッチで分けられ、\verb/zero/のときは \verb/zero/を返し、 \verb/suc n/ のときは \verb/suc/ を外した \verb/n/ で stop を実行するため停止する。 +%\subsection{<-cmp} +% 式変形の方が需要があるかもしれない -\lstinputlisting[label=code:term, caption=停止しない関数 loop、停止する関数 stop] {src/termination.agda.replaced} - -このように再帰的な定義の関数が停止するときは、何らかの値が減少する必要がある。 +% \lstinputlisting[label=syllogism, caption=syllogism, firstline=7,lastline=14] {src/agda/cmp.agda} \section{Agdaによる定理証明} -Agda での証明では関数の記述と同様の形で型部分に証明すべき論理式、 $\lambda$ 項部分にそれを満たす証明を書くことで証明を行うことが可能である。 -証明の例として \coderef{proof} を見る。 -ここでの \verb/+zero/ は右から \verb/zero/ を足しても ≡ の両辺は等しいことを証明している。 -これは、引数として受けている \verb/y/ が \verb/Nat/ なので、 \verb/zero/ の時と \verb/suc y/ の二つの場合を証明する必要がある。 +本説では、実際に Agda による定理証明の方法を簡単な例とその応用で可能な加算の交換法則の証明を用いて説明する。 + +\subsection{自然数に0を足しても値が等しいことを証明するAgda} +\coderef{proof}は型定義にも書いてあるとおり、自然数に0を足しても値が等しいことを証明するコードとなっている。 +このように、Agda では証明したい論理式を型定義に書き、実装部分に当たる2行目以降に証明を書くことができる。 \lstinputlisting[caption=等式変形の例,label=code:proof]{src/zero.agda.replaced} -\verb/y = zero/ の時は $zero \equiv zero$ とできて、左右の項が等しいということを表す \verb/refl/ で証明することができる。 -\verb/y = suc y/ の時は $x \equiv y$ の時 $fx \equiv fy$ が成り立つという -\coderef{cong}の \verb/cong/ を使って、y の値を 1 減らしたのち、再帰的に \verb/+zero y/ -を用いて証明している。 -\lstinputlisting[caption=congの定義,label=code:cong]{src/cong.agda.replaced} + +実際にコードの中で行われている証明について説明する。 +\{zero\}のパターンは$y$が0であったときの場合のことである。 +0に0を足しても0になるのは自明である。そのため refl (reflexivity) が使える。 +これは Agda で $\equiv$ の両辺が等しい場合に使われる記法である。 +つまり、$zero \equiv zero$ ということであり、それは証明として正しいことが得られた。 -%% \begin{lstlisting}[caption=等式変形の例,label=proof] -%% +zero : { y : ℕ } → y + zero ≡ y -%% +zero {zero} = refl -%% +zero {suc y} = cong ( λ x → suc x ) ( +zero {y} ) -%% -%% -- cong : ∀ (f : A → B) {x y} → x ≡ y → f x ≡ f y -%% -- cong f refl = refl -%% \end{lstlisting} +\{suc y\}はyが0以上、つまり1以上のパターンである。 +前述したzeroの場合は簡単に証明できた。 +ここで、足し算の実装を行った際のように、 +yが0であった場合に持っていくことができれば証明が行えることがわかる。 +そのために、\coderef{cong}のcongを使用する。 +\lstinputlisting[caption=congの定義,label=code:cong]{src/cong.agda.replaced} +これは、$x \equiv y$ の時 $fx \equiv fy$ が成り立つという関数になる。 +ここで注目すべきは $x \equiv y \rightarrow fx \equiv fy$ ということだ。 +つまり、$f$ を suc に見立てることで、$zero \equiv zero \rightarrow suc \: zero \equiv suc \: zero$ +が見えてくる。したがって、\{suc y\}の場合は$cong \: suc \: (\:+zero \: \{y\} \: )$となる。 +これにより y を減少させ続ける。0まで到達すると refl を得られる。あとは cong を使っていることにより元の値まで suc される流れとなる。 +以上のことから、自然数に0を足しても値が等しいことを証明できた。 -また、他にも $\lambda$ 項部分で等式を変形する構文がいくつか存在している。 -ここでは \verb/rewrite/ と ≡\verb/-Reasoning/ の構文を説明するとともに、等式を変形する構文の例として加算の交換則について示す。 + +\subsection{加算の交換法則を証明するAgda} + +次に、加算の交換法則を証明する。\coderef{agda-term-post} になる。 -\verb/rewrite/ では 関数の \verb/=/ 前に \verb/rewrite 変形規則/ の形で記述し、複数の規則を使う場合は \verb/rewrite/ 変形規則1 \verb/|/ 変形規則2 のように \verb/|/を用いて記述する。 -\coderef{agda-term-post} にある \verb/+-comm/ で \verb/x/ が \verb/zero/ のパターンが良い例である。 -ここでは、\verb/+zero/ を利用し、 \verb/zero + y/ を \verb/y/ に変形することで $y \equiv y$となり、左右の項が等しいことを示す \verb/refl/ になっている。 +再びzeroであった場合から考える。今回は受け取る引数は2つあるがxを基準としてパターンマッチさせている。 +xが0とは、yに0を足すということである。それは前項にてすでに行っている。 +そのため、rewrite による変形を使用する。 +これは = の前に rewrite 構文を使用することで等式を変形規則で記述することができる。 + +次に x が zero 以外の場合を考える。今回は ≡\verb/-Reasoning/ により式を展開している。 + \lstinputlisting[caption=congを用いた等式変形の例,label=code:agda-term-post]{src/agda-term3.agda.replaced} -\coderef{agda-term-post} では \verb/suc (y + x)/ $\equiv$ \verb/y + (suc x)/ という等式に対して $\equiv$ の対称律 \verb/sym/ を使って左右の項を反転させ\verb/y + (suc x)/ $\equiv$ \verb/suc (y + x)/の形にし、\verb/y + (suc x)/が\verb/suc (y + x)/ に変形できることを \verb/+-suc/ を用いて示した。 -これにより等式の左右の項が等しくなったため \verb/+-comm/ が示せた。 +これにより $ x + y \equiv y + x $ つまり $ (suc \: x) + y \equiv y + (suc \: x) $ を求めている +構文を説明すると、begin が始まりで $\blacksquare$ で終わりとなる。$\blacksquare$ は emacs-agda では $\backslash $qed で入力することができ、 +意味はそのまま Quod Erat Demonstrandum (証明終了) となる。 +証明の内部では、証明として正しいことが得られた$\equiv$の左項が始まる式であり、次の行の左項との一致を証明するのが右項となっている。 +5行目は自明であるため証明を省略できる。6行目は$ suc(x+y) \equiv suc (y+x) $ の証明をしている。これはcong sucを使ってこの関数自体を呼び出せば良い。 +7行目では$ suc (y+x) \equiv y+ suc \: x $の証明を行っている。これについては既存の方法ではできないので、10行目の+-sucにsymをかけている。 +symは $x \equiv y \rightarrow y \equiv x$ であり、等式なら左右を入れ替えてもよいとなる。 ++-sucでは再帰的にxを減少させることでreflを得るようになっている。 + +これらのことから、$ x + y \equiv y + x $を求めることができたため、Agdaにて加算の交換法則を証明することができた。 Agda ではこのような形で等式を変形しながら証明を行う事ができる。
--- a/Paper/tex/cbc.tex Thu Feb 02 21:20:08 2023 +0900 +++ b/Paper/tex/cbc.tex Fri Feb 03 03:06:18 2023 +0900 @@ -4,25 +4,18 @@ ことができるC言語である。 すなわちC言語の下位言語にあたり、よりアセンブラに近い記述を行う。 -CbC では CodeGear を処理の単位、 -DataGear をデータの単位として記述するプログラミング言語である。 +本章ではCbCの概要について説明する。 + +\section{CodeGear / DataGear} +CbCでは、プログラムの単位として DataGear と CodeGear という単位を用いる。 + +CodeGear はプログラムの処理そのものであり、一般的なプログラム言語における関数と同じ役割である。 +DataGear は CodeGear で扱うデータの単位であり、処理に必要なデータである。 jmp命令で関数遷移するため関数遷移し実行が終了しても、もとの関数に戻ることはない。 そのため次に遷移する CodeGear を指定する。 したがって、CodeGear に Deta Gear を与え、それをもとに処理を行い、 出力として DataGear を返し、また次の CodeGearに遷移していく流れとなる。 - -本章ではCbCの概要について説明する。 - -\section{CodeGear / DataGear} -CbCでは、検証しやすいプログラムの単位として DataGear と CodeGear という単位を用いる。 - -CodeGear はプログラムの処理そのものであり、一般的なプログラム言語における関数と同じ役割である。 -DataGear は CodeGear で扱うデータの単位であり、処理に必要なデータである。 -CodeGear の入力となる DataGear を Input DataGear と呼び、出力は Output DataGear と呼ぶ。 - -CodeGear 間の移動は継続を用いて行われる。 -継続は関数呼び出しとは異なり、呼び出した後に元のコードに戻れず、次の CodeGear へ遷移を行う。 これは、関数型プログラミングでは末尾再帰をしていることと同義である。 @@ -52,22 +45,17 @@ \lstinputlisting[label=code:c-ass, caption=cで記述した際の fib 関数のアセンブラ] {src/cbc/c.txt} \lstinputlisting[label=code:cbc-ass, caption=cbcで記述した際の fib 関数のアセンブラ] {src/cbc/cbc.txt} -以上のことから CbCが軽量継続を行っていると言える。 - +\section{Meta CodeGear / Meta DataGear} +プログラムを記述する際に、メモリ管理、スレッド管理、資源管理等の +プログラムの本筋とは別に実装が必要な場合がある。これらの計算をメタ計算と呼ぶ。 -\section{Meta CodeGear / Meta DataGear} -Meta DataGear は CbC 上のメタ計算で扱われる DataGear である。例えば stub -CodeGear では Context と呼ばれる接続可能な CodeGear、DataGear のリストや、DataGear +CbC ではメタ計算を分離するために Meta CodeGear、Meta DataGear を定義している。 +Meta CodeGear ではこのメタ計算を行い、Meta DataGear は CbC 上のメタ計算で扱われる DataGear である。 +例えば stub CodeGear では Context と呼ばれる接続可能な CodeGear、DataGear のリストや、DataGear のメモリ空間等を持った Meta DataGear を扱っている。 -また、プログラムを記述する際は、ノーマルレベルの計算の他に、メモリ管理、スレッド管理、資源管理等を記述しなければならない処理が存在する。 -これらの計算はノーマルレベルの計算と区別してメタ計算と呼ぶ。 -メタ計算は OS の機能を通して処理することが多く、信頼性の高い記述が求められる。 -そのため、 CbC ではメタ計算を分離するために Meta CodeGear、 Meta DataGear を定義している。 - -Meta CodeGear は CbC 上でのメタ計算で、通常の CodeGear を実行する際に必要なメタ計算を分離するための単位である。 -\figref{meta-cgdg} のように CodeGear を実行する前後や DataGear の大枠として Meta Gear が存在している。 +\figref{meta-cgdg} のように CodeGear を実行する前後や DataGear を内包する Meta Gear が存在している。 \begin{figure}[htpb] \begin{center}
--- a/Paper/tex/cbc_agda.tex Thu Feb 02 21:20:08 2023 +0900 +++ b/Paper/tex/cbc_agda.tex Fri Feb 03 03:06:18 2023 +0900 @@ -55,7 +55,7 @@ DataGear を作成する CodeGear を用いる。 加えて、実行なので命題の部分にある出力の型は Env になっている。 -\section{Agda による Meta Gears} +\section{Gears Agda での Meta Gears} 通常の Meta Gears はノーマルレベルの CodeGear、 DataGear では扱えないメタレベルの計算を扱う単位である。 今回は定理証明やモデル検査を行う際に使用する \cite{atton-master}。
--- a/Paper/tex/hoare.tex Thu Feb 02 21:20:08 2023 +0900 +++ b/Paper/tex/hoare.tex Fri Feb 03 03:06:18 2023 +0900 @@ -21,6 +21,10 @@ これらを満たし、 事前条件から事後条件を導けることを検証することで Hoare Logic の健全性を示すことができる。 +つまり、Hoare Triple の事後条件が次のコマンドの事前条件になり、それを実行終了まで繋げていくことで +Hoare Logic によるプログラムの検証とする。 + + \section{Invariant を用いた Hoare Logic による検証の方法 } \figref{meta-cgdg}を用いて Agda にて Hoare Logic による CodeGear を検証する流れを説明する。
--- a/Paper/tex/intro.tex Thu Feb 02 21:20:08 2023 +0900 +++ b/Paper/tex/intro.tex Fri Feb 03 03:06:18 2023 +0900 @@ -1,7 +1,7 @@ \chapter{Gears Agda でのプログラムの検証} OSやアプリケーションの信頼性の向上は重要である。 -信頼性を向上するための手段として、プログラムを検証する事が挙げられる。 +そのための手段として、プログラムが仕様を満たしているか検証する事が挙げられる。 しかし、仕様の形式化とその検証には膨大なコストを要する。 そのため、他のプログラミング言語と比べて検証に適している Gears Agda を使用する。