-title:  Agda での Programming 技術

-author: 　

--なんで、今、証明支援系なのか?

証明支援系の歴史は古い ( HOL, Coq, Agda も新しくない )

Haskell が流行ってるようだが…

     Haskell はMonad使いまくり

     Monadって何?

--この発表は...

Agdaをさんざん触って面白かった

  1部　Monad って何?
  2部　Agda って何?

--Monadって何?

Monad を解説しているサイトは多いが、多くは皮相的

元は圏論の概念

→　だったら、Monad を証明支援系を使って理解すれば良いんじゃないの?

とりあえず、目標は Monad の合成則の証明

--圏

Category とは、集合であるオブジェクト A と、オブジェクト間の写像である射 f の組。
    id(A) とは、A の要素を同じ要素に写像する射で必ず存在する 

f: A->B, g: B->C に対して、射の合成がある。
    g ○ f : A->C

合成則

    h ○ (g ○ f )  = (h ○ g) ○ f )

A->A への単位射がある。同じ値を同じ値に返す射。
    id_a : A->A

これだけ。(あとは、Functor, Natural Transformation, Adjunction, Monad ... )

--射と合成則

<center><img src="fig/arrow.jpg"></center>


--圏と関数型プログラミングとの関係

射が関数 ( = 関数型プログラミングのプログラム)

対象が型 ( 射は、型→型の写像)

これだけ。(あとは、Functor, Natural Transformation, Adjunction, Monad ... )

--圏としての型

例えば Integer は、Integer から Integer への関数がある。これを射と考える。

関数の合成則は成立しているし、単射もある。

型は圏でもある。

   Int → List

--Functor

Functor F とは、Category C から D への射

Cの対象aをDの対象a'に対応させる写像をFObjとする。
Cの射fをDの射f'に対応させる写像をFMapとする。

射の対応が、以下を満たす時に、F はFunctor と言う。

    (1) C の射 f:a->b を Dの射 F(f):F(a)->F(b) に割り当てる (FMap)
    (2) id(F(a)) = F(id(a))
    (3) f: a->b, g: b->c に対して、
        F(g) ○ F(f) : F(g○f)   分配法則

Functor は対象の写像FObjと、射の写像FMapの二つを持つ。

Functor の数学記法は polymorphic

--Constructor としての Functor

Integer と List はどちらも圏であり、
Integer から List を作る Constructor は、
Category から Category への Functor に相当する。

つまり、Haskell の data はFunctor になる。

    data List a = (::) a (List a)
           |      []

   data Nodes a = Node (Nodes a) (Nodes a)
       |       Leaf a

List や Node を Functor のFObj(対象の射)として考えることができる。
(Leaf や :: は　constructor )

--FMap

Functor の射の写像は、fmap として(自分で)定義する。

     class Functor f where
        fmap :: (a->b) -> f a -> f b

    fmap f (Leaf a ) =  Leaf (f a)
    fmap f (Node  a b ) =  Node (fmap f a) (fmap f b)


fmap は要素の関数 g: a->b を List や Node の関数へ変換している。
この時、f は List や Node の要素を操作する関数。

            T(f)
      T ------------> T

は T の要素に f を作用させると考えて良い。

--Natural Transformation (自然変換)

Node から List への変換を考える。これは、Functor から Functor への射になる。

例えば、flatten ( 木を深さ順にリストにする) は、そういう射の例である。

Node の要素をIntegerからStringに変換するには show が使える。( show 1 = '1' )

ここで、

   flattern ( List.fmap show aNode ) = Node.fmap show ( flattern  aNode )

これを可換(commute)という。可換なFunctorからFunctorへの射をNatural Transformation
とう。

<center><img src="fig/flatten.jpg"></center>

--Natural Transformation

Functor で可換を書くと、

<center><img src="fig/nat.jpg"></center>

ここで、F,G は、データ型。F(a)/F(b)) は FObj 。F(f) / G(f) は FMap。

t は自然変換(引数は要素の型)

