Binary file mid_thesis.pdf has changed

Binary file pic/hoare_cg_dg.pdf has changed

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/agda/And.agda	Mon Sep 14 02:58:14 2020 +0900
@@ -0,0 +1,4 @@
+record _∧_ (A B : Set) : Set where
+  field
+    p1 : A
+    p2 : B

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/agda/Nat.agda	Mon Sep 14 02:58:14 2020 +0900
@@ -0,0 +1,3 @@
+data ℕ : Set where
+  zero : ℕ
+  suc  : (n : ℕ) → ℕ

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/agda/plus.agda	Mon Sep 14 02:58:14 2020 +0900
@@ -0,0 +1,6 @@
+plus : (x y : ℕ) → ℕ
+plus x zero  = x
+plus x (suc y) = plus (suc x) y
+
+-- plus 10 20
+-- 30

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/agda/syllogism.agda	Mon Sep 14 02:58:14 2020 +0900
@@ -0,0 +1,2 @@
+syllogism : {A B C : Set} → ((A → B) ∧ (B → C)) → (A → C)
+syllogism x a = _∧_.p2 x (_∧_.p1 x a)

--- a/tex/agda.tex	Fri Sep 11 19:03:15 2020 +0900
+++ b/tex/agda.tex	Mon Sep 14 02:58:14 2020 +0900
@@ -1,12 +1,90 @@
 \section{Agda}
+
 Agda とは定理証明支援器であり、関数型言語である。Agda は依存型という型システ
 ムを持ち、型を第一級オブジェクトとして扱うことが可能である。また、型システムは
 Curry-Howard 同型対応により命題と型付きラムダ計算が一対一で対応するため Agda で
 は記述したプログラムを証明することができる。
 
-%\subsection{Record 型}
+\subsection{プログラムの読み方}
+以下は Agda プログラムの一例となる。
+本節では以下のコードを説明することにより、Agda プログラムについて理解を深めることにより、
+後述する Agda コードの理解を容易にすることを目的としている。
+\lstinputlisting[label=plus, caption=plus] {src/agda/plus.agda}
 
-%\subsection{Data 型}
+\begin{itemize}
+	\item 基本事項
+		\begin{itemize}
+			\item 
+				ℕ というのは自然数 (Natulal Number) のことである。
+				また、- (ハイフン) が2つ連続して並んでいる部分はコメントアウトであり、
+				ここでは関数を実行した際の例を記述している。
+				したがって、この関数は2つの自然数を受け取って足す関数であることが推測できる。
+		\end{itemize}
+    \item 定義部分
+		\begin{itemize}
+			\item 
+				コードの1行目に : (セミコロン)がある。
+				この : の前が関数名になり、その後ろがその関数の定義となる。\\
+				: の後ろの (x y : ℕ ) は関数は x, y の自然数2つを受けとる。
+				という意味になる。
+				→ の後ろは関数が返す型を記述している。
+				まとめると、この関数 plus は、型が自然数である2つの変数が x, y を受け取り、
+				自然数を返すという定義になる。
+		\end{itemize}
+	\item 実装部分
+		\begin{itemize}
+			\item 
+				関数の定義をしたコードの直下で実装を行うのが常である。
+				関数名を記述した後に引数を記述して受け取り、= (イコール) の後ろで
+				引数に対応し実装を作を記述していく。
+				今回の場合では、 plus x zero であれば +0 である為、そのまま x を返す。
+				2行目の方では受け取った y の値を減らし、x の値を増やして再び plus の関数に
+				遷移している。
+				受け取った y は+1されていたことにすることでyの値を減らしている。
+				実装部分もまとめると、x と y の値を足す為に、y から x に数値を1つずつ渡す。
+				y が 0 になった際に計算が終了となっている。
+				指折りでの足し算を実装していると捉えても良い
+		\end{itemize}
+\end{itemize}
+
+\subsection{Data 型}
+Deta 型とは分岐のことである。
+そのため、それぞれの動作について実装する必要がある。
+例として既出で Data 型である ℕ の実装を見てみる。
+
+\lstinputlisting[label=Nat, caption=Nat] {src/agda/Nat.agda}
+
+実装から、ℕ という型は zero と suc の2つのコンストラクタを持っていることが分かる。
+それぞれの仕様を見てみると、zeroは ℕ のみであるが、suc は (n : ℕ) → ℕ である。
+つまり、suc 自体の型は ℕ であるが、そこから ℕ に遷移するということである。
+そのため、suc からは suc か zero に遷移する必要があり、また zero に遷移することで停止する。
+したがって、数値は zero に遷移するまでの suc が遷移した数によって決定される。
+
+Data型にはそれぞれの動作について実装する必要があると述べたが、
+言い換えればパターンマッチをする必要があると言える。
+これは puls 関数で suc 同士の場合と、zeroが含まれる場合の両方を実装していることの説明となる。
+
+
+
+\subsection{Record 型}
+Record 型とはオブジェクトあるいは構造体ののようなものである。
+以下の関数は AND となる。p1で前方部分が取得でき、p2で後方部分が取得できる。
+
+\lstinputlisting[label=And, caption=And] {src/agda/And.agda}
+
+また、Agda の関数定義では\_(アンダースコア)で囲むことで三項演算子を定義することができる。
+
+これを使用して三段論法を定義することができる。
+定義は「AならばB」かつ「BならばC」なら「AならばC」となる。
+コードを以下に示す。
+
+\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 が取得できる。
+よって A を与えて C を取得することができたため、三段論法を定義できた。
 
 %\subsection{Agdaの基本操作}