Friday, 12 July 2013

Agda 一段落

ここ数カ月はまっていた Agda と圏論ですが、目標のところまで到達しました。Kleisli 圏の射の結合法則が証明できてうれしい。手計算でも、かなりやっかいなものです。

http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/kono/Proof/category/file/d9c2386a18a8/nat.agda

Agda には(Tutorialには載ってないが)、数式変形モード hoge-Reasoning というのがあって結構便利。で、これを Category https://github.com/konn/category-agda で使おうと思って、今週の 7/6 に「できた」とか言っているんですが、その全然動かず。

Agda の library にある ≡-Reasoning のソースコードを見ながら書くんだけど全然動かない。そいつは、≡という集合同士の等号なので、 という独自に定義した等号には無力。なので、

-to-≡ : {a b : Obj A } { x y : Hom A a b } -> A [ x ~ y ] -> x ≡ y

を証明しようとしたんけど、抽象的な圏には、 A [ x ~ y ] の定義がない。結合則とかの抽象的な定義しかないので、証明できないらいい。なので、

Category の性質として要求しちゃえ

ってことで書いてみたんですが、圏の圏 Cat で文句を言ってくる。一段、上の A [ x ~ y ] -> x ≡ y を一段下のものから作らないといけないらしい。圏の射は Functor だったりすので、二時間ぐらい Mou で頑張ったんですが諦めました。

で、もう一度、 -Reasoning を書き始めたんだけど、朝、動かしたら、なんか動く。え? 別に方針変えてないんだけど。どういうこと。どうも、7/6 に動いたのは、本当に動いたらしく、その時に、複数の Emacs を上げていたので、ダメなコードに置き換えられてしまったのではないかと。7/6 ぐらいのコードを見てみるんだけど、殆ど差がない。ええぇ。この一週間の試行錯誤はなんだったんだ。

でも、動いてめでたいです。

Agda は、だいたい 1行書くのに10分かかるらしい。作業は、

(1) recored IsHoge に公理を書いていく。
(2) recored Hoge に constructor を書く。
(3) recored Hoge に isHoge : IsHoge を書いて、公理を呼び出せるようにする

これが第一段階。

(4) 証明したい式を Lemma の型で書く
(5) 証明をλ式で Lemma = で書く

これが第二段階です。時間がかかるのは、(1)と (4) ね。(2),(3),(4) は自明なことが多い。いや、簡単なものならってことね。
い。いや、簡単なものならってことね。
    record IsNTrans {c c ℓ c′ c′ ℓ′ : Level} (D : Category c c ℓ) (C : Category c′ c′ ℓ′)
                     ( F G : Functor D C )
                     (Trans : (A : Obj D) → Hom C (FObj F A) (FObj G A))
                     : Set (suc (c  c  ℓ  c′  c′  ℓ′)) where
      field
        naturality : {a b : Obj D} {f : Hom D a b}
          → C [ C [ (  FMap G f ) o  ( Trans a ) ] ~  C [ (Trans b ) o  (FMap F f)  ] ]

    record NTrans {c c ℓ c′ c′ ℓ′ : Level} (domain : Category c c ℓ) (codomain : Category c′ c′ ℓ′) (F G : Functor domain codomain )
           : Set (suc (c  c  ℓ  c′  c′  ℓ′)) where
      field
        Trans :  (A : Obj domain) → Hom codomain (FObj F A) (FObj G A)
        isNTrans : IsNTrans domain codomain F G Trans

    open NTrans
    Lemma2 : {c c l : Level} {A : Category c c l} {F G : Functor A A}
          → (μ : NTrans A A F G) → {a b : Obj A} { f : Hom A a b }
          → A [ A [  FMap G f o Trans μ a ] ~  A [ Trans μ b o  FMap F f ] ]
    Lemma2 = \n → IsNTrans.naturality ( isNTrans  n  )


こんな感じ。変な記号が多いので読めるかどうか。\n は改行でありません。この例は公理を呼び出せるかどうかだけなので簡単。

複雑なものは、 Reasoning を使います。
 
      begin
         join k b (Trans η b) f
      refl-hom 
         c [ Trans μ b  o c [ FMap T ((Trans η b)) o f ] ]
      IsCategory.associative (Category.isCategory c) 
        c [ c [ Trans μ b  o  FMap T ((Trans η b)) ] o f ]
      car-eq f ( IsMonad.unity2 ( isMonad ( monad k )) )  
        c [  id (FObj T b)   o f ]
      IsCategory.identityL (Category.isCategory c) 
        f


