Mercurial > hg > Papers > 2020 > soto-midterm
diff tex/agda.tex @ 11:a8bc8c6b48bd default tip
fix
author | soto@cr.ie.u-ryukyu.ac.jp |
---|---|
date | Tue, 15 Sep 2020 07:06:29 +0900 |
parents | 27a6616b6683 |
children |
line wrap: on
line diff
--- a/tex/agda.tex Tue Sep 15 04:49:26 2020 +0900 +++ b/tex/agda.tex Tue Sep 15 07:06:29 2020 +0900 @@ -6,20 +6,19 @@ は記述したプログラムを証明することができる。 \subsection{プログラムの読み方} -以下は Agda プログラムの一例となる。 -本節ではAgdaの基本事項について解説する。 +本節ではAgdaの基本事項について \coderef{plus} を例として解説する。 -基本事項として、ℕ というのは自然数 (Natulal Number) のことである。 +基本事項として、$ \mathbb{N} $ というのは自然数 (Natulal Number) のことである。 また - (ハイフン) が2つ連続して並んでいる部分はコメントアウトであり、 ここでは関数を実行した際の例を記述している。 -したがって、この関数は2つの自然数を受け取って足す関数であることが推測できる。 +したがって、これは2つの自然数を受け取って足す関数であることが推測できる。 \lstinputlisting[label=plus, caption=plus] {src/agda/plus.agda} この関数の定義部分の説明をする。コードの1行目に : (セミコロン)がある。 この : の前が関数名になり、その後ろがその関数の定義となる。 -: 以降の (x y : ℕ ) は関数は x, y の自然数2つを受けとるという意味になる。 -→ 以降は関数が返す型を記述している。 +: 以降の (x y : $ \mathbb{N} $) は関数は x, y の自然数2つを受けとるという意味になる。 +$ \rightarrow $ 以降は関数が返す型を記述している。 まとめると、この関数 plus は、型が自然数である2つの変数が x, y を受け取り、 自然数を返すという定義になる。 @@ -39,13 +38,13 @@ \subsection{Data 型} Deta 型とは分岐のことである。 そのため、それぞれの動作について実装する必要がある。 -例として既出で Data 型である ℕ の実装を見てみる。 +例として既出で Data 型である $ \mathbb{N} $ の実装を \coderef{Nat} に示す。 \lstinputlisting[label=Nat, caption=Nat] {src/agda/Nat.agda} -実装から、ℕ という型は zero と suc の2つのコンストラクタを持っていることが分かる。 -それぞれの仕様を見てみると、zeroは ℕ のみであるが、suc は (n : ℕ) → ℕ である。 -つまり、suc 自体の型は ℕ であるが、そこから ℕ に遷移するということである。 +実装から、$ \mathbb{N} $ という型は zero と suc の2つのコンストラクタを持っていることが分かる。 +それぞれの仕様を見てみると、zeroは $ \mathbb{N} $ のみであるが、suc は (n : $ \mathbb{N} $ ) $ \rightarrow \ \mathbb{N} $ である。 +つまり、suc 自体の型は $ \mathbb{N} $ であるが、そこから $ \mathbb{N} $ に遷移するということである。 そのため、suc からは suc か zero に遷移する必要があり、また zero に遷移することで停止する。 したがって、数値は zero に遷移するまでの suc が遷移した数によって決定される。 @@ -53,11 +52,9 @@ 言い換えればパターンマッチをする必要があると言える。 これは puls 関数で suc 同士の場合と、zeroが含まれる場合の両方を実装していることの説明となる。 - - \subsection{Record 型} Record 型とはオブジェクトあるいは構造体ののようなものである。 -以下の関数は AND となる。p1で前方部分が取得でき、p2で後方部分が取得できる。 +\coderef{And}は AND の関数となる。p1で前方部分が取得でき、p2で後方部分が取得できる。 \lstinputlisting[label=And, caption=And] {src/agda/And.agda} @@ -65,20 +62,13 @@ これを使用して三段論法を定義することができる。 定義は「AならばB」かつ「BならばC」なら「AならばC」となる。 -コードを以下に示す。 +\coderef{syllogism}を以下に示す。 \lstinputlisting[label=syllogism, caption=syllogism] {src/agda/syllogism.agda} コードの解説をすると、引数として x と a が関数に与えられている。 -引数 x の中身は((A → B) ∧ (B → C))、引数 a の中身は A である。 -したがって、(\_∧\_.p1 x a) で (A → B) に A を与えて B を取得し、 -\_∧\_.p2 x で (B → C) であるため、これに B を与えると C が取得できる。 +引数 x の中身は ((A $ \rightarrow $ B) ∧ (B $ \rightarrow $ C)) 、引数 a の中身は A である。 +したがって、(\_∧\_.p1 x a) で (A $ \rightarrow $ B) に A を与えて B を取得し、 +\_∧\_.p2 x で (B $ \rightarrow $ C) であるため、これに B を与えると C が取得できる。 よって A を与えて C を取得することができたため、三段論法を定義できた。 -%\subsection{Agdaの基本操作} - -%\subsection{定理証明支援器としての Agda} - -%\subsectoin{} - -