-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

例題としての圏論

証明支援系の歴史は古く、80年代にはMLで記述されたHOL\cite{}が既に使われるようになってきた。
ここで使う Agda\cite{} は、証明とλ式が対応するという Curry Howard 対応に基づく証明支援系であり、
Haskell\cite{} で記述されている。この論文では、Agda での証明の実際をプログラミングの
視点から考察する。

証明支援系は、従来、小さいプログラムが満たす性質を証明しようとしても記述が膨大になると
いう欠点があった。近年では、数万行程度のプログラムも証明の対象にすることができるように
なってきてる。しかし、ここでは、実際のプログラムの性質の証明とは違った視点から
証明支援系の必要性を調べてみたい。

Haskell などの関数型言語では、I/Oや継続、計算量、並列計算などの計算の様々な様相を Monad の仕組みを用いて
実現している。Monad は圏論(Category theory)の概念であり、その性質の証明は若干煩雑である。
Monad は随伴関手(Adjoint pair)や、Kleisli 圏と対応しているが、それを理解するには一連の証明を
理解する必要がある。

Monad の非数学的な説明はいくつかあるが、Monad を使ってプログラムを記述する必然性を
理解しようとすれば証明を避けるのは好ましくない。そこで、証明支援系を使って、Monad を
理解できれば、関数型プログラミングを学ぶものにとって都合が良いと思われる。特に、
Haskell で記述された Agda は構文的に Haskell と似ていて、理解しやすい。

プログラムのバグを見つけるにはモデル検証が使われるようになってきているが、モデル検証は
式と値の対応に着目して、その可能な対応をすべて列挙することにより反例を見つける。これは、
命題式に真偽を割り当てていく方法になっている。

Agda の論理は、証明を提示すことによって命題式が真であることを示すハイティング代数という
ものである。モデル検証とは本質的に異なる方法である。

証明支援系としては Coq も良く使われている。Agda と Coq は良く似ているが、Agda は Emacs
を用いた式変形と穴埋め的な使い方をするのに対して、Coq は自動証明を重視したコマンドによる
式変形を中心とした使い方するようになっている。証明支援系の比較などは、この論文\cite{}が
参考になる。

ここでは Agda での証明の対象して圏論、特に、Monad を用いる。Monad を理解するために、
Agda をどのように使えるか、そこで使える Agda でのいつくかの tips を示す。


--人による証明

%数学の本に書いてある証明
%
%省略された部分
%
%問題を解いてわかる部分
%
%手書きの証明
%
%清書された証明
%
%Proof System 上の証明
%
%理解するとはどういうこと?
%
%モデルを理解する
%
%証明を理解する
%
%パターンを理解する

Agda での証明の実際に入る前に、本に書かれているような証明について調べてみよう。

数学の本には証明が極めて簡潔に書かれている。Monad を理解するためには、圏(Category)、関手(Functor)、
自然変換(Natrual Transformation)、Monad が満たす関手と自然変換の性質を理解して、Haskell の Monad の
join の結合法則 

   f * ( g * h ) = ( f * g ) * h

を証明することが目標だとしよう。ここでは Introduction to higher order categorical logic を例として用いる。

圏の定義は、

   Definition 1.1. A concrete category is a collection of two kind of entities called object and morphisms.
   The former are sets which are endowed with some kind of structure, and the latte are mappings, tha is functions from
   one object to another, in some sencse preserving that structure. Among the morphisms, there is atteched to each
   object A the identity mapping 1_A: A -> A such aht 1_A(a) = a for all a ∈ A. 　More over, morphims f : A -> B 
   and g : b-> C may be compoosed to prodicue a morphism gf: a -> C such hat (gf)a() = g(f(a) for all a ∈ A.

関手の定義は、

   Definition 1.3. A cuntor F: A->B is first of all a morphism of graph, that is, it sends objects of A to
   object so B and arrows of A to arrows of B such that, if f: A->A' then F(f):F(A)->F(A'). Moreover
   functor preserves identities and compisition; thus
      F(1_A) = 1_F(A), F(gf) = F(g)F(f)

自然変換の定義は、

    Definition 2.1. Given functors F,G: A -> B, a natural transformatin t: F -> G is a familty of
    arrows t(A): F(A) -> G(A) in B, one arrow for each object A of A, suc that the following
    square commutes for all arrows f: A -> in A.

    that is to say, such that

       G(f)t(a) = t(B)F(f).

