# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1485831432 -32400
# Node ID 6318c8f4bb8c378725bb4e9b30f84dc1ce9d8fec
# Parent  451c510825dee91f5ae4bd6a880eb02d02310062
Writing Agda description

diff -r 451c510825de -r 6318c8f4bb8c paper/agda.tex
--- a/paper/agda.tex	Tue Jan 31 10:30:08 2017 +0900
+++ b/paper/agda.tex	Tue Jan 31 11:57:12 2017 +0900
@@ -278,5 +278,70 @@
 % }}}
 
 \section{依存型を持つ証明支援系言語 Agda}
+型システムを用いて証明を行なうことができる言語に Agda が存在する。% ref Agda のref
+Agda は依存型という強力な型システムを持っている。
+依存型とは型も第一級オブジェクトとする型であり、型を引数に取る関数や値を取って型を返す関数、型の型などが記述できる。
+この節では Agda の文法的な紹介を行なう。 % ref pdf のアレ
+
+まず Agda のプログラムは全てモジュールの内部に記述されるため、まずはトップレベルにモジュールを定義する必要がある。
+トップレベルのモジュールはファイル名と同一となる。
+例えば \verb/AgdaBasics.agda/ のモジュール名定義はリスト~\ref{src:agda-module}のようになる。
+
+\lstinputlisting[label=src:agda-module, caption=Agdaのモジュールの定義する] {src/AgdaBasics.agda}
+
+また、Agda はインデントに意味を持つ言語であるため、インデントはきちんと揃える必要がある。
+
+まず Agda におけるデータ型について触れていく。
+Agda における型指定は $:$ を用いて行なう。
+例えば、変数xが型Aを持つ、ということを表すには \verb/x : A/ と記述する。
+
+データ型は Haskell や ML に似て代数的なデータ構造のパターンマッチを扱うことができる
+データ型の定義は \verb/data/ キーワードを用いる。
+\verb/data/キーワードの後に \verb/where/ 句を書きインデントを深くした後、値にコンストラクタとその型を列挙する。
+例えば Bool 型を定義するとリスト~\ref{src:agda-bool}のようになる。
+
+\lstinputlisting[label=src:agda-bool, caption=Agdaにおけるデータ型 Bool の定義] {src/AgdaBool.agda}
+
+Bool はコンストラクタ \verb/true/ か \verb/false/ を持つデータ型である。
+Bool 自身の型は \verb/Set/ であり、これは Agda が組み込みで持つ「型の型」である。
+Set は階層構造を持ち、型の型の型を指定するには Set1 と書く。
+
+関数の定義は Haskell に近い。
+関数名と型を記述した後に関数の本体を \verb/=/ の後に指定する。
+関数の型は単純型付き $ \lambda$ 計算と同様に $ \rightarrow $ を用いる。
+なお、$\rightarrow$に対しては糖衣構文 \verb/->/ も用意されている。
+引数は変数名で受けることもできるが、具体的なコンストラクタを指定することでそのコンストラクタが渡された時の挙動を定義できる。
+これはパターンマッチと呼ばれ、コンストラクタで case 文を行なっているようなものである。
+例えば Bool 型の値を反転する \verb/not/ 関数を書くとリスト~\ref{src:agda-not}のようになる。
+
+\lstinputlisting[label=src:agda-not, caption=Agdaにおける関数 not の定義] {src/AgdaNot.agda}
+
+パターンマッチは全てのコンストラクタのパターンを含まなくてはならない。
+パターンマッチは上からマッチされていくため、優先順位が存在する。
+なお、コンストラクタをいくつか指定した後に変数で受けると、変数が持ちうる値は指定したコンストラクタ以外となる。
+例えばリスト~\ref{src:agda-pattern}のnot は x には true しか入ることは無い。
+
+\lstinputlisting[label=src:agda-pattern, caption=Agdaにおけるパターンマッチ] {src/AgdaPattern.agda}
+
+なお、マッチした値を変数として利用しない場合は \verb/_/ を用いて捨てることもできる。
+
+単純型で利用した自然数もデータ型として定義できる(リスト~\ref{src:agda-nat})。
+自然数のコンストラクタは2つあり、片方は自然数ゼロ、片方は自然数を取って後続数を返すものである。
+例えば3は \verb/suc (suc (suc zero))/ となる。
+
+\lstinputlisting[label=src:agda-nat, caption=Agdaにおける自然数の定義] {src/AgdaNat.agda}
+
+自然数に対する演算は再帰関数として定義できる。
+例えば自然数どうしの加算は二項演算子\verb/+/としてリスト~\ref{src:agda-plus}のように書ける。
+
+この二項演算子は正確には中置関数である。
+前置や後置で定義できる部分を関数名に \verb/_/ として埋め込んでおくことで、関数を呼ぶ時にあたかも前置演算子のように振る舞う。
+また、Agda は関数が停止するかを判定できる。
+この加算の二項演算子は左側がゼロに対しては明かに停止する。
+左側が1以上の時の再帰時には \verb/suc n/ から \verb/n/へと減っているため、再帰で繰り返し減らすことでいつかは停止する。
+
+\lstinputlisting[label=src:agda-plus, caption=Agda における自然数の加算の定義] {src/AgdaPlus.agda}
+
+
 \section{Reasoning}
 
