Agda での Programming 技術

Menu Menu

 


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

証明支援系の歴史は古い ( 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 ... )


射と合成則


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

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

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

これだけ。(あとは、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 とう。


Natural Transformation

Functor で可換を書くと、

ここで、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 と呼ばれる以下の可換図を満たす。


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 に相当する。

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


Monad の合成

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

合成則の証明は煩雑


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 を使うと幸せになれます

 

  / Sat Jan 11 10:10:38 2014