と書かれている。さらに、Monad は関手Tと二つの自然変換の組であり以下のように定義されている。

    Definition 6.1 A triple(T,η,μ) on a category A consists of a functor T: A->A and natural transformation η: 1_A -> T
    and μ:T^2 -> T satifying the equation

      μ○Tη = 1_T = μ○ηT, μ○μT = μ○Tμ

となっている。 ここで、関手Tと自然変換ηの 合成 Tηの定義は

     (Tη)(A) = T(η(A))     \label{comp-of-func-nat}
     (ηT)(A) = η(T(A))     \label{comp-of-nat-func}

である。

これらの定義から証明するべきなのは、join の結合性であり、join は以下のように記述される。

    g * f =def μ(A'')T(g)f 

以上の定義に対して、

   f * ( g * h ) = ( f * g ) * h

を示せば良い。

本の証明は自然言語で書かれていて、簡潔な代わりに多くのものが省略されている。例えば、式\ref{comp-of-func-nat}
に出てくるTと式\ref{comp-of-nat-func} に出てくるT は、前者は arrows からarrows の関数であり、後者は
object から object への関数である。つまり、同じ T で二つの異なる関数を表している。確かに関手の定義には、
二つの関数が記述されている。これは、文章による証明の記述では記号が polymorphic に使われることを示している。
つまり、それが要求される型によって異なる関数が対応している。

---関手とは何か、自然変換とは何か

関手は定義の通りのものだが、Monad の視点から見ると、データ型のコンストラクタに相当する。
例えば、文字の集合があった時に、文字列やファイルを作るのは、文字の集合に相当する圏から、
ファイルの集合に相当する圏への関手になる。この場合、関手は文字列の結合に対する分配則を
満たす必要がある。

すると、自然変換はデータ型からデータ型への変換を表す。例えば、SJISのファイルからUTF8へのファイルに変換する
プログラム nkf は、自然変換だと考えられる。実際、 ファイルからファイルへの操作、例えば grep '単位' があった時に、SJIS で SJIS対応のgrepを使ってから、nkf で
UTF8の結果に変換するのと、先にnkfでUTF8に変換してからUTF8対応のgrepを使うのと結果は同じでなければならない。
これが可換性であり、自然変換であるための条件になる。

このような特定の分野に向いた例示は定義からは出てこない。

証明で重要なのは、関手の提供する関手の分配法則と、自然変換の提供する可観測であり、それ以外の余計な直観は必要ない。

---Monadのjoinとは何か

Monad は一つの関手Tと二つの自然変換(η,μ)を含む複雑な概念だが、T は Monad を表すデータ構造のコンストラクタだと考えて良い。
これは、計算の様々な様相を表すメタデータと、通常の入力との組であることが多い。

ηは、メタデータから通常のデータだけを取ってくる自然変換であり、Haskell Monad のreturnに相当する。μは、結合されるべき二つの
関数が生成する二つのTを一つのTにまとめる自然変換である。これは、Haskell Monad の join に相当する。

--手書きの証明

定義は与えられたので、証明するべき命題、

   f * ( g * h ) = ( f * g ) * h

を定義に沿って展開すれば良い。これはかなり長い式になる。右側と左側から両方を展開する。そして、見比べる。
これを関手の分配則と、自然変換が持つ可観測により変形して等しいことを示せば良い。

ここで、可換図が重要になる。可換図は自然変換の可換則の具体例を示すのに使える。つまり、自然変換の等式の
変数を具体的に決めたものを与える。これを使って、計算することになる。

--証明の清書

手書きの証明が終わると、これを例えば LaTeX などで清書する。清書には一部可換図も含まれる。ここでは以下のような式の変形と可換図が
得られる。

--証明を理解するということ

ここでは証明は式の一連の変形であり操作に過ぎない。この操作を理解することと、関手や自然変換が何かを理解することは別物である。

圏や関手の公理を満たす例を考えることは、その数学構造のモデルを考えることに相当する。モデルとは、ここでは、公理をすべて正しくするような
変数の値の組である。

