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 ( * f )(A))
* これを満たす定義を関数applyの実装として書けば良い
* 証明 == 正しい返り値を返す なので
* つまりコンパイルを通してしまえば良い


# 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

* といったように書けます。
* lambda の syntax は \arg -> body です


# 'ならば' を含む証明
* 三段論法 の証明

* compose : (A -> B) -> (B -> C) -> (A -> C)
* compose f g = \a -> g (f a)

* 三段論法は関数の合成に相当しています


# Agda による 証明 の方法のまとめ
* 型として (仮定) -> (仮定) -> ... -> (命題)
* として命題を定義
* それを満たす定義を関数として定義する


# 自然数の加算の交換法則の証明

* TODO: いまから

<!-- vim: set filetype=markdown.slide: -->