# HG changeset patch # User soto # Date 1674189603 -32400 # Node ID c28e8156a37b3dba3e2d118dd5b60b46a8031df6 # Parent 0425278b683b54a8b57bb1986003bc5235a5f06d Add paper init~agda diff -r 0425278b683b -r c28e8156a37b Paper/master_paper.out --- a/Paper/master_paper.out Thu Jan 12 20:31:09 2023 +0900 +++ b/Paper/master_paper.out Fri Jan 20 13:40:03 2023 +0900 @@ -2,25 +2,33 @@ \BOOKMARK [0][]{chapter*.3}{\376\377\170\024\172\166\225\242\220\043\212\326\145\207\151\155\176\076}{}% 1 \BOOKMARK [0][]{chapter.1}{\376\377\173\054\0001\172\340\000\040\000G\000e\000a\000r\000s\000\040\000A\000g\000d\000a\000\040\060\147\060\156\137\142\137\017\142\113\154\325}{}% 2 \BOOKMARK [0][]{chapter.2}{\376\377\173\054\0002\172\340\000\040\000C\000o\000n\000t\000i\000n\000u\000a\000t\000i\000o\000n\000\040\000b\000a\000s\000e\000d\000\040\000C}{}% 3 -\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\126\150\060\150\060\127\060\146\060\156\000\040\000A\000g\000d\000a}{}% 4 -\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}{}% 5 -\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}% 6 -\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}{}% 7 -\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}% 8 -\BOOKMARK [2][]{subsection.5.1.1}{\376\377\0005\000.\0001\000.\0001\000\040\000H\000o\000a\000r\000e\000\040\000L\000o\000g\000i\000c\000\040\060\153\060\210\060\213\000\040\000C\000o\000d\000e\000\040\000G\000e\000a\000r\000\040\060\156\151\034\212\074\142\113\154\325\000\040}{section.5.1}% 9 -\BOOKMARK [1][]{section.5.2}{\376\377\0005\000.\0002\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}% 10 -\BOOKMARK [2][]{subsection.5.2.1}{\376\377\0005\000.\0002\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.2}% 11 -\BOOKMARK [2][]{subsection.5.2.2}{\376\377\0005\000.\0002\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.2}% 12 -\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\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}% 13 -\BOOKMARK [2][]{subsection.5.3.1}{\376\377\0005\000.\0003\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.3}% 14 -\BOOKMARK [2][]{subsection.5.3.2}{\376\377\0005\000.\0003\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.3}% 15 -\BOOKMARK [2][]{subsection.5.3.3}{\376\377\0005\000.\0003\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.3}% 16 -\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}{}% 17 -\BOOKMARK [1][]{section.6.1}{\376\377\0006\000.\0001\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}% 18 -\BOOKMARK [2][]{subsection.6.1.1}{\376\377\0006\000.\0001\000.\0001\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}{section.6.1}% 19 -\BOOKMARK [0][]{chapter.7}{\376\377\173\054\0007\172\340\000\040\116\312\137\214\060\156\134\125\147\033}{}% 20 -\BOOKMARK [0][]{chapter*.7}{\376\377\213\035\217\236}{}% 21 -\BOOKMARK [0][]{chapter*.8}{\376\377\123\302\200\003\145\207\163\056}{}% 22 -\BOOKMARK [0][]{chapter*.8}{\376\377\116\330\223\062}{}% 23 -\BOOKMARK [0][]{appendix.A}{\376\377\116\330\000\040\223\062\000A\000\040\000\040\170\024\172\166\117\032\151\155\176\076}{}% 24 -\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}% 25 +\BOOKMARK [1][]{section.2.1}{\376\377\0002\000.\0001\000\040\000C\000o\000d\000e\000\040\000G\000e\000a\000r\000\040\000/\000\040\000D\000a\000t\000a\000\040\000G\000e\000a\000r}{chapter.2}% 4 +\BOOKMARK [1][]{section.2.2}{\376\377\0002\000.\0002\000\040\000C\000b\000C\000\040\060\150\000\040\000C\212\000\212\236\060\156\220\125\060\104}{chapter.2}% 5 +\BOOKMARK [1][]{section.2.3}{\376\377\0002\000.\0003\000\040\000M\000e\000t\000a\000\040\000C\000o\000d\000e\000\040\000G\000e\000a\000r\000\040\000/\000\040\000M\000e\000t\000a\000\040\000D\000a\000t\000a\000\040\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 [2][]{subsection.5.1.1}{\376\377\0005\000.\0001\000.\0001\000\040\000H\000o\000a\000r\000e\000\040\000L\000o\000g\000i\000c\000\040\060\153\060\210\060\213\000\040\000C\000o\000d\000e\000\040\000G\000e\000a\000r\000\040\060\156\151\034\212\074\142\113\154\325\000\040}{section.5.1}% 14 +\BOOKMARK [1][]{section.5.2}{\376\377\0005\000.\0002\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.2.1}{\376\377\0005\000.\0002\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.2}% 16 +\BOOKMARK [2][]{subsection.5.2.2}{\376\377\0005\000.\0002\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.2}% 17 +\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\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.3.1}{\376\377\0005\000.\0003\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.3}% 19 +\BOOKMARK [2][]{subsection.5.3.2}{\376\377\0005\000.\0003\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.3}% 20 +\BOOKMARK [2][]{subsection.5.3.3}{\376\377\0005\000.\0003\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.3}% 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\000S\000P\000I\000N\060\153\060\210\060\213\060\342\060\307\060\353\151\034\147\373}{chapter.6}% 24 +\BOOKMARK [1][]{section.6.3}{\376\377\0006\000.\0003\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}% 25 +\BOOKMARK [1][]{section.6.4}{\376\377\0006\000.\0004\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}% 26 +\BOOKMARK [2][]{subsection.6.4.1}{\376\377\0006\000.\0004\000.\0001\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}{section.6.4}% 27 +\BOOKMARK [0][]{chapter.7}{\376\377\173\054\0007\172\340\000\040\116\312\137\214\060\156\134\125\147\033}{}% 28 +\BOOKMARK [0][]{chapter*.7}{\376\377\213\035\217\236}{}% 29 +\BOOKMARK [0][]{chapter*.8}{\376\377\123\302\200\003\145\207\163\056}{}% 30 +\BOOKMARK [0][]{chapter*.8}{\376\377\116\330\223\062}{}% 31 +\BOOKMARK [0][]{appendix.A}{\376\377\116\330\000\040\223\062\000A\000\040\000\040\170\024\172\166\117\032\151\155\176\076}{}% 32 +\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}% 33 diff -r 0425278b683b -r c28e8156a37b Paper/master_paper.pdf Binary file Paper/master_paper.pdf has changed diff -r 0425278b683b -r c28e8156a37b Paper/master_paper.tex --- a/Paper/master_paper.tex Thu Jan 12 20:31:09 2023 +0900 +++ b/Paper/master_paper.tex Fri Jan 20 13:40:03 2023 +0900 @@ -138,6 +138,9 @@ 加えて、CbCでは並列処理も実行できる\cite{parusu-master}が、 並列処理を定理証明にて検証するには考慮する状態が多すぎる。 そのため、並列処理はモデル検査にて検証する。 +\section{モデル検査とは} +\section{SPINによるモデル検査}% 内容にそぐわない場合は使わない +\section{Gears Agdaによるモデル検査の流れ} \input{tex/dpp_impl.tex}% Gears Agda の記法　loopのやつやる diff -r 0425278b683b -r c28e8156a37b Paper/src/agda/_Fresh.agda.replaced --- a/Paper/src/agda/_Fresh.agda.replaced Thu Jan 12 20:31:09 2023 +0900 +++ b/Paper/src/agda/_Fresh.agda.replaced Fri Jan 20 13:40:03 2023 +0900 @@ -1,7 +1,7 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- Fresh lists, a proof relevant variant of Catarina Coquand's contexts in +-- Fresh lists, a proof relevant variant of Catarina Coquand!$\prime$!s contexts in -- "A Formalised Proof of the Soundness and Completeness of a Simply Typed -- Lambda-Calculus with Explicit Substitutions" ------------------------------------------------------------------------ @@ -15,8 +15,8 @@ open import Level using (Level; _!$\sqcup$!_) open import Data.Bool.Base using (true; false) -open import Data.Unit.Polymorphic.Base using (⊤) -open import Data.Product using (∃; _!$\times$!_; _,_; -,_; proj!$\text{1}$!; proj₂) +open import Data.Unit.Polymorphic.Base using (!$\top$!) +open import Data.Product using (∃; _!$\times$!_; _,_; -,_; proj!$\text{1}$!; proj!$\text{2}$!) open import Data.List.Relation.Unary.All using (All; []; _!$\text{::}$!_) open import Data.List.Relation.Unary.AllPairs using (AllPairs; []; _!$\text{::}$!_) open import Data.Maybe.Base as Maybe using (Maybe; just; nothing) @@ -57,7 +57,7 @@ infixr 5 _!$\text{::}$!#_ pattern _!$\text{::}$!#_ x xs = cons x xs _ - fresh a [] = ⊤ + fresh a [] = !$\top$! fresh a (x !$\text{::}$!# xs) = R a x !$\times$! fresh a xs -- Convenient notation for freshness making A and R implicit parameters @@ -86,8 +86,8 @@ module _ {R : Rel A r} {S : Rel A s} (R!$\Rightarrow$!S : ∀[ R !$\Rightarrow$! S ]) where - map₂ : List# A R !$\rightarrow$! List# A S - map₂ = map id R!$\Rightarrow$!S + map!$\text{2}$! : List# A R !$\rightarrow$! List# A S + map!$\text{2}$! = map id R!$\Rightarrow$!S ------------------------------------------------------------------------ -- Views @@ -136,7 +136,7 @@ head = Maybe.map proj!$\text{1}$! ∘′ uncons tail : {R : Rel A r} !$\rightarrow$! List# A R !$\rightarrow$! Maybe (List# A R) -tail = Maybe.map proj₂ ∘′ uncons +tail = Maybe.map proj!$\text{2}$! ∘′ uncons take : {R : Rel A r} !$\rightarrow$! !$\mathbb{N}$! !$\rightarrow$! List# A R !$\rightarrow$! List# A R take-# : {R : Rel A r} !$\rightarrow$! ∀ n a (as : List# A R) !$\rightarrow$! a # as !$\rightarrow$! a # take n as @@ -195,7 +195,7 @@ toAll : ∀ {R : Rel A r} {a} as !$\rightarrow$! fresh A R a as !$\rightarrow$! All (R a) (proj!$\text{1}$! (toList as)) toList [] = -, [] -toList (cons x xs ps) = -, toAll xs ps !$\text{::}$! proj₂ (toList xs) +toList (cons x xs ps) = -, toAll xs ps !$\text{::}$! proj!$\text{2}$! (toList xs) toAll [] ps = [] toAll (a !$\text{::}$!# as) (p , ps) = p !$\text{::}$! toAll as ps diff -r 0425278b683b -r c28e8156a37b Paper/src/agda/abridgement.agda.replaced --- a/Paper/src/agda/abridgement.agda.replaced Thu Jan 12 20:31:09 2023 +0900 +++ b/Paper/src/agda/abridgement.agda.replaced Fri Jan 20 13:40:03 2023 +0900 @@ -16,7 +16,7 @@ patternmatch-extraction env with c env patternmatch-extraction env | c = c -patternmatch-extraction' : env !$\rightarrow$! !$\mathbb{N}$! -patternmatch-extraction' env with c env +patternmatch-extraction!$\prime$! : env !$\rightarrow$! !$\mathbb{N}$! +patternmatch-extraction!$\prime$! env with c env ... | c = c diff -r 0425278b683b -r c28e8156a37b Paper/src/agda/hoare-while.agda.replaced --- a/Paper/src/agda/hoare-while.agda.replaced Thu Jan 12 20:31:09 2023 +0900 +++ b/Paper/src/agda/hoare-while.agda.replaced Fri Jan 20 13:40:03 2023 +0900 @@ -69,15 +69,15 @@ proof5 : (suc zero !$\leq$! (varn env)) !$\rightarrow$! ((varn env ) - 1) + (vari env + 1) !$\equiv$! c10 env proof5 (s!$\leq$!s lt) with varn env proof5 (s!$\leq$!s z!$\leq$!n) | zero = !$\bot$!-elim (1<0 a) - proof5 (s!$\leq$!s (z!$\leq$!n {n'}) ) | suc n = let open !$\equiv$!-Reasoning in + proof5 (s!$\leq$!s (z!$\leq$!n {n!$\prime$!}) ) | suc n = let open !$\equiv$!-Reasoning in begin - n' + (vari env + 1) - !$\equiv$!!$\langle$! cong ( !$\lambda$! z !$\rightarrow$! n' + z ) ( +-sym {vari env} {1} ) !$\rangle$! - n' + (1 + vari env ) - !$\equiv$!!$\langle$! sym ( +-assoc (n') 1 (vari env) ) !$\rangle$! - (n' + 1) + vari env + n!$\prime$! + (vari env + 1) + !$\equiv$!!$\langle$! cong ( !$\lambda$! z !$\rightarrow$! n!$\prime$! + z ) ( +-sym {vari env} {1} ) !$\rangle$! + n!$\prime$! + (1 + vari env ) + !$\equiv$!!$\langle$! sym ( +-assoc (n!$\prime$!) 1 (vari env) ) !$\rangle$! + (n!$\prime$! + 1) + vari env !$\equiv$!!$\langle$! cong ( !$\lambda$! z !$\rightarrow$! z + vari env ) +1!$\equiv$!suc !$\rangle$! - (suc n' ) + vari env + (suc n!$\prime$! ) + vari env !$\equiv$!!$\langle$!!$\rangle$! varn env + vari env !$\equiv$!!$\langle$! s !$\rangle$! @@ -85,14 +85,14 @@ !$\blacksquare$! -whileLoopPwP' : {l : Level} {t : Set l} !$\rightarrow$! (n : !$\mathbb{N}$!) !$\rightarrow$! (env : Envc ) !$\rightarrow$! (n !$\equiv$! varn env) !$\rightarrow$! whileTestStateP s2 env +whileLoopPwP!$\prime$! : {l : Level} {t : Set l} !$\rightarrow$! (n : !$\mathbb{N}$!) !$\rightarrow$! (env : Envc ) !$\rightarrow$! (n !$\equiv$! varn env) !$\rightarrow$! whileTestStateP s2 env !$\rightarrow$! (next : (env : Envc ) !$\rightarrow$! (pred n !$\equiv$! varn env) !$\rightarrow$! whileTestStateP s2 env !$\rightarrow$! t) !$\rightarrow$! (exit : (env : Envc ) !$\rightarrow$! whileTestStateP sf env !$\rightarrow$! t) !$\rightarrow$! t -whileLoopPwP' zero env refl refl next exit = exit env refl -whileLoopPwP' (suc n) env refl refl next exit = next (record env {varn = pred (varn env) ; vari = suc (vari env) }) refl (+-suc n (vari env)) +whileLoopPwP!$\prime$! zero env refl refl next exit = exit env refl +whileLoopPwP!$\prime$! (suc n) env refl refl next exit = next (record env {varn = pred (varn env) ; vari = suc (vari env) }) refl (+-suc n (vari env)) -whileTestPSemSound : (c : !$\mathbb{N}$! ) (output : Envc ) !$\rightarrow$! output !$\equiv$! whileTestP c (!$\lambda$! e !$\rightarrow$! e) !$\rightarrow$! ⊤ implies ((vari output !$\equiv$! 0) /\ (varn output !$\equiv$! c)) +whileTestPSemSound : (c : !$\mathbb{N}$! ) (output : Envc ) !$\rightarrow$! output !$\equiv$! whileTestP c (!$\lambda$! e !$\rightarrow$! e) !$\rightarrow$! !$\top$! implies ((vari output !$\equiv$! 0) /\ (varn output !$\equiv$! c)) whileTestPSemSound c output refl = whileTestPSem c diff -r 0425278b683b -r c28e8156a37b Paper/src/agda/lambda.agda.replaced --- a/Paper/src/agda/lambda.agda.replaced Thu Jan 12 20:31:09 2023 +0900 +++ b/Paper/src/agda/lambda.agda.replaced Fri Jan 20 13:40:03 2023 +0900 @@ -19,10 +19,10 @@ test*2 : (a : !$\mathbb{N}$!) !$\rightarrow$! !$\mathbb{N}$! test*2 a = +n a (!$\lambda$! z !$\rightarrow$! z + 2) -test*2' : (a : !$\mathbb{N}$!) !$\rightarrow$! !$\mathbb{N}$! -test*2' a = +n a (!$\lambda$! z !$\rightarrow$! +n z (!$\lambda$! z !$\rightarrow$! z)) +test*2!$\prime$! : (a : !$\mathbb{N}$!) !$\rightarrow$! !$\mathbb{N}$! +test*2!$\prime$! a = +n a (!$\lambda$! z !$\rightarrow$! +n z (!$\lambda$! z !$\rightarrow$! z)) -!$\lambda$!'+2 : (x : !$\mathbb{N}$!) !$\rightarrow$! !$\mathbb{N}$! -!$\lambda$!'+2 d = {!!} -- (!$\lambda$! x !$\rightarrow$! x +1) +!$\lambda$!!$\prime$!+2 : (x : !$\mathbb{N}$!) !$\rightarrow$! !$\mathbb{N}$! +!$\lambda$!!$\prime$!+2 d = {!!} -- (!$\lambda$! x !$\rightarrow$! x +1) diff -r 0425278b683b -r c28e8156a37b Paper/src/agda/list-any.agda.replaced --- a/Paper/src/agda/list-any.agda.replaced Thu Jan 12 20:31:09 2023 +0900 +++ b/Paper/src/agda/list-any.agda.replaced Fri Jan 20 13:40:03 2023 +0900 @@ -60,13 +60,13 @@ testany1 bt-empty = {!!} testany1 (bt-node record { key = key ; ltree = ltree ; rtree = rtree }) = {!!} -testrbt1 = whileTestPCall' bt-empty 0 -testrbt2 = whileTestPCall' (Env.vart testrbt1) 1 -testrbt3 = whileTestPCall' (Env.vart testrbt2) 2 -testrbt4 = whileTestPCall' (Env.vart testrbt3) 3 -testrbt5 = whileTestPCall' (Env.vart testrbt4) 4 -testrbt6 = whileTestPCall' (Env.vart testrbt5) 5 -testrbt7 = whileTestPCall' (Env.vart testrbt6) 6 +testrbt1 = whileTestPCall!$\prime$! bt-empty 0 +testrbt2 = whileTestPCall!$\prime$! (Env.vart testrbt1) 1 +testrbt3 = whileTestPCall!$\prime$! (Env.vart testrbt2) 2 +testrbt4 = whileTestPCall!$\prime$! (Env.vart testrbt3) 3 +testrbt5 = whileTestPCall!$\prime$! (Env.vart testrbt4) 4 +testrbt6 = whileTestPCall!$\prime$! (Env.vart testrbt5) 5 +testrbt7 = whileTestPCall!$\prime$! (Env.vart testrbt6) 6 test1kk = 100 ∈ (Env.vart testrbt6) diff -r 0425278b683b -r c28e8156a37b Paper/src/agda/rbt_imple.agda.replaced --- a/Paper/src/agda/rbt_imple.agda.replaced Thu Jan 12 20:31:09 2023 +0900 +++ b/Paper/src/agda/rbt_imple.agda.replaced Fri Jan 20 13:40:03 2023 +0900 @@ -74,23 +74,23 @@ bt-empty : rbt-meta bt-node : (node : tree-meta (node col !$\mathbb{N}$! ) meta rbt-meta rbt-meta ) !$\rightarrow$! rbt-meta -test'1 = whileTestPCall' bt-empty 0 -test'2 = whileTestPCall' (rbt_t.Env.vart test'1) 1 -test'3 = whileTestPCall' (rbt_t.Env.vart test'2) 2 -test'4 = whileTestPCall' (rbt_t.Env.vart test'3) 3 -test'5 = whileTestPCall' (rbt_t.Env.vart test'4) 4 -test'6 = whileTestPCall' (rbt_t.Env.vart test'5) 5 -test'7 = whileTestPCall' (rbt_t.Env.vart test'6) 6 -test'8 = whileTestPCall' (rbt_t.Env.vart test'7) 7 -test'9 = whileTestPCall' (rbt_t.Env.vart test'8) 8 -test'10 = whileTestPCall' (rbt_t.Env.vart test'9) 9 -test'11 = whileTestPCall' (rbt_t.Env.vart test'10) 10 -test'12 = whileTestPCall' (rbt_t.Env.vart test'11) 11 -test'13 = whileTestPCall' (rbt_t.Env.vart test'12) 12 -test'14 = whileTestPCall' (rbt_t.Env.vart test'13) 13 -test'15 = whileTestPCall' (rbt_t.Env.vart test'14) 14 +test!$\prime$!1 = whileTestPCall!$\prime$! bt-empty 0 +test!$\prime$!2 = whileTestPCall!$\prime$! (rbt_t.Env.vart test!$\prime$!1) 1 +test!$\prime$!3 = whileTestPCall!$\prime$! (rbt_t.Env.vart test!$\prime$!2) 2 +test!$\prime$!4 = whileTestPCall!$\prime$! (rbt_t.Env.vart test!$\prime$!3) 3 +test!$\prime$!5 = whileTestPCall!$\prime$! (rbt_t.Env.vart test!$\prime$!4) 4 +test!$\prime$!6 = whileTestPCall!$\prime$! (rbt_t.Env.vart test!$\prime$!5) 5 +test!$\prime$!7 = whileTestPCall!$\prime$! (rbt_t.Env.vart test!$\prime$!6) 6 +test!$\prime$!8 = whileTestPCall!$\prime$! (rbt_t.Env.vart test!$\prime$!7) 7 +test!$\prime$!9 = whileTestPCall!$\prime$! (rbt_t.Env.vart test!$\prime$!8) 8 +test!$\prime$!10 = whileTestPCall!$\prime$! (rbt_t.Env.vart test!$\prime$!9) 9 +test!$\prime$!11 = whileTestPCall!$\prime$! (rbt_t.Env.vart test!$\prime$!10) 10 +test!$\prime$!12 = whileTestPCall!$\prime$! (rbt_t.Env.vart test!$\prime$!11) 11 +test!$\prime$!13 = whileTestPCall!$\prime$! (rbt_t.Env.vart test!$\prime$!12) 12 +test!$\prime$!14 = whileTestPCall!$\prime$! (rbt_t.Env.vart test!$\prime$!13) 13 +test!$\prime$!15 = whileTestPCall!$\prime$! (rbt_t.Env.vart test!$\prime$!14) 14 -testdata = rbt_t.Env.vart test'7 +testdata = rbt_t.Env.vart test!$\prime$!7 -- ここからmetaの作成 @@ -136,5 +136,5 @@ ; rtree = makemeta-comm (rtree node) (node.number (key node)) ( record { deeps = 1 ; black-nodes = 1 ; l-list = [] ; r-list = insert-r (node.number (key node)) [] } ) }) ----test11 = makemeta (rbt_t.Env.vart test'11) +---test11 = makemeta (rbt_t.Env.vart test!$\prime$!11) -} diff -r 0425278b683b -r c28e8156a37b Paper/src/agda/rbt_t.agda.replaced --- a/Paper/src/agda/rbt_t.agda.replaced Thu Jan 12 20:31:09 2023 +0900 +++ b/Paper/src/agda/rbt_t.agda.replaced Fri Jan 20 13:40:03 2023 +0900 @@ -219,17 +219,17 @@ -- skewはnextがrotate-right．exitはsplitとなる -- skewの中にrotate-rightが内包され，実行後は必ずsplitに遷移する -- それはskewのexitと等しいので同時に記述してやる． -skew' : {l : Level} {t : Set l} !$\rightarrow$! Env !$\rightarrow$! (exit : Env !$\rightarrow$! t) !$\rightarrow$! t -skew' env exit = skew-bt env (!$\lambda$! env !$\rightarrow$! merge-rotate-left env exit exit ) exit +skew!$\prime$! : {l : Level} {t : Set l} !$\rightarrow$! Env !$\rightarrow$! (exit : Env !$\rightarrow$! t) !$\rightarrow$! t +skew!$\prime$! env exit = skew-bt env (!$\lambda$! env !$\rightarrow$! merge-rotate-left env exit exit ) exit -split' : {l : Level} {t : Set l} !$\rightarrow$! Env !$\rightarrow$! (exit : Env !$\rightarrow$! t) !$\rightarrow$! t -split' env exit = split-branch env (!$\lambda$! env !$\rightarrow$! merge-rotate-right env (!$\lambda$! env !$\rightarrow$! split env exit exit ) (!$\lambda$! env !$\rightarrow$! split env exit exit ) ) exit +split!$\prime$! : {l : Level} {t : Set l} !$\rightarrow$! Env !$\rightarrow$! (exit : Env !$\rightarrow$! t) !$\rightarrow$! t +split!$\prime$! env exit = split-branch env (!$\lambda$! env !$\rightarrow$! merge-rotate-right env (!$\lambda$! env !$\rightarrow$! split env exit exit ) (!$\lambda$! env !$\rightarrow$! split env exit exit ) ) exit {- -merge' : {l : Level} {t : Set l} !$\rightarrow$! Env !$\rightarrow$! (exit : Env !$\rightarrow$! t) !$\rightarrow$! t -merge' node@record { vart = vart ; varn = varn ; varl = [] } exit = exit node -merge' node@record { vart = vart ; varn = varn ; varl = (x !$\text{::}$! varl!$\text{1}$!) } exit = merge' (merge-tree node (!$\lambda$! env !$\rightarrow$! skew' env (!$\lambda$! env !$\rightarrow$! split' env (!$\lambda$! env !$\rightarrow$! env) ) ) (!$\lambda$! env !$\rightarrow$! env) ) exit +merge!$\prime$! : {l : Level} {t : Set l} !$\rightarrow$! Env !$\rightarrow$! (exit : Env !$\rightarrow$! t) !$\rightarrow$! t +merge!$\prime$! node@record { vart = vart ; varn = varn ; varl = [] } exit = exit node +merge!$\prime$! node@record { vart = vart ; varn = varn ; varl = (x !$\text{::}$! varl!$\text{1}$!) } exit = merge!$\prime$! (merge-tree node (!$\lambda$! env !$\rightarrow$! skew!$\prime$! env (!$\lambda$! env !$\rightarrow$! split!$\prime$! env (!$\lambda$! env !$\rightarrow$! env) ) ) (!$\lambda$! env !$\rightarrow$! env) ) exit -} whileTestP : {l : Level} {t : Set l} !$\rightarrow$! (tree : rbt) !$\rightarrow$! (n : !$\mathbb{N}$!) !$\rightarrow$! (Code : Env !$\rightarrow$! t) !$\rightarrow$! t @@ -239,7 +239,7 @@ {-# TERMINATING #-} mergeP : {l : Level} {t : Set l} !$\rightarrow$! Env !$\rightarrow$! (exit : Env !$\rightarrow$! t) !$\rightarrow$! t -mergeP env exit = merge-tree env (!$\lambda$! env !$\rightarrow$! skew' env (!$\lambda$! env !$\rightarrow$! split' env (!$\lambda$! env !$\rightarrow$! mergeP env exit)) ) exit +mergeP env exit = merge-tree env (!$\lambda$! env !$\rightarrow$! skew!$\prime$! env (!$\lambda$! env !$\rightarrow$! split!$\prime$! env (!$\lambda$! env !$\rightarrow$! mergeP env exit)) ) exit {- mergeP1 : {l : Level} {t : Set l} !$\rightarrow$! Env !$\rightarrow$! (exit : Env !$\rightarrow$! t) !$\rightarrow$! t @@ -265,19 +265,19 @@ --whileTestPCall : (tree : rbt) !$\rightarrow$! (n : !$\mathbb{N}$!) !$\rightarrow$! Env --whileTestPCall tree n = whileTestP {_} {_} tree n (!$\lambda$! env !$\rightarrow$! insert env (!$\lambda$! env !$\rightarrow$! merge env (!$\lambda$! env !$\rightarrow$! init-col env (!$\lambda$! env !$\rightarrow$! env ) ) ) ) -whileTestPCall' : (tree : rbt) !$\rightarrow$! (n : !$\mathbb{N}$!) !$\rightarrow$! Env -whileTestPCall' tree n = whileTestP {_} {_} tree n (!$\lambda$! env !$\rightarrow$! insert env (!$\lambda$! env !$\rightarrow$! mergeP env (!$\lambda$! env !$\rightarrow$! init-col env (!$\lambda$! env !$\rightarrow$! env ) ) ) ) +whileTestPCall!$\prime$! : (tree : rbt) !$\rightarrow$! (n : !$\mathbb{N}$!) !$\rightarrow$! Env +whileTestPCall!$\prime$! tree n = whileTestP {_} {_} tree n (!$\lambda$! env !$\rightarrow$! insert env (!$\lambda$! env !$\rightarrow$! mergeP env (!$\lambda$! env !$\rightarrow$! init-col env (!$\lambda$! env !$\rightarrow$! env ) ) ) ) -- 以下test部分 -test1 = whileTestPCall' bt-empty 8 -test2 = whileTestPCall' (vart test1) 10 -test3 = whileTestPCall' (vart test2) 24 -test4 = whileTestPCall' (vart test3) 31 -test5 = whileTestPCall' (vart test4) 41 -test6 = whileTestPCall' (vart test5) 45 -test7 = whileTestPCall' (vart test6) 50 -test8 = whileTestPCall' (vart test7) 59 -test9 = whileTestPCall' (vart test8) 73 -test10 = whileTestPCall' (vart test9) 74 -test11 = whileTestPCall' (vart test10) 79 +test1 = whileTestPCall!$\prime$! bt-empty 8 +test2 = whileTestPCall!$\prime$! (vart test1) 10 +test3 = whileTestPCall!$\prime$! (vart test2) 24 +test4 = whileTestPCall!$\prime$! (vart test3) 31 +test5 = whileTestPCall!$\prime$! (vart test4) 41 +test6 = whileTestPCall!$\prime$! (vart test5) 45 +test7 = whileTestPCall!$\prime$! (vart test6) 50 +test8 = whileTestPCall!$\prime$! (vart test7) 59 +test9 = whileTestPCall!$\prime$! (vart test8) 73 +test10 = whileTestPCall!$\prime$! (vart test9) 74 +test11 = whileTestPCall!$\prime$! (vart test10) 79 diff -r 0425278b683b -r c28e8156a37b Paper/src/bt_verif/invariant.agda.replaced --- a/Paper/src/bt_verif/invariant.agda.replaced Thu Jan 12 20:31:09 2023 +0900 +++ b/Paper/src/bt_verif/invariant.agda.replaced Fri Jan 20 13:40:03 2023 +0900 @@ -1,12 +1,12 @@ treeInvariant : {n : Level} {A : Set n} !$\rightarrow$! (tree : bt A) !$\rightarrow$! Set -treeInvariant leaf = ⊤ -treeInvariant (node key value leaf leaf) = ⊤ -treeInvariant (node key value leaf n@(node key!$\text{1}$! value!$\text{1}$! t!$\text{1}$! t₂)) = (key < key!$\text{1}$!) !$\wedge$! treeInvariant n +treeInvariant leaf = !$\top$! +treeInvariant (node key value leaf leaf) = !$\top$! +treeInvariant (node key value leaf n@(node key!$\text{1}$! value!$\text{1}$! t!$\text{1}$! t!$\text{2}$!)) = (key < key!$\text{1}$!) !$\wedge$! treeInvariant n treeInvariant (node key value n@(node key!$\text{1}$! value!$\text{1}$! t t!$\text{1}$!) leaf) = treeInvariant n !$\wedge$! (key < key!$\text{1}$!) -treeInvariant (node key value n@(node key!$\text{1}$! value!$\text{1}$! t t!$\text{1}$!) m@(node key₂ value₂ t₂ t₃)) = treeInvariant n !$\wedge$! (key < key!$\text{1}$!) !$\wedge$! (key!$\text{1}$! < key₂) !$\wedge$! treeInvariant m +treeInvariant (node key value n@(node key!$\text{1}$! value!$\text{1}$! t t!$\text{1}$!) m@(node key!$\text{2}$! value!$\text{2}$! t!$\text{2}$! t!$\text{3}$!)) = treeInvariant n !$\wedge$! (key < key!$\text{1}$!) !$\wedge$! (key!$\text{1}$! < key!$\text{2}$!) !$\wedge$! treeInvariant m stackInvariant : {n : Level} {A : Set n} !$\rightarrow$! (tree : bt A) !$\rightarrow$! (stack : List (bt A)) !$\rightarrow$! Set n -stackInvariant {_} {A} _ [] = Lift _ ⊤ +stackInvariant {_} {A} _ [] = Lift _ !$\top$! stackInvariant {_} {A} tree (tree1 !$\text{::}$! [] ) = tree1 !$\equiv$! tree stackInvariant {_} {A} tree (x !$\text{::}$! tail @ (node key value leaf right !$\text{::}$! _) ) = (right !$\equiv$! x) !$\wedge$! stackInvariant tree tail stackInvariant {_} {A} tree (x !$\text{::}$! tail @ (node key value left leaf !$\text{::}$! _) ) = (left !$\equiv$! x) !$\wedge$! stackInvariant tree tail diff -r 0425278b683b -r c28e8156a37b Paper/src/cbc/c.out Binary file Paper/src/cbc/c.out has changed diff -r 0425278b683b -r c28e8156a37b Paper/src/cbc/c.txt --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/cbc/c.txt Fri Jan 20 13:40:03 2023 +0900 @@ -0,0 +1,33 @@ +0000000100000e52 _fib: +100000e52: 55 pushq %rbp +100000e53: 48 89 e5 movq %rsp, %rbp +100000e56: 48 83 ec 20 subq $32, %rsp +100000e5a: 48 89 7d f8 movq %rdi, -8(%rbp) +100000e5e: 48 89 75 f0 movq %rsi, -16(%rbp) +100000e62: 48 89 55 e8 movq %rdx, -24(%rbp) +100000e66: 48 83 7d f8 00 cmpq $0, -8(%rbp) +100000e6b: 75 0c jne 12 <_fib+0x27> +100000e6d: 48 8b 45 f0 movq -16(%rbp), %rax +100000e71: 48 89 c7 movq %rax, %rdi +100000e74: e8 ab ff ff ff callq -85 <_fin> +100000e79: 48 83 7d f8 01 cmpq $1, -8(%rbp) +100000e7e: 75 0c jne 12 <_fib+0x3a> +100000e80: 48 8b 45 e8 movq -24(%rbp), %rax +100000e84: 48 89 c7 movq %rax, %rdi +100000e87: e8 98 ff ff ff callq -104 <_fin> +100000e8c: 48 8b 55 f0 movq -16(%rbp), %rdx +100000e90: 48 8b 45 e8 movq -24(%rbp), %rax +100000e94: 48 01 c2 addq %rax, %rdx +100000e97: 48 8b 45 e8 movq -24(%rbp), %rax +100000e9b: 48 01 c2 addq %rax, %rdx +100000e9e: 48 8b 4d f0 movq -16(%rbp), %rcx +100000ea2: 48 8b 45 e8 movq -24(%rbp), %rax +100000ea6: 48 01 c1 addq %rax, %rcx +100000ea9: 48 8b 45 f8 movq -8(%rbp), %rax +100000ead: 48 83 e8 02 subq $2, %rax +100000eb1: 48 89 ce movq %rcx, %rsi +100000eb4: 48 89 c7 movq %rax, %rdi +100000eb7: e8 96 ff ff ff callq -106 <_fib> +100000ebc: 90 nop +100000ebd: c9 leave +100000ebe: c3 retq diff -r 0425278b683b -r c28e8156a37b Paper/src/cbc/cbc.txt --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/cbc/cbc.txt Fri Jan 20 13:40:03 2023 +0900 @@ -0,0 +1,32 @@ +0000000100000e3a _fib: +100000e3a: 55 pushq %rbp +100000e3b: 48 89 e5 movq %rsp, %rbp +100000e3e: 48 89 7d f8 movq %rdi, -8(%rbp) +100000e42: 48 89 75 f0 movq %rsi, -16(%rbp) +100000e46: 48 89 55 e8 movq %rdx, -24(%rbp) +100000e4a: 48 83 7d f8 00 cmpq $0, -8(%rbp) +100000e4f: 75 0d jne 13 <_fib+0x24> +100000e51: 48 8b 45 f0 movq -16(%rbp), %rax +100000e55: 48 89 c7 movq %rax, %rdi +100000e58: 5d popq %rbp +100000e59: e9 b5 ff ff ff jmp -75 <_fin> +100000e5e: 48 83 7d f8 01 cmpq $1, -8(%rbp) +100000e63: 75 0d jne 13 <_fib+0x38> +100000e65: 48 8b 45 e8 movq -24(%rbp), %rax +100000e69: 48 89 c7 movq %rax, %rdi +100000e6c: 5d popq %rbp +100000e6d: e9 a1 ff ff ff jmp -95 <_fin> +100000e72: 48 8b 55 f0 movq -16(%rbp), %rdx +100000e76: 48 8b 45 e8 movq -24(%rbp), %rax +100000e7a: 48 01 c2 addq %rax, %rdx +100000e7d: 48 8b 45 e8 movq -24(%rbp), %rax +100000e81: 48 01 c2 addq %rax, %rdx +100000e84: 48 8b 4d f0 movq -16(%rbp), %rcx +100000e88: 48 8b 45 e8 movq -24(%rbp), %rax +100000e8c: 48 01 c1 addq %rax, %rcx +100000e8f: 48 8b 45 f8 movq -8(%rbp), %rax +100000e93: 48 83 e8 02 subq $2, %rax +100000e97: 48 89 ce movq %rcx, %rsi +100000e9a: 48 89 c7 movq %rax, %rdi +100000e9d: 5d popq %rbp +100000e9e: eb 9a jmp -102 <_fib> diff -r 0425278b683b -r c28e8156a37b Paper/src/cbc/fib Binary file Paper/src/cbc/fib has changed diff -r 0425278b683b -r c28e8156a37b Paper/src/cbc/fib.c --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/cbc/fib.c Fri Jan 20 13:40:03 2023 +0900 @@ -0,0 +1,20 @@ +#include +#include + + +void fin(unsigned long long n){ + printf("%lld", n); + exit(0); +} + +void fib(unsigned long long n, unsigned long long a, unsigned long long b){ + if (n==0) fin(a); + if (n==1) fin(b); + fib(n-2, a+b, a+b+b); +} + +int main(int argc, char *argv[]){ + unsigned long long n=atoll(argv[1]); + fib(n,0,1); +} + diff -r 0425278b683b -r c28e8156a37b Paper/src/cbc/fib.cbc --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/cbc/fib.cbc Fri Jan 20 13:40:03 2023 +0900 @@ -0,0 +1,19 @@ +#include +#include + + +__code fin(unsigned long long n){ + printf("%lld", n); +} + +__code fib(unsigned long long n, unsigned long long a, unsigned long long b){ + if (n==0) goto fin(a); + if (n==1) goto fin(b); + goto fib(n-2, a+b, a+b+b); +} + +int main(int argc, char *argv[]){ + unsigned long long n = atoll(argv[1]); + goto fib(n,0,1); +} + diff -r 0425278b683b -r c28e8156a37b Paper/src/cbc/fib.out Binary file Paper/src/cbc/fib.out has changed diff -r 0425278b683b -r c28e8156a37b Paper/src/escape_agda.rb --- a/Paper/src/escape_agda.rb Thu Jan 12 20:31:09 2023 +0900 +++ b/Paper/src/escape_agda.rb Fri Jan 20 13:40:03 2023 +0900 @@ -14,6 +14,8 @@ '⟨' => 'langle', '⟩' => 'rangle', '₁' => 'text{1}', + '₂' => 'text{2}', + '₃' => 'text{3}', 'ℕ' => 'mathbb{N}', '∎' => 'blacksquare', 'λ' => 'lambda', @@ -22,6 +24,8 @@ '¬' => 'neg', '≤' => 'leq', '⊥' => 'bot', + "'" => "prime", + '⊤' => 'top' } code = File.read(FileName) diff -r 0425278b683b -r c28e8156a37b Paper/src/while_loop_verif/init_cg.agda.replaced --- a/Paper/src/while_loop_verif/init_cg.agda.replaced Thu Jan 12 20:31:09 2023 +0900 +++ b/Paper/src/while_loop_verif/init_cg.agda.replaced Fri Jan 20 13:40:03 2023 +0900 @@ -1,5 +1,5 @@ -whileTest' : {l : Level} {t : Set l} !$\rightarrow$! {c10 : !$\mathbb{N}$! } !$\rightarrow$! (Code : (env : Env) !$\rightarrow$! ((vari env) !$\equiv$! 0) /\ ((varn env) !$\equiv$! c10) !$\rightarrow$! t) !$\rightarrow$! t -whileTest' {_} {_} {c10} next = next env proof2 +whileTest!$\prime$! : {l : Level} {t : Set l} !$\rightarrow$! {c10 : !$\mathbb{N}$! } !$\rightarrow$! (Code : (env : Env) !$\rightarrow$! ((vari env) !$\equiv$! 0) /\ ((varn env) !$\equiv$! c10) !$\rightarrow$! t) !$\rightarrow$! t +whileTest!$\prime$! {_} {_} {c10} next = next env proof2 where env : Env env = record {vari = 0 ; varn = c10} diff -r 0425278b683b -r c28e8156a37b Paper/src/while_loop_verif/verif.agda.replaced --- a/Paper/src/while_loop_verif/verif.agda.replaced Thu Jan 12 20:31:09 2023 +0900 +++ b/Paper/src/while_loop_verif/verif.agda.replaced Fri Jan 20 13:40:03 2023 +0900 @@ -1,4 +1,4 @@ -proofGearsTermS : {c10 : !$\mathbb{N}$! } !$\rightarrow$! ⊤ -proofGearsTermS {c10} = whileTest' {_} {_} {c10} (!$\lambda$! n p !$\rightarrow$! conversion1 n p (!$\lambda$! n1 p1 !$\rightarrow$! +proofGearsTermS : {c10 : !$\mathbb{N}$! } !$\rightarrow$! !$\top$! +proofGearsTermS {c10} = whileTest!$\prime$! {_} {_} {c10} (!$\lambda$! n p !$\rightarrow$! conversion1 n p (!$\lambda$! n1 p1 !$\rightarrow$! TerminatingLoopS Env (!$\lambda$! env !$\rightarrow$! varn env) (!$\lambda$! n2 p2 loop !$\rightarrow$! whileLoopSeg {_} {_} {c10} n2 p2 loop (!$\lambda$! ne pe !$\rightarrow$! whileTestSpec1 c10 ne pe)) n1 p1 )) \ No newline at end of file diff -r 0425278b683b -r c28e8156a37b Paper/src/while_loop_verif/verif_term.agda.replaced --- a/Paper/src/while_loop_verif/verif_term.agda.replaced Thu Jan 12 20:31:09 2023 +0900 +++ b/Paper/src/while_loop_verif/verif_term.agda.replaced Fri Jan 20 13:40:03 2023 +0900 @@ -1,5 +1,5 @@ -whileTestSpec1 : (c10 : !$\mathbb{N}$!) !$\rightarrow$! (e1 : Env ) !$\rightarrow$! vari e1 !$\equiv$! c10 !$\rightarrow$! ⊤ +whileTestSpec1 : (c10 : !$\mathbb{N}$!) !$\rightarrow$! (e1 : Env ) !$\rightarrow$! vari e1 !$\equiv$! c10 !$\rightarrow$! !$\top$! whileTestSpec1 _ _ x = tt -proofGears : {c10 : !$\mathbb{N}$! } !$\rightarrow$! ⊤ -proofGears {c10} = whileTest' {_} {_} {c10} (!$\lambda$! n p1 !$\rightarrow$! conversion1 n p1 (!$\lambda$! n1 p2 !$\rightarrow$! whileLoop' n1 p2 (!$\lambda$! n2 p3 !$\rightarrow$! whileTestSpec1 c10 n2 p3 ))) \ No newline at end of file +proofGears : {c10 : !$\mathbb{N}$! } !$\rightarrow$! !$\top$! +proofGears {c10} = whileTest!$\prime$! {_} {_} {c10} (!$\lambda$! n p1 !$\rightarrow$! conversion1 n p1 (!$\lambda$! n1 p2 !$\rightarrow$! whileLoop!$\prime$! n1 p2 (!$\lambda$! n2 p3 !$\rightarrow$! whileTestSpec1 c10 n2 p3 ))) \ No newline at end of file diff -r 0425278b683b -r c28e8156a37b Paper/src/while_loop_verif/while_loop.agda.replaced --- a/Paper/src/while_loop_verif/while_loop.agda.replaced Thu Jan 12 20:31:09 2023 +0900 +++ b/Paper/src/while_loop_verif/while_loop.agda.replaced Fri Jan 20 13:40:03 2023 +0900 @@ -1,24 +1,24 @@ {-# TERMINATING #-} -whileLoop' : {l : Level} {t : Set l} !$\rightarrow$! (env : Env) !$\rightarrow$! {c10 : !$\mathbb{N}$! } !$\rightarrow$! ((varn env) + (vari env) !$\equiv$! c10) +whileLoop!$\prime$! : {l : Level} {t : Set l} !$\rightarrow$! (env : Env) !$\rightarrow$! {c10 : !$\mathbb{N}$! } !$\rightarrow$! ((varn env) + (vari env) !$\equiv$! c10) !$\rightarrow$! (Code : (e1 : Env )!$\rightarrow$! vari e1 !$\equiv$! c10 !$\rightarrow$! t) !$\rightarrow$! t -whileLoop' env proof next with ( suc zero !$\leq$!? (varn env) ) -whileLoop' env {c10} proof next | no p = next env ( begin +whileLoop!$\prime$! env proof next with ( suc zero !$\leq$!? (varn env) ) +whileLoop!$\prime$! env {c10} proof next | no p = next env ( begin vari env !$\equiv$!!$\langle$! refl !$\rangle$! 0 + vari env !$\equiv$!!$\langle$! cong (!$\lambda$! k !$\rightarrow$! k + vari env) (sym (lemma1 p )) !$\rangle$! varn env + vari env !$\equiv$!!$\langle$! proof !$\rangle$! c10 !$\blacksquare$! ) where open !$\equiv$!-Reasoning -whileLoop' env {c10} proof next | yes p = whileLoop' env1 (proof3 p ) next where +whileLoop!$\prime$! env {c10} proof next | yes p = whileLoop!$\prime$! env1 (proof3 p ) next where env1 = record {varn = (varn env) - 1 ; vari = (vari env) + 1} 1<0 : 1 !$\leq$! zero !$\rightarrow$! !$\bot$! 1<0 () proof3 : (suc zero !$\leq$! (varn env)) !$\rightarrow$! varn env1 + vari env1 !$\equiv$! c10 proof3 (s!$\leq$!s lt) with varn env proof3 (s!$\leq$!s z!$\leq$!n) | zero = !$\bot$!-elim (1<0 p) - proof3 (s!$\leq$!s (z!$\leq$!n {n'}) ) | suc n = let open !$\equiv$!-Reasoning in begin - n' + (vari env + 1) !$\equiv$!!$\langle$! cong ( !$\lambda$! z !$\rightarrow$! n' + z ) ( +-sym {vari env} {1} ) !$\rangle$! - n' + (1 + vari env ) !$\equiv$!!$\langle$! sym ( +-assoc (n') 1 (vari env) ) !$\rangle$! - (n' + 1) + vari env !$\equiv$!!$\langle$! cong ( !$\lambda$! z !$\rightarrow$! z + vari env ) +1!$\equiv$!suc !$\rangle$! - (suc n' ) + vari env !$\equiv$!!$\langle$!!$\rangle$! + proof3 (s!$\leq$!s (z!$\leq$!n {n!$\prime$!}) ) | suc n = let open !$\equiv$!-Reasoning in begin + n!$\prime$! + (vari env + 1) !$\equiv$!!$\langle$! cong ( !$\lambda$! z !$\rightarrow$! n!$\prime$! + z ) ( +-sym {vari env} {1} ) !$\rangle$! + n!$\prime$! + (1 + vari env ) !$\equiv$!!$\langle$! sym ( +-assoc (n!$\prime$!) 1 (vari env) ) !$\rangle$! + (n!$\prime$! + 1) + vari env !$\equiv$!!$\langle$! cong ( !$\lambda$! z !$\rightarrow$! z + vari env ) +1!$\equiv$!suc !$\rangle$! + (suc n!$\prime$! ) + vari env !$\equiv$!!$\langle$!!$\rangle$! varn env + vari env !$\equiv$!!$\langle$! proof !$\rangle$! c10 !$\blacksquare$! \ No newline at end of file diff -r 0425278b683b -r c28e8156a37b Paper/tex/agda.tex --- a/Paper/tex/agda.tex Thu Jan 12 20:31:09 2023 +0900 +++ b/Paper/tex/agda.tex Fri Jan 20 13:40:03 2023 +0900 @@ -1,16 +1,104 @@ -\chapter{定理証明支援器としての Agda} +\chapter{定理証明支援系言語 Agda} Agda \cite{agda-wiki} \cite{Stump:2016:VFP:2841316} は純粋関数型言語である． Agda は依存型という型システムを持ち，型を第一級オブジェクトとして扱う． + +本章ではAgdaの基本とAgdaによる定理証明の方法について述べる。 + +\section{Agdaの基本} +Agda の記述ではインデントが意味を持ち，スペースの有無もチェックされる． +コメントは \verb/-- comment/ か \verb/{-- comment --}/ のように記述される． +また，\verb/_/でそこに入りうるすべての値を示すことができ， +\verb/?/でそこに入る値や型を不明瞭なままにしておくことができる． + +%% データについて +Agda では型をデータや関数に記述する必要がある． +Agda における型指定は \verb/:/ を用いて \verb/name : type/ のように記述する． +このとき \verb/name/ に 空白があってはいけない． +データ型は，代数的なデータ構造で，その定義には \verb/data/ キーワードを用いる． +\verb/data/ キーワードの後に \verb/data/ の名前と，型， \verb/where/ 句を書きインデントを深くし， +値にコンストラクタとその型を列挙する． + +Code \ref{agda-nat}は自然数の型である $\mathbb{N}$ (Natural Number)を例である． + +\lstinputlisting[label=agda-nat, caption=自然数を表すデータ型 Nat の定義] {src/nat.agda.replaced} + +\verb/Nat/ では \verb/zero/ と \verb/suc/ の2つのコンストラクタを持つデータ型である． +\verb/suc/ は $\mathbb{N}$ を受け取って $\mathbb{N}$ を表す再帰的なデータになっており， +\verb/suc/ を連ねることで自然数全体を表現することができる． + +$\mathbb{N}$ 自身の型は \verb/Set/ であり，これは Agda が組み込みで持つ「型集合の型」である． +\verb/Set/ は階層構造を持ち，型集合の集合の型を指定するには \verb/Set1/ と書く． +%% \verb/Level/ を用いることで異なる \verb/Set/ を表現できる． + +Agda には C 言語における構造体に相当するレコード型というデータも存在する， +例えば \verb/x/ と \verb/y/ の二つの自然数からなるレコード \verb/Point/ を定義する．Code \ref{agda-record}のようになる． +\lstinputlisting[label=agda-record, caption=Agdaにおけるレコード型の定義] {src/env.agda.replaced} +レコードを構築する際は \verb/record/ キーワード後の \verb/{}/ の内部に \verb/FieldName = value/ の形で値を列挙する． +複数の値を列挙するには \verb/;/ で区切る必要がある． + +%% 関数について +Agda での関数は型の定義と，関数の定義をする必要がある． +関数の型はデータと同様に \verb/:/ を用いて \verb/name : type/ に記述するが，入力を受け取り出力返す型として記述される．$\rightarrow$ ， または\verb/→/ を用いて \verb/input → output/ のように記述される． +また，\verb/_+_/のように関数名で\verb/_/を使用すると引数がその位置にあることを意味し，中間記法で関数を定義することもできる． +関数の定義は型の定義より下の行に，\verb/=/ を使い \verb/name input = output/ のように記述される． + +例えば引数が型 \verb/A/ で返り値が型 \verb/B/ の関数は \verb/A → B/ のように書くことができる． +また，複数の引数を取る関数の型は \verb/A → A → B/ のように書ける． +例として任意の自然数$\mathbb{N}$を受け取り，\verb/+1/した値を返す関数はCode \ref{agda-function}のように定義できる． +\lstinputlisting[label=agda-function, caption=Agda における関数定義] {src/agda-func.agda.replaced} + + +引数は変数名で受けることもでき，具体的なコンストラクタを指定することでそのコンストラクタが渡された時の挙動を定義できる． +これはパターンマッチと呼ばれ，コンストラクタで case 文を行なっているようなものである． +例として自然数$\mathbb{N}$の加算を関数で書くとCode \ref{agda-plus}のようになる． + +\lstinputlisting[label=agda-plus, caption=自然数での加算の定義] {src/agda-plus.agda.replaced} +%% \lstinputlisting[label=agda-not, caption=Agdaにおける関数 not の定義] {src/AgdaNot.agda.replaced} + +パターンマッチでは全てのコンストラクタのパターンを含む必要がある． +例えば，自然数$\mathbb{N}$を受け取る関数では \verb/zero/ と \verb/suc/ の2つのパターンが存在する必要がある． +なお，コンストラクタをいくつか指定した後に変数で受けることもでき，その変数では指定されたもの以外を受けることができる． +例えばCode \ref{agda-pattern}の減算では初めのパターンで2つ目の引数が\verb/zero/のすべてのパターンが入る． + + +\lstinputlisting[label=agda-pattern, caption=自然数の減算によるパターンマッチの例] {src/agda-pattern.agda.replaced} + +Agda には$\lambda$計算が存在している．$\lambda$計算とは関数内で生成できる無名の関数であり， +\verb/\arg1 arg2 → function/ または $\lambda$\verb/arg1 arg2 → function/ のように書くことができる． +Code \ref{agda-function} で例とした \verb/+1/ をラムダ計算で書くとCode \ref{agda-lambda}の\verb/$\lambda$+1/ように書くことができる．この二つの関数は同一の動作をする． + +\lstinputlisting[label=agda-lambda, caption=Agda におけるラムダ計算] {src/AgdaLambda.agda.replaced} + +Agda では特定の関数内のみで利用できる関数を \verb/where/ 句で記述できる． +スコープは \verb/where/句が存在する関数内部のみであるため，名前空間が汚染させることも無い． +例えば自然数3つを取ってそれぞれ3倍して加算する関数 \verb/f/ を定義するとき， \verb/where/ を使うとリストCode \ref{agda-where} のように書ける． +これは \verb/f'/ と同様の動作をする． +\verb/where/ 句は利用したい関数の末尾にインデント付きで \verb/where/ キーワードを記述し，改行の後インデントをして関数内部で利用する関数を定義する． + +\lstinputlisting[label=agda-where, caption=Agda における where 句] {src/AgdaWhere.agda.replaced} + +また Agda では停止性の検出機能が存在し，プログラム中に停止しない記述が存在するとコンパイル時にエラーが出る． +\verb/{-# TERMINATING #-}/のタグを付けると停止しないプログラムをコンパイルすることができるがあまり望ましくない． +Code \ref{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 を実行するため停止する． + +\lstinputlisting[label=term, caption=停止しない関数 loop，停止する関数 stop] {src/termination.agda.replaced} + +このように再帰的な定義の関数が停止するときは，何らかの値が減少する必要がある． + + +\section{Agdaによる定理証明} Agda での証明では関数の記述と同様の形で型部分に証明すべき論理式， $\lambda$ 項部分にそれを満たす証明を書くことで証明を行うことが可能である． -証明の例として Code Code \ref{proof} を見る． +証明の例として \coderef{proof} を見る． ここでの \verb/+zero/ は右から \verb/zero/ を足しても ≡ の両辺は等しいことを証明している． これは，引数として受けている \verb/y/ が \verb/Nat/ なので， \verb/zero/ の時と \verb/suc y/ の二つの場合を証明する必要がある． -\lstinputlisting[caption=等式変形の例,label=proof]{src/zero.agda.replaced} +\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$ が成り立つという -Code \ref{cong}の \verb/cong/ を使って，y の値を 1 減らしたのち，再帰的に \verb/+zero y/ +\coderef{cong}の \verb/cong/ を使って，y の値を 1 減らしたのち，再帰的に \verb/+zero y/ を用いて証明している． -\lstinputlisting[caption=cong,label=cong]{src/cong.agda.replaced} +\lstinputlisting[caption=congによる等式変換の例,label=code:cong]{src/cong.agda.replaced} %% \begin{lstlisting}[caption=等式変形の例,label=proof] %% +zero : { y : ℕ } → y + zero ≡ y @@ -25,11 +113,11 @@ ここでは \verb/rewrite/ と ≡\verb/-Reasoning/ の構文を説明するとともに，等式を変形する構文の例として加算の交換則について示す． \verb/rewrite/ では 関数の \verb/=/ 前に \verb/rewrite 変形規則/ の形で記述し，複数の規則を使う場合は \verb/rewrite/ 変形規則1 \verb/|/ 変形規則2 のように \verb/|/を用いて記述する． -Code \ref{agda-term-post} にある \verb/+-comm/ で \verb/x/ が \verb/zero/ のパターンが良い例である． +\coderef{agda-term-post} にある \verb/+-comm/ で \verb/x/ が \verb/zero/ のパターンが良い例である． ここでは，\verb/+zero/ を利用し， \verb/zero + y/ を \verb/y/ に変形することで $y \equiv y$となり，左右の項が等しいことを示す \verb/refl/ になっている． -\lstinputlisting[caption=等式変形の例3/3,label=agda-term-post]{src/agda-term3.agda.replaced} -Code \ref{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/ を用いて示した． +\lstinputlisting[caption=等式変形の例3/3,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/ が示せた． Agda ではこのような形で等式を変形しながら証明を行う事ができる． diff -r 0425278b683b -r c28e8156a37b Paper/tex/cbc.tex --- a/Paper/tex/cbc.tex Thu Jan 12 20:31:09 2023 +0900 +++ b/Paper/tex/cbc.tex Fri Jan 20 13:40:03 2023 +0900 @@ -13,11 +13,53 @@ したがって，Code Gear に Deta Gear を与え，それをもとに処理を行い， 出力として Data Gear を返し，また次の Code Gearに遷移していく流れとなる． -他のプログラミング言語とは違い， -Code Gear が　暗黙の環境を持たず，受け取った Data Gear のみを -もとに処理をすること， -さらに Code Gear 単位で処理が完結していることから， -検証に適したプログラミング言語であると言える． +本章ではCbCの概要について説明する。 + +\section{Code Gear / Data Gear} +CbCでは、検証しやすいプログラムの単位として DataGear と CodeGear という単位を用いる。 + +CodeGear はプログラムの処理そのものであり、一般的なプログラム言語における関数と同じ役割である。 +DataGear は CodeGear で扱うデータの単位であり、処理に必要なデータである。 +CodeGear の入力となる DataGear を Input DataGear と呼び、出力は Output DataGear と呼ぶ。 + +CodeGear 間の移動は継続を用いて行われる。 +継続は関数呼び出しとは異なり、呼び出した後に元のコードに戻れず、次の CodeGear へ継続を行う。 +これは、関数型プログラミングでは末尾再帰をしていることと同義である。 + + +\section{CbC と C言語の違い} +同じ仕様でCbCとC言語で実装した際の違いを、実際のコードを元に比較する。 +比較するにあたり、再起処理が含まれるコードの例として、 +フィボナッチ数列の n 番目を求めるコードを挙げる。 +C言語で記述したものが\coderef{fib_c}。CbCで記述したものが\coderef{fib_cbc}になる。 +CbCは実行を継続するため、 return を行えない。そのためC言語での実装も return を書 +かず関数呼び出しを行い、最後にexitをして実行終了するように記述している。 + +\lstinputlisting[label=code:fib_c, caption=C言語で記述した フィボナッチ数列の n 番目 +を求めるコード, firstline=5] {src/cbc/fib.c} +\lstinputlisting[label=code:fib_cbc, caption=CbCで記述した フィボナッチ数列の n 番目 +を求めるコード, firstline=5] {src/cbc/fib.cbc} + +軽量実装になっているのか、上記のコードをアセンブラ変換した結果を見て確認する。 +全てを記載すると長くなるので、アセンブラ変換した際のfib関数のみを記載する。 +C言語で記述した\coderef{fib_c}をアセンブラ変換した結果が\coderef{c-ass}。 +CbCで記述した\coderef{fib_cbc}をアセンブラ変換した結果が\coderef{cbc-ass}になる。 + +比較すると、fib 関数の内部で再度 fib 関数を呼び出す際、 +C言語で実装した\coderef{c-ass}の30行目では callq で fib 関数を呼び出している。 +対して CbC で実装した\coderef{cbc-ass}の32行目では、 jmp により fib 関数に移動 +している。 + +\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 Code Gear / Meta Data Gear} +Meta DataGear は CbC 上のメタ計算で扱われる DataGear である。例えば stub +CodeGear では Context と呼ばれる接続可能な CodeGear、DataGear のリストや、DataGear +のメモリ空間等を持った Meta DataGear を扱っている。 また，プログラムを記述する際は，ノーマルレベルの計算の他に，メモリ管理，スレッド管理，資源管理等を記述しなければならない処理が存在する． これらの計算はノーマルレベルの計算と区別してメタ計算と呼ぶ． @@ -30,9 +72,8 @@ \begin{figure}[htpb] \begin{center} - \scalebox{0.35}{\includegraphics{fig/cbc_codegear.pdf}} + \scalebox{0.65}{\includegraphics{fig/cbc_codegear.pdf}} \end{center} \caption{メタ計算を可視化した CodeGear と DataGear} \label{fig:meta-cgdg} \end{figure} -