Mercurial > hg > Papers > 2020 > ryokka-master

comparison paper/agda.tex @ 13:e8655e0264b8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix paper, slide
author ryokka
date Tue, 11 Feb 2020 02:31:26 +0900
parents 831316a767e8
children 046b2b20d6c7
comparison
equal deleted inserted replaced
12:bf3288c36d7e 13:e8655e0264b8
39 データ型は、代数的なデータ構造で、その定義には \verb/data/ キーワードを用いる。 39 データ型は、代数的なデータ構造で、その定義には \verb/data/ キーワードを用いる。
40 \verb/data/ キーワードの後に \verb/data/ の名前と、型、 \verb/where/ 句を書きインデントを深くし、 40 \verb/data/ キーワードの後に \verb/data/ の名前と、型、 \verb/where/ 句を書きインデントを深くし、
41 値にコンストラクタとその型を列挙する。 41 値にコンストラクタとその型を列挙する。
42 42
43 \coderef{agda-nat}は自然数の型である $\mathbb{N}$ (Natural Number)を例である。 43 \coderef{agda-nat}は自然数の型である $\mathbb{N}$ (Natural Number)を例である。
44 %%　Agda では $\mathbb{N}$ のような utf8 の文字を扱う事ができる。なんで？
45 %%
44 46
45 \lstinputlisting[label=agda-nat, caption=自然数を表すデータ型 Nat の定義] {src/nat.agda.replaced} 47 \lstinputlisting[label=agda-nat, caption=自然数を表すデータ型 Nat の定義] {src/nat.agda.replaced}
46 48
47 \verb/Nat/ では \verb/zero/ と \verb/suc/ の2つのコンストラクタを持つデータ型である。 49 \verb/Nat/ では \verb/zero/ と \verb/suc/ の2つのコンストラクタを持つデータ型である。
48 \verb/suc/ は $\mathbb{N}$ を受け取って $\mathbb{N}$ を表す再帰的なデータになっており、 50 \verb/suc/ は $\mathbb{N}$ を受け取って $\mathbb{N}$ を表す再帰的なデータになっており、
100 これは \verb/f'/ と同様の動作をする。 102 これは \verb/f'/ と同様の動作をする。
101 \verb/where/ 句は利用したい関数の末尾にインデント付きで \verb/where/ キーワードを記述し、改行の後インデントをして関数内部で利用する関数を定義する。 103 \verb/where/ 句は利用したい関数の末尾にインデント付きで \verb/where/ キーワードを記述し、改行の後インデントをして関数内部で利用する関数を定義する。
102 104
103 \lstinputlisting[label=agda-where, caption=Agda における where 句] {src/AgdaWhere.agda.replaced} 105 \lstinputlisting[label=agda-where, caption=Agda における where 句] {src/AgdaWhere.agda.replaced}
104 106
105 \section{Agda の関数での停止性} 107 また Agda では停止性の検出機能が存在し、プログラム中に停止しない記述が存在するとコンパイル時にエラーが出る。
106 Agda では停止性の検出機能が存在し、プログラム中に停止しない記述が存在するとコンパイル時にエラーが出る。
107 \verb/{-# TERMINATING #-}/のタグを付けると停止しないプログラムをコンパイルすることができるがあまり望ましくない。 108 \verb/{-# TERMINATING #-}/のタグを付けると停止しないプログラムをコンパイルすることができるがあまり望ましくない。
108 109 \coderef{term} で書かれた、\verb/loop/ と \verb/stop/ は任意の自然数を受け取り、0になるまでループして0を返す関数である。
109 ここでは停止する関数と停止しない関数の例\coderef{termination}を扱う。 110 \verb/loop/ では $\mathbb{N}$ の数を受け取り、 \verb/loop/ 自身を呼び出しながら 数を減らす関数 pred を呼んでいる。しかし、\verb/loop/の記述では関数が停止すると言えないため、定義するには\verb/{-# TERMINATING #-}/のタグが必要である。
110 %% \lstinputlisting[label=termination, caption=停止する関数、停止しない関数] {src/terminating.agda.replaced} 111 \verb/stop/ では自然数がパターンマッチで分けられ、\verb/zero/のときは \verb/zero/を返し、 \verb/suc n/ のときは \verb/suc/ を外した \verb/n/ で stop を実行するため停止する。
112
113 \lstinputlisting[label=term, caption=停止しない関数 loop、停止する関数 stop] {src/termination.agda.replaced}
111 114
112 このように再帰的な定義の関数が停止するときは、何らかの値が減少する必要がある。 115 このように再帰的な定義の関数が停止するときは、何らかの値が減少する必要がある。
113 116
114 117
115 \section{定理証明支援器としての Agda} 118 \section{定理証明支援器としての Agda}
116 Agda での証明では関数の記述と同様の形で型部分に証明すべき論理式、 $\lambda$ 項部分にそれを満たす証明を書くことで証明を行うことが可能である。 119 Agda での証明では関数の記述と同様の形で型部分に証明すべき論理式、 $\lambda$ 項部分にそれを満たす証明を書くことで証明を行うことが可能である。
117 証明の例として Code \coderef{proof} を見る。 120 証明の例として Code \coderef{proof} を見る。
118 ここでの \verb/+zero/ は右から \verb/zero/ を足しても $\equiv$ の両辺は等しいことを証明している。 121 ここでの \verb/+zero/ は右から \verb/zero/ を足しても $\equiv$ の両辺は等しいことを証明している。
119 これは、引数として受けている \verb/y/ が \verb/Nat/ なので、 \verb/zero/ の時と \verb/suc y/ の二つの場合を証明する必要がある。 122 これは、引数として受けている \verb/y/ が \verb/Nat/ なので、 \verb/zero/ の時と \verb/suc y/ の二つの場合を証明する必要がある。
120 123
121 \verb/y = zero/ の時は両辺が \verb/zero/ とできて、左右の項が等しいということを表す \verb/refl/ で証明することができる。 124 \verb/y = zero/ の時は $zero \equiv zero$ とできて、左右の項が等しいということを表す \verb/refl/ で証明することができる。
122 \verb/y = suc y/ の時は $x \equiv y$ の時 $fx \equiv fy$ が成り立つという \verb/cong/ を使って、y の値を 1 減らしたのちに再帰的に \verb/+zero y/ 125 \verb/y = suc y/ の時は $x \equiv y$ の時 $fx \equiv fy$ が成り立つという
126 \verb/cong/ を使って、y の値を 1 減らしたのち、再帰的に \verb/+zero y/
123 を用いて証明している。 127 を用いて証明している。
124 128
125 \lstinputlisting[caption=等式変形の例,label=proof]{src/zero.agda.replaced} 129 \lstinputlisting[caption=等式変形の例,label=proof]{src/zero.agda.replaced}
126 %% \begin{lstlisting}[caption=等式変形の例,label=proof] 130 %% \begin{lstlisting}[caption=等式変形の例,label=proof]
127 %% +zero : { y : ℕ } → y + zero ≡ y 131 %% +zero : { y : ℕ } → y + zero ≡ y
128 %% +zero {zero} = refl 132 %% +zero {zero} = refl
129 %% +zero {suc y} = cong ( λ x → suc x ) ( +zero {y} ) 133 %% +zero {suc y} = cong ( λ x → suc x ) ( +zero {y} )
134 %%
135 %% -- cong : ∀ (f : A → B) {x y} → x ≡ y → f x ≡ f y
136 %% -- cong f refl = refl
130 %% \end{lstlisting} 137 %% \end{lstlisting}
131 138
132 また、他にも $\lambda$ 項部分で等式を変形する構文がいくつか存在している。 139 また、他にも $\lambda$ 項部分で等式を変形する構文がいくつか存在している。
133 ここでは \verb/rewrite/ と $\equiv$\verb/-Reasoning/ の構文を説明するとともに、等式を変形する構文の例として加算の交換則について示す。 140 ここでは \verb/rewrite/ と $\equiv$\verb/-Reasoning/ の構文を説明するとともに、等式を変形する構文の例として加算の交換則について示す。
134 141