Mercurial > hg > Papers > 2020 > ryokka-master

comparison paper/agda.tex @ 9:95a5f8e76944

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix cbc_agda, cbc_hoare and Conclusion.tex
author ryokka
date Fri, 07 Feb 2020 21:40:26 +0900
parents b8ff2bd1a5af
children 831316a767e8
comparison
equal deleted inserted replaced
8:b8ff2bd1a5af 9:95a5f8e76944
29 インポートを行なう際、モジュール内部の関数を別名に変更するには \verb/as/ キーワードを用いる。 29 インポートを行なう際、モジュール内部の関数を別名に変更するには \verb/as/ キーワードを用いる。
30 他にも、モジュールから特定の関数のみをインポートする場合は \verb/using/ キーワード、 30 他にも、モジュールから特定の関数のみをインポートする場合は \verb/using/ キーワード、
31 関数名を、関数の名前を変える時は \verb/renaming/キーワードを、特定の関数のみを隠 31 関数名を、関数の名前を変える時は \verb/renaming/キーワードを、特定の関数のみを隠
32 す場合は \verb/hiding/ キーワードを用いる。 32 す場合は \verb/hiding/ キーワードを用いる。
33 なお、モジュールに存在する関数をトップレベルで用いる場合は \verb/open import/ キーワードを使うことで展開できる。 33 なお、モジュールに存在する関数をトップレベルで用いる場合は \verb/open import/ キーワードを使うことで展開できる。
34 モジュールをインポートする例を\coderef{src:agda-import}に示す。 34 モジュールをインポートする例を\coderef{agda-import}に示す。
35 35
36 \lstinputlisting[label=src:agda-import, caption=モジュールのインポートとオプション] {src/AgdaImport.agda.replaced} 36 \lstinputlisting[label=agda-import, caption=モジュールのインポートとオプション] {src/AgdaImport.agda.replaced}
37 37
38 38
39 \section{Agda のデータ} 39 \section{Agda のデータ}
40 Agda 型をデータや関数に記述する必要がある。 40 Agda 型をデータや関数に記述する必要がある。
41 Agda における型指定は \verb/:/ を用いて \verb/name : type/ のように記述する。 41 Agda における型指定は \verb/:/ を用いて \verb/name : type/ のように記述する。
42 データ型は、代数的なデータ構造で、その定義には \verb/data/ キーワードを用いる。 42 データ型は、代数的なデータ構造で、その定義には \verb/data/ キーワードを用いる。
43 \verb/data/ キーワードの後に \verb/data/ の名前と、型、 \verb/where/ 句を書きインデントを深くし、 43 \verb/data/ キーワードの後に \verb/data/ の名前と、型、 \verb/where/ 句を書きインデントを深くし、
44 値にコンストラクタとその型を列挙する。 44 値にコンストラクタとその型を列挙する。
45 45
46 \coderef{src:agda-nat}は自然数の型である $\mathbb{N}$ (Natural Number)を例である。 46 \coderef{agda-nat}は自然数の型である $\mathbb{N}$ (Natural Number)を例である。
47 47
48 \lstinputlisting[label=src:agda-nat, caption=自然数を表すデータ型 Nat の定義] {src/nat.agda.replaced} 48 \lstinputlisting[label=agda-nat, caption=自然数を表すデータ型 Nat の定義] {src/nat.agda.replaced}
49 49
50 \verb/Nat/ では \verb/zero/ と \verb/suc/ の2つのコンストラクタを持つデータ型である。 50 \verb/Nat/ では \verb/zero/ と \verb/suc/ の2つのコンストラクタを持つデータ型である。
51 \verb/suc/ は $\mathbb{N}$ を受け取って $\mathbb{N}$ を表す再帰的なデータになっており、 51 \verb/suc/ は $\mathbb{N}$ を受け取って $\mathbb{N}$ を表す再帰的なデータになっており、
52 \verb/suc/ を連ねることで自然数全体を表現することができる。 52 \verb/suc/ を連ねることで自然数全体を表現することができる。
53 53
54 $\mathbb{N}$ 自身の型は \verb/Set/ であり、これは Agda が組み込みで持つ「型集合の型」である。 54 $\mathbb{N}$ 自身の型は \verb/Set/ であり、これは Agda が組み込みで持つ「型集合の型」である。
55 \verb/Set/ は階層構造を持ち、型集合の集合の型を指定するには \verb/Set1/ と書く。 55 \verb/Set/ は階層構造を持ち、型集合の集合の型を指定するには \verb/Set1/ と書く。
56 %% \verb/Level/ を用いることで異なる \verb/Set/ を表現できる。 56 %% \verb/Level/ を用いることで異なる \verb/Set/ を表現できる。
57 57
58 Agda には C 言語における構造体に相当するレコード型というデータも存在する、 58 Agda には C 言語における構造体に相当するレコード型というデータも存在する、
59 例えば \verb/x/ と \verb/y/ の二つの自然数からなるレコード \verb/Point/ を定義する。\coderef{src:agda-record}のようになる。 59 例えば \verb/x/ と \verb/y/ の二つの自然数からなるレコード \verb/Point/ を定義する。\coderef{agda-record}のようになる。
60 \lstinputlisting[label=src:agda-record, caption=Agdaにおけるレコード型の定義] {src/AgdaRecord.agda.replaced} 60 \lstinputlisting[label=agda-record, caption=Agdaにおけるレコード型の定義] {src/AgdaRecord.agda.replaced}
61 レコードを構築する際は \verb/record/ キーワード後の \verb/{}/ の内部に \verb/FieldName = value/ の形で値を列挙する。 61 レコードを構築する際は \verb/record/ キーワード後の \verb/{}/ の内部に \verb/FieldName = value/ の形で値を列挙する。
62 複数の値を列挙するには \verb/;/ で区切る必要がある。 62 複数の値を列挙するには \verb/;/ で区切る必要がある。
63 63
64 64
65 \section{Agda の関数} 65 \section{Agda の関数}
68 関数の定義は型の定義より下の行に、\verb/=/ を使い \verb/name input = output/ のように記述される。 68 関数の定義は型の定義より下の行に、\verb/=/ を使い \verb/name input = output/ のように記述される。
69 69
70 例えば引数が型 \verb/A/ で返り値が型 \verb/B/ の関数は \verb/A → B/ のように書くことができる。 70 例えば引数が型 \verb/A/ で返り値が型 \verb/B/ の関数は \verb/A → B/ のように書くことができる。
71 また、複数の引数を取る関数の型は \verb/A → A → B/ のように書ける。 71 また、複数の引数を取る関数の型は \verb/A → A → B/ のように書ける。
72 この時の型は \verb/A → (A → B)/のように考えられる。 72 この時の型は \verb/A → (A → B)/のように考えられる。
73 %% 変数 \verb/x/ を取って true を返す関数 \verb/f/は\tabref{src:agda-function}のようになる。 73 %% 変数 \verb/x/ を取って true を返す関数 \verb/f/は\tabref{agda-function}のようになる。
74 例として任意の自然数$mathbb{N}$を受け取り、\verb/+1/した値を返す関数は\coderef{src:agda-function}のように定義できる。 74 例として任意の自然数$\mathbb{N}$を受け取り、\verb/+1/した値を返す関数は\coderef{agda-function}のように定義できる。
75 \lstinputlisting[label=src:agda-function, caption=Agda における関数定義] {src/agda-func.agda.replaced} 75 \lstinputlisting[label=agda-function, caption=Agda における関数定義] {src/agda-func.agda.replaced}
76 76
77 77
78 引数は変数名で受けることもでき、具体的なコンストラクタを指定することでそのコンストラクタが渡された時の挙動を定義できる。 78 引数は変数名で受けることもでき、具体的なコンストラクタを指定することでそのコンストラクタが渡された時の挙動を定義できる。
79 これはパターンマッチと呼ばれ、コンストラクタで case 文を行なっているようなものである。 79 これはパターンマッチと呼ばれ、コンストラクタで case 文を行なっているようなものである。
80 例として自然数$mathbb{N}$の加算を関数で書くと\coderef{agda-plus}のようになる。 80 例として自然数$\mathbb{N}$の加算を関数で書くと\coderef{agda-plus}のようになる。
81 81
82 \lstinputlisting[label=src:agda-plus, caption=自然数での加算の定義] {src/agda-plus.agda.replaced} 82 \lstinputlisting[label=agda-plus, caption=自然数での加算の定義] {src/agda-plus.agda.replaced}
83 %% \lstinputlisting[label=src:agda-not, caption=Agdaにおける関数 not の定義] {src/AgdaNot.agda.replaced} 83 %% \lstinputlisting[label=agda-not, caption=Agdaにおける関数 not の定義] {src/AgdaNot.agda.replaced}
84 \verb/_+_/のように関数名で\verb/_/を使用すると引数がその位置にあることを意味する。 84 \verb/_+_/のように関数名で\verb/_/を使用すると引数がその位置にあることを意味する。
85 85
86 パターンマッチでは全てのコンストラクタのパターンを含む必要がある。 86 パターンマッチでは全てのコンストラクタのパターンを含む必要がある。
87 例えば、自然数$mathbb{N}$を受け取る関数では \verb/zero/ と \verb/suc/ の2つのパターンが存在する必要がある。 87 例えば、自然数$\mathbb{N}$を受け取る関数では \verb/zero/ と \verb/suc/ の2つのパターンが存在する必要がある。
88 なお、コンストラクタをいくつか指定した後に変数で受けることもでき、その変数では指定されたもの以外を受けることができる。 88 なお、コンストラクタをいくつか指定した後に変数で受けることもでき、その変数では指定されたもの以外を受けることができる。
89 例えば\coderef{src:agda-pattern}の減算では初めのパターンで2つ目の引数が\verb/zero/のすべてのパターンが入る。 89 例えば\coderef{agda-pattern}の減算では初めのパターンで2つ目の引数が\verb/zero/のすべてのパターンが入る。
90 90
91 91
92 \lstinputlisting[label=src:agda-pattern, caption=自然数の減算によるパターンマッチの例] {src/agda-pattern.agda.replaced} 92 \lstinputlisting[label=agda-pattern, caption=自然数の減算によるパターンマッチの例] {src/agda-pattern.agda.replaced}
93 93
94 Agda には$\lambda$計算が存在している。$\lambda$計算とは関数内で生成できる無名の関数であり、 94 Agda には$\lambda$計算が存在している。$\lambda$計算とは関数内で生成できる無名の関数であり、
95 \verb/\arg1 arg2 → function/ のように書くことができる。 95 \verb/\arg1 arg2 → function/ または $\lambda$\verb/arg1 arg2 → function/ のように書くことができる。
96 \coderef{agda-function} で例とした \verb/+1/ をラムダ計算で書くと\coderef{src:agda-lambda}の\verb/$\lambda$+1/ように書くことができる。この二つの関数は同一の動作をする。 96 \coderef{agda-function} で例とした \verb/+1/ をラムダ計算で書くと\coderef{agda-lambda}の\verb/$\lambda$+1/ように書くことができる。この二つの関数は同一の動作をする。
97 97
98 \lstinputlisting[label=src:agda-lambda, caption=Agda におけるラムダ計算] {src/AgdaLambda.agda.replaced} 98 \lstinputlisting[label=agda-lambda, caption=Agda におけるラムダ計算] {src/AgdaLambda.agda.replaced}
99 99
100 Agda では特定の関数内のみで利用できる関数を \verb/where/ 句で記述できる。 100 Agda では特定の関数内のみで利用できる関数を \verb/where/ 句で記述できる。
101 スコープは \verb/where/句が存在する関数内部のみであるため、名前空間が汚染させることも無い。 101 スコープは \verb/where/句が存在する関数内部のみであるため、名前空間が汚染させることも無い。
102 例えば自然数3つを取ってそれぞれ3倍して加算する関数 \verb/f/ を定義するとき、 \verb/where/ を使うとリスト~\ref{src:agda-where} のように書ける。 102 例えば自然数3つを取ってそれぞれ3倍して加算する関数 \verb/f/ を定義するとき、 \verb/where/ を使うとリスト\coderef{agda-where} のように書ける。
103 これは \verb/f'/ と同様の動作をする。 103 これは \verb/f'/ と同様の動作をする。
104 \verb/where/ 句は利用したい関数の末尾にインデント付きで \verb/where/ キーワードを記述し、改行の後インデントをして関数内部で利用する関数を定義する。 104 \verb/where/ 句は利用したい関数の末尾にインデント付きで \verb/where/ キーワードを記述し、改行の後インデントをして関数内部で利用する関数を定義する。
105 105
106 \lstinputlisting[label=src:agda-where, caption=Agda における where 句] {src/AgdaWhere.agda.replaced} 106 \lstinputlisting[label=agda-where, caption=Agda における where 句] {src/AgdaWhere.agda.replaced}
107 107
108 108
109 \section{定理証明支援器としての Agda} 109 \section{定理証明支援器としての Agda}
110 Agda での証明では関数の記述と同様の形で型部分に証明すべき論理式、 $\lambda$ 項部分にそれを満たす証明を書くことで証明を行うことが可能である。 110 Agda での証明では関数の記述と同様の形で型部分に証明すべき論理式、 $\lambda$ 項部分にそれを満たす証明を書くことで証明を行うことが可能である。
111 証明の例として Code \coderef{proof} を見る。 111 証明の例として Code \coderef{proof} を見る。