モデルとして圏や関手を理解することと、証明を理解することは違うことだが、モデルがあれば、その理論は整合的であることが言える。
また、証明があれば、その式は正しい。

Monad の定義から自明に join の結合法則を導くようなモデルを考えることは難しいが、証明自体は式の変形でわかりやすい。しかし、
量も多く煩雑な操作となる。ここで、証明支援系が役に立つと思われる。


--Agda

% Append の例
% 
% 式
% 
% Lambda 式
% 
% 変数の定義
% 
% 変数の型
% 
% データ型
% 
% レコード型
% 
% 等号
% 
%    データ型を使った等号
%    関係を表す集合としての等号
% 
% 集合のレベル
% 
% 暗黙の引数
% 
% emacs との連携

ここでは Agda をざっと概観する。例えば、\cite{} の論文がわかりやすい。
Agda は Haskell と同じような構文を持つλ式の集合である。例えば、Agda の append は以下のようになる。

    infixr 40 _::_
    data  List {a} (A : Set a) : Set a where
       [] : List A
       _::_ : A → List A → List A


    infixl 30 _++_
    _++_ : ∀ {a} {A : Set a} → List A → List A → List A
    []        ++ ys = ys
    (x :: xs) ++ ys = x :: (xs ++ ys)

このプログラムは、Haskell の定義とほぼ同じである。Haskell と違い型定義を省略することはできない。また、List の要素の型 A が Set として
明示されている。最初の data List が List のデータ型を定義している。append は ++ で定義される。

つまり、Agda では、一つの関数を定義するのに、型と関数の両方を定義する必要がある。Agda の型は、また、Agda の式であり、それ自体の
型の整合性が要求される。 一つの名前を定義するのに、: で型を定義して、= で、その値を定義する。 

data 型の要素の数だけパータンを作ることができ、この場合は、[] と _::_ の二つの場合分けになっている。:: は中置き演算子であり、

    _::_(a,b) 

と

   (a :: b)

は同じものを表している。

ここでは型には ( 変数名 : 型名 ) による型の要素の定義と、(入力型→出力型)で表される関数の二種類がある。

{a} は、暗黙の引数であり、呼び出す時に省略することができる。ここでは、集合のレベルを暗黙に与えている。
∀ は飾りであるが任意の a に付いて成り立つことを意味している。

Agda では集合のパラドックスを避けるために集合の集合は一つの上のレベルの集合になる。Set a はレベルaの
集合になる。Set (suc a) は、Set a の一つ上のレベルの集合を表す。ここでは、任意のレベルの集合に対する
List を定義している。

infixl, infixr が中置き演算子であり、_  が引数の位置を表す。a ++ b の演算子は _++_ であり、_++_ a b  と同じものを表している。

---data型を使った等号

Agda には、さまざまな等号や関係が定義されるが、同じ物を表すのには data 型が使われる。

    infixr 20  _==_

    data _==_  {A : Set } :  List A → List A → Set  where
          reflection  : {x : List A} → x == x

同じ物を二つ並べて作られるデータ構造が reflection を提供する。これは等号の反射率 a= a に相当する。
data の filed の reflection は、等号のコンストラクタだと考えることができる。つまり、a を与えると、
a == a というデータ構造を返す。これは、a == a の証明に対応するλ式でもあって、Curry Haward 対応に
相当する。

これは、実際には、Relation.Binary.PropositionalEquality で定義されているので、自分で定義する必要はない。

data 型の他に record 型あり、この append の例題では使わないが、排他的和を表すデータ構造を提供し、圏や関手を定義することができる。


--Agda での証明方法

Agda は Emacs と連携して使用されることが想定されている。Emacs が backend である agda を起動して、Emacs 上で操作を行う。

--- ? の使い方


Agda では、まず、ファイルを読み込み C-L (agda2-load)とすると、 全体の型がチェックされ、色で識別される。

<img src="fig/agda-list-1.png">
 
定義した式の一部を ? で置き換えると、そこに必要な型を示してくれる。

--List の append の結合法則の証明

証明には、まず証明するべき式を型として定義する。この型を与えるλ式が証明になるのが Curry Howard 対応である。

    list-assoc : {A : Set } → ( xs ys zs : List A ) →
         ( ( xs ++ ys ) ++ zs ) == ( xs ++ ( ys ++ zs ) )
    list-assoc  = ?

