Mercurial > hg > Papers > 2020 > soto-midterm

comparison tex/agda.tex @ 8:27a6616b6683

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 Mon, 14 Sep 2020 19:58:10 +0900
parents acad18934981
children a8bc8c6b48bd
comparison
equal deleted inserted replaced
7:acad18934981 8:27a6616b6683
5 Curry-Howard 同型対応により命題と型付きラムダ計算が一対一で対応するため Agda で 5 Curry-Howard 同型対応により命題と型付きラムダ計算が一対一で対応するため Agda で
6 は記述したプログラムを証明することができる。 6 は記述したプログラムを証明することができる。
7 7
8 \subsection{プログラムの読み方} 8 \subsection{プログラムの読み方}
9 以下は Agda プログラムの一例となる。 9 以下は Agda プログラムの一例となる。
10 本節では以下のコードを説明することにより、Agda プログラムについて理解を深めることにより、 10 本節ではAgdaの基本事項について解説する。
11 後述する Agda コードの理解を容易にすることを目的としている。
12 11
13 基本事項として、ℕ というのは自然数 (Natulal Number) のことである。 12 基本事項として、ℕ というのは自然数 (Natulal Number) のことである。
14 また - (ハイフン) が2つ連続して並んでいる部分はコメントアウトであり、 13 また - (ハイフン) が2つ連続して並んでいる部分はコメントアウトであり、
15 ここでは関数を実行した際の例を記述している。 14 ここでは関数を実行した際の例を記述している。
16 したがって、この関数は2つの自然数を受け取って足す関数であることが推測できる。 15 したがって、この関数は2つの自然数を受け取って足す関数であることが推測できる。
22 : 以降の (x y : ℕ ) は関数は x, y の自然数2つを受けとるという意味になる。 21 : 以降の (x y : ℕ ) は関数は x, y の自然数2つを受けとるという意味になる。
23 → 以降は関数が返す型を記述している。 22 → 以降は関数が返す型を記述している。
24 まとめると、この関数 plus は、型が自然数である2つの変数が x, y を受け取り、 23 まとめると、この関数 plus は、型が自然数である2つの変数が x, y を受け取り、
25 自然数を返すという定義になる。 24 自然数を返すという定義になる。
26 25
27 実装部分の説明をする。
28 関数の定義をしたコードの直下で実装を行うのが常である。 26 関数の定義をしたコードの直下で実装を行うのが常である。
29 関数名を記述した後に引数を記述して受け取り、= (イコール) 以降で 27 関数名を記述した後に引数を記述して受け取り、= (イコール) 以降で
30 引数に対応した実装をする。 28 引数に対応した実装をする。
31 29
32 今回の場合 plus x zero であれば +0 である為、そのまま x を返す。 30 今回の場合 plus x zero であれば +0 である為、そのまま x を返す。
34 遷移している。 32 遷移している。
35 受け取った y を +1 されていたとして y の値を減らしている。 33 受け取った y を +1 されていたとして y の値を減らしている。
36 34
37 関数の実装全体をまとめると、x と y の値を足す為に y から x に数値を1つずつ渡す。 35 関数の実装全体をまとめると、x と y の値を足す為に y から x に数値を1つずつ渡す。
38 y が 0 になった際に計算が終了となっている。 36 y が 0 になった際に計算が終了となっている。
39 指折りでの足し算を実装していると捉えても良い 37 指折りでの足し算を実装していると捉えても良い。
40 38
41 \subsection{Data 型} 39 \subsection{Data 型}
42 Deta 型とは分岐のことである。 40 Deta 型とは分岐のことである。
43 そのため、それぞれの動作について実装する必要がある。 41 そのため、それぞれの動作について実装する必要がある。
44 例として既出で Data 型である ℕ の実装を見てみる。 42 例として既出で Data 型である ℕ の実装を見てみる。