Mercurial > hg > Papers > 2018 > ryokka-thesis

comparison final_main/chapter5.tex @ 7:28f900230c26

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add final_pre
author ryokka
date Mon, 19 Feb 2018 23:32:24 +0900
parents d927f6b3d2b3
children 9af6c3636ea0
comparison
equal deleted inserted replaced
6:d927f6b3d2b3 7:28f900230c26
28 などの性質がある。 28 などの性質がある。
29 29
30 本セクションでは「どのような状態の Stack でも、値を push した後 pop した値は直前 30 本セクションでは「どのような状態の Stack でも、値を push した後 pop した値は直前
31 に入れた値と一致する」という性質を証明する。 31 に入れた値と一致する」という性質を証明する。
32 32
33
33 % この証明では任意の Stack に2回 push したあと2回 pop すると push したものと同じ 34 % この証明では任意の Stack に2回 push したあと2回 pop すると push したものと同じ
34 % ものが受け取れることを 証明している。 35 % ものが受け取れることを 証明している。
35 36
36 まず始めに不定状態の Stack を定義する。ソースコード~\ref{src:agda-in-some-state} 37 まず始めに不定状態の Stack を定義する。ソースコード~\ref{src:agda-in-some-state}
37 の line1~2 で定義している stackInSomeState が不定状態の Stack である。 38 の stackInSomeState 型は中身の分からない抽象的な Stack を表現している。ソースコー
38 stackInSomeState 型は中身の分からない抽象的な Stack を作成している。ソースコー 39 ド~\ref{src:agda-in-some-state}の証明ではこのstackInSomeState に対して、 push を
39 ド~\ref{src:agda-in-some-state}の証明ではこのstackInSomeState に対して、 push を 40 2回行い、 pop2 をして取れたデータは push したデータと同じものになることを証明してい
40 2回行い、 pop2 をして取れたデータは push したデータと同じものになることを証明してい 41 る。
41 る。
42 42
43 \lstinputlisting[label=src:agda-in-some-state, caption=抽象的なStackの定義とpush$->$push$->$pop2 の証明]{src/AgdaStackSomeState.agda.replaced} 43 \lstinputlisting[label=src:agda-in-some-state, caption=抽象的なStackの定義とpush$->$push$->$pop2 の証明]{src/AgdaStackSomeState.agda.replaced}
44 44
45 % Agda でも継続を使った書き方で Interface 部分の実装を示した。 45 % Agda でも継続を使った書き方で Interface 部分の実装を示した。
46 46