list-assoc は、入力として A の list を取る。そして、結合法則を表す等式(を表したデータ構造 _==_ )を返す。_==_ は、同じものからしか作ることはできない。

? は、

    ?0 : {A₁ : Set} (xs ys zs : List A₁) →
        xs ++ ys ++ zs == xs ++ (ys ++ zs)

だと Agda が教えてくれるが、これは、証明すべき型を返しているだけで証明のヒントにはならない。

List は、二つのfieldを持つデータ構造なので、それを場合分けすることができる。

    list-assoc  [] ys zs = ?
    list-assoc  (x :: xs)  ys zs = ?

これは、Haskell のパターンマッチと同じ構文である。今度は、

    ?0 : [] ++ ys ++ zs == [] ++ (ys ++ zs)
    ?1 : x :: xs ++ ys ++ zs == x :: xs ++ (ys ++ zs)

となる。?0 の方は、_++_ の定義( [] ++ ys = ys )から ys ++ zs になる。これは、Emacs の ?0 上にカーソルを合わせて、

    \ys zs -> [] ++ ys ++ zs
    \ys zs -> [] ++ (ys ++ zs)

を、それぞれ C-n ( normalize ) すると、両方、

    λ ys₁ zs₁ → ys₁ ++ zs₁

となる。つまり両辺は同じものなので、_==_ のコンストラクタ reflection を使って生成できる。

    list-assoc  [] ys zs = reflection

つまり、 list-assoc  [] ys zs の型を生成するのが reflection であり、list-assoc  [] ys zs は ys ++ zs == ys ++ zs でもある。

    ?1 : x :: xs ++ ys ++ zs == x :: xs ++ (ys ++ zs)

の方は、_++_ のもう一つのパターンを使う必要がある。こちらの両辺は、C-n を使っても

    λ x₁ xs₁ ys₁ zs₁ → x₁ :: (xs₁ ++ ys₁ ++ zs₁)
    λ x₁ xs₁ ys₁ zs₁ → x₁ :: (xs₁ ++ (ys₁ ++ zs₁))

となり、そのままでは同じにはならない。しかし、:: の後ろの部分が証明するべき式と同じであることはわかる。
List は一つ短くなっているので、これを既に証明されている式とみなして良い。[] の場合の証明は終わっているので、
帰納法の基点は証明されている。つまり、後ろの部分、

    (xs₁ ++ ys₁ ++ zs₁) == (xs₁ ++ (ys₁ ++ zs₁))

は list-assoc xs₁ ys₁ zs₁ そのものになる。あとは、同じものに xs₁ を append しても同じであることが証明できれば良い。つまり、

    eq-cons :  ∀{n} {A : Set n} {x y : List A} ( a : A ) → x ==  y → ( a :: x ) == ( a :: y )

を証明できれば良い。

そのためには、congluence を使う。これは、同じ入力に同じ関数を作用させても同じになるという定理になる。これは、以下のように証明される。

    cong1 : ∀{a} {A : Set a } {b} { B : Set b } →
       ( f : List A → List B ) → {x : List A } → {y : List A} → x == y → f x == f y
    cong1 f reflection = reflection

ここで、cong1 の最初の引数は作用させる関数f で、二つ目の引数は x == y という式である。x == y は _==_ のデータ構造で、
reflection という field を持っている。

    cong1 f reflection 

は、

    list-assco [] ys zs

と同じパターンマッチングになる。reflection の型は x == x なので、x == y とマッチした時に、x と y は単一化されて同じものになる。
同じものなので、

   f x == f x 

という型を reflection によって作ることができる。これで cong1 の証明ができたことになる。

f に λ x → ( a :: x ) を使うと eq-cons を証明できる。

    eq-cons :  ∀{n} {A : Set n} {x y : List A} ( a : A ) → x ==  y → ( a :: x ) == ( a :: y )
    eq-cons a z = cong1 ( λ x → ( a :: x) ) z

最終的な証明は、

    list-assoc : {A : Set } → ( xs ys zs : List A ) →
         ( ( xs ++ ys ) ++ zs ) == ( xs ++ ( ys ++ zs ) )
    list-assoc  [] ys zs = reflection
    list-assoc  (x :: xs)  ys zs = eq-cons x ( list-assoc xs ys zs )

