# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1400569718 -32400
# Node ID c2e4b521d70c0a2ec8b785fc7df04fc1c35d58d0
# Parent  7e1b309f3181eeb104c0f79375b60b1a5f6b6cf7
Add slide to basic of Agda

diff -r 7e1b309f3181 -r c2e4b521d70c slide.md
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/slide.md	Tue May 20 16:08:38 2014 +0900
@@ -0,0 +1,129 @@
+title: Agda 入門
+author: Yasutaka Higa
+cover:
+lang: Japanese
+
+
+# このセミナーの目的
+* 証明支援系の言語である Agda の入門を目的としています
+* 具体的には
+  * Agda による証明の方法を知る
+  * 実際に自然数の加算の交換法則の証明を追う
+
+
+# セミナーについて必要する事前知識
+* なお、このセミナーについては
+  * C や Java によるプログラミング言語を書いたことがある
+    * 関数や引数、型といった単語への詳細は省略することがあります
+  * 数学における述語論理
+    * P ならば Q といった論理
+* ことを前提条件としています
+
+
+# Agda とはどういう言語なのか
+* 証明支援系と呼ばれる分野の言語です
+  * 他には Coq などがあります
+* Haskell で実装されています
+* dependent type の言語 です
+  * 型から生成さえれた型を扱える
+  * いわゆる「強い静的型付け」などと言われる種類です
+
+
+# 型と証明との対応 : Curry-Howard Isomorphism
+* Agda における証明は
+  * 証明したい命題 == 関数の型
+  * 命題の証明     == 関数の定義
+* として定義します。
+* 関数と命題の対応を Curry-Howard Isomorphism と言います
+
+
+# A ならば B と A が成り立つのなら B が成りたつ
+
+* Agda において
+  * apply : A -> (A -> B) -> B
+  * apply a f = f a
+* と記述します
+
+
+# Agda のSyntax
+* apply : A -> (A -> B) -> B
+* apply a f = f a
+
+* 関数名 : 型
+* 関数名 <引数,,,> = 定義
+
+
+# Agda の型のSyntax
+* apply : A -> (A -> B) -> B
+
+* 引数の型 -> 返り値の型
+* 結合は右結合です。なのでこのようになります
+  * A -> ((A -> B) -> B)
+* 右結合のため、A を受けとって ((A -> B) -> B) を返す、とも読めます
+
+
+# Agda の型のSyntax : 複数の引数
+* 複数の引数は
+  * Arg1Type -> Arg2Type -> ReturnType
+* のように書きますが、右結合により
+  * Arg1Type -> (Arg2Type -> ReturnType)
+* となり、引数は1つしかないと考えることができます。
+* これを Curry 化と言い、引数が複数の場合を考えずに良くなります
+
+
+# 関数の定義を C の Syntax 書くと
+* apply : A -> (A -> B) -> B
+
+* B apply(A a, B ( * apply )(A))
+* これを満たす B を関数の定義で書けば良い
+* 証明 == 返り値を返す なので
+* つまりコンパイルを通してしまえば良い
+
+
+# Agda で書いてみると
+
+* emacs から使うと良いです
+* module <filename> where
+* を先頭に書く必要があります
+* 下に証明を定義していく
+* C-c C-l で型チェック
+
+
+# Agda による apply
+* apply : A -> (A -> B) -> B
+* apply a f = f a
+
+* とは
+* A を Int, B を String とすると
+* Int と、 Int から String を返す関数があれば String を作れる
+* と読める
+
+
+# 命題に 'ならば' を含む場合
+* 関数を返せば良いです
+* Agda には lambda があるので
+
+* id : A -> A
+* id = \a -> a
+
+* いったように書けます
+
+
+# 'ならば' を含む証明
+* 三段論法 の証明
+
+* compose : (A -> B) -> (B -> C) -> (A -> C)
+* compose f g = \a -> g (f a)
+
+* 三段論法は関数の合成に相当しています
+
+
+# Agda による 証明 の方法のまとめ
+* 型として (仮定) -> (仮定) -> ... -> (命題)
+* として命題を定義
+* それを満たす定義を関数として定義する
+
+
+# 自然数の加算の交換法則の証明
+
+<!-- vim: set filetype=markdown.slide: -->