こんな感じ。begin で初めて で終わる。目的の式に到達したら終わり。もちろん、証明したい式は型に書いてあって、この場合は、

-- η(b) ○ f = f
A [ join k b (Trans η b) f ~ f ]

こんな感じ。本当は、もっと長い。 x の x が式を変形するλ式ですね。実際には、

A [ (f o (g o h)) ~ ((f o g) o h) ]

とかを生成する関数です。refl-hom は、

A [ x ~ x ]

を生成してます。つまり、何もしてない。何もしてないが、join とかを展開することができます。

Agda はいろいろ癖がある。

隠れた入力変数がある

これが dependent type とか呼ばれる理由らしいのだけど、{} で書くと隠せる。() だと見える。ということは、

() と {} を目の子で区別していく必要がある

ってことね。これは非常に厳しいです。老眼には。Agda 作った奴があほだと思う理由の一つ。

隠れた変数は、実は {} で参照できる。わからなくなったら、全部手で{} で書いた方が良いです。そうすると何が衝突しているのかわかるので。

使われてない変数があると、黄色になります。なんで黄色になるのかよくわからなかったが、ようやっとわかった。使われない変数を消すと黄色は消えます。

Unresolved metas は、library が間違っている時に出るエラーメッセージ。

? と書くと、そこの型を表示してくれますが、あまり役に立たないことが多い。それよりも、

]] A→ A:

と続けるとエラー。大半のエラーがそれでしょう。Agda 作った人があほだという理由の一つ。() だけは許してもらえるらしい。

_[__] と _ [ _ _]

は違う。 お前なぁ〜〜 infix には英単語は使えないらしい。あと、

UTF-8 の特殊記号を使いまくるのが礼儀

らしいです。おかげで、7x14 にないグリフを随分作った。

式の変形に使う式で、中で出てくるものは引数として渡さないとだめらしい。{} にするか () にするかを気を付けないといけないってことね。
 
    A [ A [ A [ Trans μ d o  A [ FMap T h   o  Trans μ c ] ]  o  FMap T g ] o f ]
    car-eq f (car-eq ( FMap T g) ( cdr-eq  ( Trans μ d ) ( begin
           A [ FMap T h o Trans μ c ]
        nat A μ 
           A [ Trans μ (FObj T d) o FMap T (FMap T h) ]
        
   )))  
      A [ A [ A [ Trans μ d  o  A [ Trans μ ( FObj T d)    o  FMap T (  FMap T h ) ] ]  o FMap T g ]  o f ]
    car-eq f (sym assoc) 
     A [ A [ Trans μ d  o  A [ A [ Trans μ ( FObj T d)     o FMap T (  FMap T h ) ]   o FMap T g ] ]   o f 

という感じで、式の一部だけを Reasoning することも可能。ついさっき発見しました。
   
     car-eq f ( car-eq  (FMap T ( A [ FMap T h  o g ] )) (
     begin
         { }0
       { }1 
         { }2
      
   )) 


と部分を抜き出すと、
    ?1 : (A Category.~ A [ Trans μ d o Trans μ (FObj T d) ])
    (A [ Trans μ d o FMap T (Trans μ d) ])

と、0,2 に書くべき部分を教えてくれる。素晴らしい。これは便利だ。

証明チェック後の Read only を Writeに変える C-C C-X C-D を間違えて、C-X C-C C-D とすると、emacs を抜けて、xterm も C-D で抜けてくれます。

Agda を作った奴のアホ〜

と叫びましょう。

証明が終わると「何も(エラーが)表示されない」ので非常に達成感あって良いです。

だいたい手計算の10倍ぐらい時間がかかるんじゃなかろうか。いや、一週間、同じバグと格闘していただけだけど。手計算だと

( a + ( b + c ) + d )

( a + b ) + (c + d )

とかに直すの簡単だけど、Agda だと asocc 使って結構、苦労します。小学生が結合則を理解出来なくて試行錯誤するあれですね。まぁ、この辺りを自動的になんとかするものもあるんだろうが、

Agda は何もしない主義

らしい。いさぎよい。BSD 的だ。

まぁ、だいたい Agda は把握した気がする。いや、面白かったよ。Emacs と vi を交互に使って手がつりましたが。vi で、つい、同じキーを繰り返し押してたりして、だいぶ退化した感じ。
Post a Comment