Mercurial > hg > Papers > 2020 > soto-midterm

comparison tex/agda.tex @ 7:acad18934981

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add description of rbtree
author soto@cr.ie.u-ryukyu.ac.jp
date Mon, 14 Sep 2020 05:41:23 +0900
parents 4bf00f7ba825
children 27a6616b6683
comparison
equal deleted inserted replaced
6:4bf00f7ba825 7:acad18934981
7 7
8 \subsection{プログラムの読み方} 8 \subsection{プログラムの読み方}
9 以下は Agda プログラムの一例となる。 9 以下は Agda プログラムの一例となる。
10 本節では以下のコードを説明することにより、Agda プログラムについて理解を深めることにより、 10 本節では以下のコードを説明することにより、Agda プログラムについて理解を深めることにより、
11 後述する Agda コードの理解を容易にすることを目的としている。 11 後述する Agda コードの理解を容易にすることを目的としている。
12
13 基本事項として、ℕ というのは自然数 (Natulal Number) のことである。
14 また - (ハイフン) が2つ連続して並んでいる部分はコメントアウトであり、
15 ここでは関数を実行した際の例を記述している。
16 したがって、この関数は2つの自然数を受け取って足す関数であることが推測できる。
17
12 \lstinputlisting[label=plus, caption=plus] {src/agda/plus.agda} 18 \lstinputlisting[label=plus, caption=plus] {src/agda/plus.agda}
13 19
14 \begin{itemize} 20 この関数の定義部分の説明をする。コードの1行目に : (セミコロン)がある。
15 \item 基本事項 21 この : の前が関数名になり、その後ろがその関数の定義となる。
16 \begin{itemize} 22 : 以降の (x y : ℕ ) は関数は x, y の自然数2つを受けとるという意味になる。
17 \item 23 → 以降は関数が返す型を記述している。
18 ℕ というのは自然数 (Natulal Number) のことである。 24 まとめると、この関数 plus は、型が自然数である2つの変数が x, y を受け取り、
19 また、- (ハイフン) が2つ連続して並んでいる部分はコメントアウトであり、 25 自然数を返すという定義になる。
20 ここでは関数を実行した際の例を記述している。 26
21 したがって、この関数は2つの自然数を受け取って足す関数であることが推測できる。 27 実装部分の説明をする。
22 \end{itemize} 28 関数の定義をしたコードの直下で実装を行うのが常である。
23 \item 定義部分 29 関数名を記述した後に引数を記述して受け取り、= (イコール) 以降で
24 \begin{itemize} 30 引数に対応した実装をする。
25 \item 31
26 コードの1行目に : (セミコロン)がある。 32 今回の場合 plus x zero であれば +0 である為、そのまま x を返す。
27 この : の前が関数名になり、その後ろがその関数の定義となる。\\ 33 実装2行目の方で受け取った y の値を減らし、x の値を増やして再び plus の関数に
28 : の後ろの (x y : ℕ ) は関数は x, y の自然数2つを受けとる。 34 遷移している。
29 という意味になる。 35 受け取った y を +1 されていたとして y の値を減らしている。
30 → の後ろは関数が返す型を記述している。 36
31 まとめると、この関数 plus は、型が自然数である2つの変数が x, y を受け取り、 37 関数の実装全体をまとめると、x と y の値を足す為に y から x に数値を1つずつ渡す。
32 自然数を返すという定義になる。 38 y が 0 になった際に計算が終了となっている。
33 \end{itemize} 39 指折りでの足し算を実装していると捉えても良い
34 \item 実装部分
35 \begin{itemize}
36 \item
37 関数の定義をしたコードの直下で実装を行うのが常である。
38 関数名を記述した後に引数を記述して受け取り、= (イコール) の後ろで
39 引数に対応し実装を作を記述していく。
40 今回の場合では、 plus x zero であれば +0 である為、そのまま x を返す。
41 2行目の方では受け取った y の値を減らし、x の値を増やして再び plus の関数に
42 遷移している。
43 受け取った y は+1されていたことにすることでyの値を減らしている。
44 実装部分もまとめると、x と y の値を足す為に、y から x に数値を1つずつ渡す。
45 y が 0 になった際に計算が終了となっている。
46 指折りでの足し算を実装していると捉えても良い
47 \end{itemize}
48 \end{itemize}
49 40
50 \subsection{Data 型} 41 \subsection{Data 型}
51 Deta 型とは分岐のことである。 42 Deta 型とは分岐のことである。
52 そのため、それぞれの動作について実装する必要がある。 43 そのため、それぞれの動作について実装する必要がある。
53 例として既出で Data 型である ℕ の実装を見てみる。 44 例として既出で Data 型である ℕ の実装を見てみる。