Mercurial > hg > Papers > 2020 > soto-midterm

comparison tex/agda.tex @ 11:a8bc8c6b48bd default tip

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author soto@cr.ie.u-ryukyu.ac.jp
date Tue, 15 Sep 2020 07:06:29 +0900
parents 27a6616b6683
children
comparison
equal deleted inserted replaced
10:c162ca9b997e 11:a8bc8c6b48bd
4 ムを持ち、型を第一級オブジェクトとして扱うことが可能である。また、型システムは 4 ムを持ち、型を第一級オブジェクトとして扱うことが可能である。また、型システムは
5 Curry-Howard 同型対応により命題と型付きラムダ計算が一対一で対応するため Agda で 5 Curry-Howard 同型対応により命題と型付きラムダ計算が一対一で対応するため Agda で
6 は記述したプログラムを証明することができる。 6 は記述したプログラムを証明することができる。
7 7
8 \subsection{プログラムの読み方} 8 \subsection{プログラムの読み方}
9 以下は Agda プログラムの一例となる。 9 本節ではAgdaの基本事項について \coderef{plus} を例として解説する。
10 本節ではAgdaの基本事項について解説する。
11 10
12 基本事項として、ℕ というのは自然数 (Natulal Number) のことである。 11 基本事項として、$ \mathbb{N} $ というのは自然数 (Natulal Number) のことである。
13 また - (ハイフン) が2つ連続して並んでいる部分はコメントアウトであり、 12 また - (ハイフン) が2つ連続して並んでいる部分はコメントアウトであり、
14 ここでは関数を実行した際の例を記述している。 13 ここでは関数を実行した際の例を記述している。
15 したがって、この関数は2つの自然数を受け取って足す関数であることが推測できる。 14 したがって、これは2つの自然数を受け取って足す関数であることが推測できる。
16 15
17 \lstinputlisting[label=plus, caption=plus] {src/agda/plus.agda} 16 \lstinputlisting[label=plus, caption=plus] {src/agda/plus.agda}
18 17
19 この関数の定義部分の説明をする。コードの1行目に : (セミコロン)がある。 18 この関数の定義部分の説明をする。コードの1行目に : (セミコロン)がある。
20 この : の前が関数名になり、その後ろがその関数の定義となる。 19 この : の前が関数名になり、その後ろがその関数の定義となる。
21 : 以降の (x y : ℕ ) は関数は x, y の自然数2つを受けとるという意味になる。 20 : 以降の (x y : $ \mathbb{N} $) は関数は x, y の自然数2つを受けとるという意味になる。
22 → 以降は関数が返す型を記述している。 21 $ \rightarrow $ 以降は関数が返す型を記述している。
23 まとめると、この関数 plus は、型が自然数である2つの変数が x, y を受け取り、 22 まとめると、この関数 plus は、型が自然数である2つの変数が x, y を受け取り、
24 自然数を返すという定義になる。 23 自然数を返すという定義になる。
25 24
26 関数の定義をしたコードの直下で実装を行うのが常である。 25 関数の定義をしたコードの直下で実装を行うのが常である。
27 関数名を記述した後に引数を記述して受け取り、= (イコール) 以降で 26 関数名を記述した後に引数を記述して受け取り、= (イコール) 以降で
37 指折りでの足し算を実装していると捉えても良い。 36 指折りでの足し算を実装していると捉えても良い。
38 37
39 \subsection{Data 型} 38 \subsection{Data 型}
40 Deta 型とは分岐のことである。 39 Deta 型とは分岐のことである。
41 そのため、それぞれの動作について実装する必要がある。 40 そのため、それぞれの動作について実装する必要がある。
42 例として既出で Data 型である ℕ の実装を見てみる。 41 例として既出で Data 型である $ \mathbb{N} $ の実装を \coderef{Nat} に示す。
43 42
44 \lstinputlisting[label=Nat, caption=Nat] {src/agda/Nat.agda} 43 \lstinputlisting[label=Nat, caption=Nat] {src/agda/Nat.agda}
45 44
46 実装から、ℕ という型は zero と suc の2つのコンストラクタを持っていることが分かる。 45 実装から、$ \mathbb{N} $ という型は zero と suc の2つのコンストラクタを持っていることが分かる。
47 それぞれの仕様を見てみると、zeroは ℕ のみであるが、suc は (n : ℕ) → ℕ である。 46 それぞれの仕様を見てみると、zeroは $ \mathbb{N} $ のみであるが、suc は (n : $ \mathbb{N} $ ) $ \rightarrow \ \mathbb{N} $ である。
48 つまり、suc 自体の型は ℕ であるが、そこから ℕ に遷移するということである。 47 つまり、suc 自体の型は $ \mathbb{N} $ であるが、そこから $ \mathbb{N} $ に遷移するということである。
49 そのため、suc からは suc か zero に遷移する必要があり、また zero に遷移することで停止する。 48 そのため、suc からは suc か zero に遷移する必要があり、また zero に遷移することで停止する。
50 したがって、数値は zero に遷移するまでの suc が遷移した数によって決定される。 49 したがって、数値は zero に遷移するまでの suc が遷移した数によって決定される。
51 50
52 Data型にはそれぞれの動作について実装する必要があると述べたが、 51 Data型にはそれぞれの動作について実装する必要があると述べたが、
53 言い換えればパターンマッチをする必要があると言える。 52 言い換えればパターンマッチをする必要があると言える。
54 これは puls 関数で suc 同士の場合と、zeroが含まれる場合の両方を実装していることの説明となる。 53 これは puls 関数で suc 同士の場合と、zeroが含まれる場合の両方を実装していることの説明となる。
55 54
56
57
58 \subsection{Record 型} 55 \subsection{Record 型}
59 Record 型とはオブジェクトあるいは構造体ののようなものである。 56 Record 型とはオブジェクトあるいは構造体ののようなものである。
60 以下の関数は AND となる。p1で前方部分が取得でき、p2で後方部分が取得できる。 57 \coderef{And}は AND の関数となる。p1で前方部分が取得でき、p2で後方部分が取得できる。
61 58
62 \lstinputlisting[label=And, caption=And] {src/agda/And.agda} 59 \lstinputlisting[label=And, caption=And] {src/agda/And.agda}
63 60
64 また、Agda の関数定義では\_(アンダースコア)で囲むことで三項演算子を定義することができる。 61 また、Agda の関数定義では\_(アンダースコア)で囲むことで三項演算子を定義することができる。
65 62
66 これを使用して三段論法を定義することができる。 63 これを使用して三段論法を定義することができる。
67 定義は「AならばB」かつ「BならばC」なら「AならばC」となる。 64 定義は「AならばB」かつ「BならばC」なら「AならばC」となる。
68 コードを以下に示す。 65 \coderef{syllogism}を以下に示す。
69 66
70 \lstinputlisting[label=syllogism, caption=syllogism] {src/agda/syllogism.agda} 67 \lstinputlisting[label=syllogism, caption=syllogism] {src/agda/syllogism.agda}
71 68
72 コードの解説をすると、引数として x と a が関数に与えられている。 69 コードの解説をすると、引数として x と a が関数に与えられている。
73 引数 x の中身は((A → B) ∧ (B → C))、引数 a の中身は A である。 70 引数 x の中身は ((A $ \rightarrow $ B) ∧ (B $ \rightarrow $ C)) 、引数 a の中身は A である。
74 したがって、(\_∧\_.p1 x a) で (A → B) に A を与えて B を取得し、 71 したがって、(\_∧\_.p1 x a) で (A $ \rightarrow $ B) に A を与えて B を取得し、
75 \_∧\_.p2 x で (B → C) であるため、これに B を与えると C が取得できる。 72 \_∧\_.p2 x で (B $ \rightarrow $ C) であるため、これに B を与えると C が取得できる。
76 よって A を与えて C を取得することができたため、三段論法を定義できた。 73 よって A を与えて C を取得することができたため、三段論法を定義できた。
77 74
78 %\subsection{Agdaの基本操作}
79
80 %\subsection{定理証明支援器としての Agda}
81
82 %\subsectoin{}
83
84