という形になる。残念ながら、これは人に読みやすいとは言えないが、Agda では推論規則による数式変形という形で読みやすい形にすることが可能になっている。

--数式変形

数式変形を使うと、この証明は以下のようになる。

    ++-assoc : ∀{n} (L : Set n) ( xs ys zs : List L ) → (xs ++ ys) ++ zs  == xs ++ (ys ++ zs)
    ++-assoc A [] ys zs = let open ==-Reasoning A in
      begin -- to prove ([] ++ ys) ++ zs  == [] ++ (ys ++ zs)                                                                                     
       ( [] ++ ys ) ++ zs
      ==⟨ reflection ⟩
        ys ++ zs
      ==⟨⟩
        [] ++ ( ys ++ zs )
      ∎

    ++-assoc A (x :: xs) ys zs = let open  ==-Reasoning A in
      begin -- to prove ((x :: xs) ++ ys) ++ zs == (x :: xs) ++ (ys ++ zs)                                                                        
        ((x :: xs) ++ ys) ++ zs
      ==⟨⟩
         (x :: (xs ++ ys)) ++ zs
      ==⟨⟩
        x :: ((xs ++ ys) ++ zs)
      ==⟨ cong1 (_::_ x) (++-assoc A xs ys zs) ⟩
        x :: (xs ++ (ys ++ zs))
      ==⟨⟩
        (x :: xs) ++ (ys ++ zs)
      ∎

数式が ==⟨ cong1 (_::_ x) (++-assoc A xs ys zs) ⟩ などで変形されている。 ==⟨ reflection ⟩ は、何の変形もしてないが、両方が異なる見かけの同じ正規型
である時に見かけを変形している。 ==⟨⟩ と書くこともできる。

---数式変形の記述

この数式変形自体も Agda で記述されている。

    module ==-Reasoning {n} (A : Set n ) where

      infixr  2 _∎
      infixr 2 _==⟨_⟩_ _==⟨⟩_
      infix  1 begin_


      data _IsRelatedTo_ (x y : List A) :
                         Set n where
        relTo : (x≈y : x  == y  ) → x IsRelatedTo y

      begin_ : {x : List A } {y : List A} →
               x IsRelatedTo y →  x ==  y
      begin relTo x≈y = x≈y

      _==⟨_⟩_ : (x : List A ) {y z : List A} →
                x == y  → y IsRelatedTo z → x IsRelatedTo z
      _ ==⟨ x≈y ⟩ relTo y≈z = relTo (trans-list x≈y y≈z)

      _==⟨⟩_ : (x : List A ) {y : List A}
                → x IsRelatedTo y → x IsRelatedTo y
      _ ==⟨⟩ x≈y = x≈y

      _∎ : (x : List A ) → x IsRelatedTo x
      _∎ _ = relTo reflection

これは List 専用の式変形を定義している。trans-list は、List での等式の三段論法になっている。これは、単一化で証明される。

    trans-list :  ∀{n} {A : Set n} {x y z : List A}  → x ==  y → y == z → x == z
    trans-list reflection reflection = reflection

relTo が、等しくなるべき等式を持っていて、証明の最後を示す _∎ _ が、三段論法で繋がったすべての等式が等しいことを要求する。
最後に　begin_ が _IsRelatedTo_ を _==_ に変換する。

数式変形は任意の等式に使えるが、自分用にカスタマイズして使う方が良い。良く使用する推論や定理も一緒に記述する方が良い。

Agda の module には引数があり、暗黙の引数も使うことができる。

---数式変形用に ? を使う

証明の例 (Append の結合)

record の使い方

数学的構造の存在を示す

record での変数の位置の選択

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

eval の使い方

Agda では証明できないもの

外延性

合同性

a=b は証明できない。

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

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

暗黙の変数を明示する

再利用性

module parameter と、lemma の入力

Mono morphism から来る問題

--圏論の例

圏の定義

関手の定義

自然変換の定義

Monad の結合性の証明


--Agda の有効性

Haskell の構文との親和性

証明の完成度がわかる

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

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

すべて人手

式変形を明示できる

証明は極めて個人的

勝手な記号

勝手なrecord

勝手な module parameter

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

--今後の展開

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