Thursday 24 March 2016

Agda

この間からはまっていたのは、ようやっとできました。

* 振動するんだよね

あっちやって行き詰まって、また別な方向やって、また、元に戻って。しまいには、

* やろうとすると、こういう風に行き詰まるというのを思い出すように。

今回は Maybe の使い方と、data を使った制約の書き方を学べました。

まぁ、圏論/Agdaは1個とか2個とかの具体的なことをやろうと思うと大変。証明の場合分けが爆発しちゃう。

入力の射の種類によって場合分けするんですが、

* 起きないはずの場合わけが出てしまう

まぁねえ。それぞれの射にt0とt1があれば全部の組み合わせが出ちゃうよな。で、証明できない...

と思ったんですが、

* Maybeを扱っていると、just/nothingの組み合わせで出ないものがある

nothing と nothing の等号はnothingになるわけなので、等号のところにはjustとは書けない。逆に等号がnothingだと、その両辺はnothing。

そうか、そうやって場合分けを制約することができるのか! 等号は data で実装されているので、data で場合分けの制約を書ける! とわかったので、なんとかなりました。

まぁ、あんまり綺麗な感じでないけどなぁ。

Agda の data は論理式としては排他的和で異なる型の組み合わせで、データ構造としてはタグ付きのUnion。

record は直積に相当して、用途としては「fieldに記述した論理式を満たす性質を持つもの」というように使うようです。

例えば、等号は、

 data _≡_ {a} {A : Set a} (x : A) : A → Set a where
  refl : x ≡ x

こんな感じ。Prolog の f(X,X). ですね。同じ値で、refl a a みたいにしないと a ≡ a を作れない。これを入力で受けると、

  lemma1 : {a} ( x y : Set a ) -> x ≡ y -> ...
  lemma1 {a} x y eq = ...

で、x と y は同じ場合しか受け付けなくなるというわけ。なるほど。単一化、Unification という理屈だとはわかっていても、ちょっと気持ち悪いか。

二個の圏の対象は、

  data TwoObject {c₁ : Level} : Set c₁ where
    t0 : TwoObject
    t1 : TwoObject

こんな感じ。t0 と t1 は constructor ですね。

それで、射を

                                                
data Arrow {c₁ c₂ : Level } ( a b : TwoObject {c₁} ) : TwoObject {c₁} 
   -> TwoObject {c₁} -> Set c₂ where
  id-a : Arrow a b a a
  id-b : Arrow a b b b
  arrow-f : Arrow a b a b
  arrow-g : Arrow a b a b
  inv-f : Arrow a b b a

という感じで、id-a は aからa、id-b は bからb。arrow-f は a から b という風に制約してみました。これで、

aからbの射とbからbの射を入力しているのに、abからabへのあらゆる組合せが出てきてしまっていたのが、ちゃん整合しているのものしかでなくなっって、ばっちり。

なるほどね〜 いや、まぁ、あんまい綺麗な方法とも思えないが... とりあえずできてめでたい。

いや、これを使って、LimitからEqualizaerを出して、それを使って、Floyd Adjunction Functor Theorem を証明するはずなのだが、まぁ、それはおいおいだな....

No comments: