-title: Agda での Programming 技術

--abstract:

Agda は、Haskell 上の Dependent type に基づく証明支援系である。
Agda での証明は型付きλ式であり、証明するべき式も型付きλ式になっている。
したがって、Agda での証明は、本質的にはλ式を構築していく作業になる。

この発表ではAgdaの入門と、Emacs 上で行われる Agda のプログラミング技術
について圏論の例題を用いながら紹介する。Dependent type に関する論文は
多いが、ここでは Agda の証明を構成するために使われる技術を紹介していく。

プログラミング言語と異なり、Agdaの証明を書き上げても、それが動くことはない。
その意味では、Agdaの証明はプログラミングとは異なる。しかし、型宣言を
行い、その型に沿ったλ式を書いていくという点ではプログラミングそのもの
である。

Agdaの証明は、Curry Howard対応に基づいており、
すべては、型を表す式と、その型を持つλ式の組で表される。
Dependent type の特徴は省略可能な引数(暗黙の引数)にあり、
これは、通常のプログラミング言語にはない概念である。


証明を構成する作業は、型に沿って行われる。Agda には、未定部分を ? と
しして指定すると、その部分に相当する型をλ式として表示してくれる。
これにより、証明の指針が得られる。

証明は型が十分に与えら得ていることが必要であり、未定の部分が含まれている
場合には Agda は、その部分を黄色で表示する。これを解決するには、暗黙の
引数を表示してやると良い。

また、Agda の特徴である式変形を明示する推論に対するいくつかの手法に
関しても考察する。

--証明支援系

Monad とか Kan extension とかを知らないと関数型プログラミングできない

Monad の結合性を示すだけでも煩雑な計算が必要

高階述語論理

ハイティング代数

Curry Howard 対応

Coq

例題としての圏論

--人による証明

数学の本に書いてある証明

省略された部分

問題を解いてわかる部分

手書きの証明

清書された証明

Proof System 上の証明

理解するとはどういうこと?

モデルを理解する

証明を理解する

パターンを理解する

--Agda

式

Lambda 式

変数の定義

変数の型

データ型

レコード型

等号

   データ型を使った等号
   関係を表す集合としての等号

集合のレベル

暗黙の引数

emacs との連携

--Agda での証明方法

? の使い方

数式変形

数式変形の記述

数式変形用に ? を使う

record の使い方

数学的構造の存在を示す

record での変数の位置の選択

これから証明する部分の扱い

eval の使い方

Agda では証明できないもの

外延性

合同性

a=b は証明できない。

赤を解決する(型の矛盾)

黄を解決する(十分限定されていない変数)

暗黙の変数を明示する

再利用性

module parameter と、lemma の入力

Mono morphism から来る問題

--Agda の有効性

Haskell の構文との親和性

証明の完成度がわかる

証明の対称性を視認できる

Unification により証明を見つけることができる

すべて人手

式変形を明示できる

証明は極めて個人的

勝手な記号

勝手なrecord

勝手な module parameter

理論の理解に使う Monad とか Kan extension とか

--今後の展開

プログラミングと証明を同時に行う