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 で、つい、同じキーを繰り返し押してたりして、だいぶ退化した感じ。
No comments:
Post a Comment