--Monad

Monad とは、Functor T と二つの自然変換η,μの三つ組　 (T,η,μ) で、
以下の性質を満たすものである。

    T: A -> A             T は AからAへのFunctor
    η: 1_A -> T            ηは、a から T a への自然変換
    μ: T^2 -> T            μは T T a から T a への自然変換

さらに、Unity Law と呼ばる

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

と、Association Law　と呼ばれる以下の可換図を満たす。

<center><img src="fig/nat.jpg"></center>

--Kleisli 圏

上の Monad で、 a から T b への射を 新しい Kleisli 圏の射と考える。

この射の合成を、

  f : b -> T(c)
  g : c -> T(d)
  g * f = μ(d)T(g)f    

として定義する。

Monad の合成則 (g * f ) * h = g * ( f * h ) が成立する。

--Haskell での Monad

T はFunctorだからデータ型。メタデータだと思って良い。計算の詳細に関する
メタなデータと、元のデータを含むデータ型。

Haskell Monad はメタデータを追加して返す関数。 Reflection に相当する。

<center><img src="fig/Kleisli.jpg"></center>


例えば、IO Monad は、入出力するデータをメタデータとして返す。

--Monad の合成

メタデータの変化は自然変換 μ で決まる。

<center><img src="fig/join.jpg"></center>

合成則の証明は
<a href="fig/monad-assoc.png">煩雑 </a>

--Haskell 使うのに圏論とか必要なのか?

知らなくても困らない

Monad とか用語は理解できる

Functor と map はわかる

煩雑な証明を自分でやって理解する

そもそも証明自体が圏論( Curry Howard 対応)

Curry Howard 対応な証明支援系である Agda を使えば?

(これで1部終わり。長かった...)

--Curry Howard 対応

証明とλ計算式が対応する。対応は、扱う論理に寄って異なる

論理が複雑になる分、λ計算を拡張する必要がある

　　→　ラムダ計算の拡張の指針になる

証明する論理式は型に対応する

証明するべき式の型になるλ式を作れれば証明されたことになる

--Agda とは何か

Haskell実装、Haskellに似た構文

   indent による scope の生成

型と値

   : で型を定義
   = で値を定義

集合
    すべての値は集合

集合のレベル
    集合の集合はレベルが上がる

暗黙の引数

    {} で省略可能な引数を作れる

--λ

    module proposition where
    postulate A : Set
    postulate B : Set

集合であるA,Bを命題変数として使う。

    Lemma1 : Set
    Lemma1 = A -> ( A -> B ) -> B

これが証明すべき命題論理式になる。実際には式に対応する型。
    lemma1 : Lemma1

として、この型を持つ lambda 式を使えば証明したことになる。
以下のどれもが証明となり得る。

    -- lemma1 a a-b = a-b a
    -- lemma1 = \a a-b -> a-b a
    -- lemma1 = \a b -> b a
    -- lemma1  a b = b a


--data 

Haskell の data と同じ。

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


論理式の排他的論理和を表すのにも使える。

    data _∨_  (A B : Set) : Set where
      or1 : A -> A ∨ B
      or2 : B -> A ∨ B

or1 と or2 が Constructor である。

    Lemma6  : Set
    Lemma6 = B -> ( A ∨ B )
    lemma6 : Lemma6
    lemma6 = \b -> or2 b

これは、∨ の導入になっている。削除は、

    lemma7: ( A ∨ B ) -> A
    lemma7 = ?


--equality

さらに、data は等式を表すのにも使う。

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

直観主義論理には命題自体に真偽はない。なので、返すのは Set になっている。なので、二重否定は自明には成立しない。

--record

record は、論理積を作るのに使う。

    record _∧_ (A B : Set) : Set where
       field
          and1 : A
          and2 : B

∧の導入

    lemma2 : A → B → A ∧ B
    lemma2 a b =  record { and1 = a ; and2 = b }

∧の削除 ( open _∧_  が必要 )

    lemma3 : A ∧ B → A
    lemma3 a =  and1 a