diff -r 451c510825de -r 6318c8f4bb8c paper/escape_agda.rb
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/escape_agda.rb	Tue Jan 31 11:57:12 2017 +0900
@@ -0,0 +1,23 @@
+#!/usr/bin/env ruby
+
+Suffix     = '.agda.replaced'
+EscapeChar = '@'
+FileName   = ARGV.first
+
+ReplaceTable = {
+  '->' => 'rightarrow',
+  '∙'  => 'circ',
+  '≡' => 'equiv',
+  '×' => 'times',
+  '⟨'  => 'langle',
+  '⟩'  => 'rangle',
+  '∎'  => 'blacksquare'
+}
+
+code = File.read(FileName)
+ReplaceTable.each do |k, v|
+  escaped_str = EscapeChar + "$\\#{v}$" + EscapeChar
+  code = code.gsub(k, escaped_str)
+end
+
+File.write(FileName.sub(/.agda$/, Suffix), code)
diff -r 451c510825de -r 6318c8f4bb8c paper/src/AgdaBasics.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/AgdaBasics.agda	Tue Jan 31 11:57:12 2017 +0900
@@ -0,0 +1,1 @@
+module AgdaBasics where
diff -r 451c510825de -r 6318c8f4bb8c paper/src/AgdaBool.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/AgdaBool.agda	Tue Jan 31 11:57:12 2017 +0900
@@ -0,0 +1,3 @@
+data Bool : Set where
+  true  : Bool
+  false : Bool
diff -r 451c510825de -r 6318c8f4bb8c paper/src/AgdaNat.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/AgdaNat.agda	Tue Jan 31 11:57:12 2017 +0900
@@ -0,0 +1,3 @@
+data Nat : Set where
+  zero : Nat
+  suc  : Nat -> Nat
diff -r 451c510825de -r 6318c8f4bb8c paper/src/AgdaNot.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/AgdaNot.agda	Tue Jan 31 11:57:12 2017 +0900
@@ -0,0 +1,3 @@
+not : Bool -> Bool
+not  true = false
+not false = true
diff -r 451c510825de -r 6318c8f4bb8c paper/src/AgdaPattern.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/AgdaPattern.agda	Tue Jan 31 11:57:12 2017 +0900
@@ -0,0 +1,3 @@
+not : Bool -> Bool
+not false = true
+not x     = false
diff -r 451c510825de -r 6318c8f4bb8c paper/src/AgdaPlus.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/AgdaPlus.agda	Tue Jan 31 11:57:12 2017 +0900
@@ -0,0 +1,3 @@
+_+_ : Nat -> Nat -> Nat
+zero  + m = m
+suc n + m = suc (n + m)