record は、ある性質を満たす数学的構造を表すのに使う。

--Append の例

    postulate A : Set

    postulate a : A
    postulate b : A
    postulate c : A


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


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


-- Append の実行

 　Agda の実行は正規化
   Haskell と同じ

    l1 = a :: []
    l2 = a :: b :: a :: c ::  []

    l3 = l1 ++ l2


--Append の結合則の証明

証明するべき式 

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


List の持つ性質を表す式

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

    cong1 :  {A : Set  }  { B : Set  } →
       ( f : List A → List B ) → {x : List A } → {y : List A} → x == y → f x == f y

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

--Agda での証明手順

(1) 証明するべき式を型として記述する

(2) 値を = ? と取り敢えず書く

(3) ? をλ式で埋めていく

(4) C-N で正しいかどうかをチェックする

    赤   ... 型エラー
    黄色 ... 具象化が足りない
    停止性を満たさなない

(5) data  は patern match で場合分けする

(6) 必要なら式変形を使う


--Haskell と Agda の違い

Haskell で結合則を証明できる?

Haskell は型に関数やデータ型の constructor を書けない

Haskell のプログラムは Agda のプログラムになる?

   float とかはない
   integer は、succesor で書く必要がある

--式変形

λ式では、人間に読める証明にならない

    ++-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
      ==⟨ reflection ⟩
         (x :: (xs ++ ys)) ++ zs
      ==⟨ reflection ⟩
        x :: ((xs ++ ys) ++ zs)
      ==⟨ cong1 (_::_ x) (++-assoc A xs ys zs) ⟩
        x :: (xs ++ (ys ++ zs))
      ==⟨ reflection ⟩
        (x :: xs) ++ (ys ++ zs)
      ∎




--いくつかの技術

等号

?

Unicode の記号

module

暗黙の引数が多すぎる

--Agda で証明できないこと

a ≡ b は証明できない

functional extensionarty

    -- Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → 
          (∀ x → f x ≡ g x) → f ≡ g → ( λ x → f x ≡ λ x → g x )

実際には、

    postulate extensionality : { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } 
       → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂


部分集合

    異なる集合の要素は異なるので、部分集合を作れない
    →　　x ∈ P 　を自分で定義する

合同性   x ≡  y ならば f x ≡  f y 。これは、_≡_  に付いてしか言えない。
Relation などで定義すると、合同性は自分で仮定あるいは証明する必要がある。


直観主義論理の限界

   あんまり良くわかりません

--圏論の定理の証明

  Monad の結合性
  Monad から作る Kleisli 圏
  Kleisli 圏から作る随伴関手
  随伴関手での Limit の保存
  米田のレンマ

--本の証明とAgdaの証明

    本の証明は、山登りの道標しか示さない

    Agdaの証明は、全部繋がっている

    Agda の証明は式なので対称性が目で見える

--定理を理解することと証明を理解すること

定理を理解するということは使い方を理解すること

定理は証明のショートカットでもある

証明を理解しても使いこなせない

--結局、Monad は役に立つのか?

メタプログラミング(IOや並列処理)として便利

構文やややうざい。C のプログラミングみたい。

結合則や Functor(fmapを持つ) は必須ではない

Monad の合成はさらに煩雑 (Beck Law)

Monad Transform も「一度Monadを分解して再合成」

圏論知らなくても使えるが、勉強すれば用語は納得できる

--結局、証明 は役に立つのか?

Monad に関しては役に立たない

圏論を理解するのは役に立つ

教科書は「道標のみ」

自分で山を登らないと。山を登るためのツール。

--Agda は面白い

詰将棋みたいなもの

学会でノートPCで内職しているのは Coq 

Agda は Coq よりもマイナー

Agda の情報が少ないので面白い

みんな Agda を使おう!

--おまけ

Agda は Emacs で使うもの

Vimmer にはつらすぎる (手がつる)

vim emulator を使うと幸せになれます