Just $ A sandbox

プログラミングと計算機科学とかわいさ

functor, あるいはarrow equalityについて

Category TheoryのFormalizationがらみの話。

Category TheoryのFormalizationをするときは、基本的にSetoid-enrichedでやるのが筋がよいということはこの業界(?)では有名な話だし、少し前のブログ記事にも書いたのでそのことを前提として次のようなことを考える。

functorの(strong)equalityは、「object partが等しい」上で「arrow partも等しい」ということで定める。
ところで、この2つのequalityは同じレベルの話ではない。

F == Gforall A, F A == G Aかつforall f, F f == G fとはできなくて、なぜなら後者は左辺と右辺で型が違う(F a -> F bG a -> G bはunifyできない)ので、この定義は上手くいかない。
さてどうするかというと、少なくとも今のところは3つの定義を考えている。

  1. F == G := Sigma (eq: forall A, F A == G A) (forall f, extend [F f] with eq == G f)のように、dependent sum typeを使ってequalityを書き換える方法
  2. 新たに圏にheterogeneous equality~を定め(定義: ~ : forall a b, hom(a,b) -> hom(c,d) -> Propであって、各homへの制限~ : relation on hom(a,b)はそこでのhomに入っている同値関係に等しい)、F == G := forall f, F f ~ G fとする方法
  3. F == G := exist (k: Nat F G), k a ~ identityとする方法

最初の方法は自明につらい。
少なくとも茨の道であることが明らかなときわざわざそこへ分け入っていこうという人は珍しいと思う。

2つ目の方法は今回やってみたがかなりヤバイことだけがわかった。
詳細は後述。

最後の方法はまだ真面目には試していない。
Natが簡単に取り出せるのでよいのかもしれないが、hetero equalityを使っている以上2番目と同じ危険性を孕んでいるのではないか、と思っているので今は積極的に採用したくない。

つらみへ

上で述べた2番目の方法のつらさについて解説する。

Canonical Extension

~は実は次のようにして、homのequality ==を用いて定義できる。(これはhom equalityの自然な拡張、あるいは貼り合わせとでも言うべき状態になっている)

Inductive Heq_hom {C : Category} {a b : C} (f : hom a b) : ∀ {c d}, hom c d → Prop :=
| mk_Heq_hom : ∀ {g : hom a b}, f == g → Heq_hom f g.

これはつまりconstructorとしてf == gからくるものだけを採用するという意味で、relationとしては異なるhom上では∅として定めるという方法だった。

さてhetero equalityではよくある話として、この型からequalityは取り出せない。
というわけでheq -> eqは公理として追加するのだけど、じゃあ公理はどうするの?という問題があって、

Axiom Heq_eq : ∀ {C : Category} {a b c d : C} (f : hom a b) (g : hom c d),
    f ≈ g → { eq : a = c ∧ b = d | extend (proj1 eq) (proj2 eq) f == g }.

当然これは最初に述べた方法のつらみから(equalityを直接扱うことのつらみから)解放されていないのであまり意味がない。
他の方法として、新たにarrow type(dom,codを無視した射の型)を作ってどうのこうのとする方法は思いついていたけれど、今度はarrow type constructorのinjectiveや他にも何らかの性質を公理として追加する必要がありそうだったのでやめた。

さて、まぁどうにかして上のようなHeq_homを(つらみは無視して)使って色々やっているとわかるのだけど、具体的に圏を作るたびにこのように対応するextended equalityを「公理とともに」追加しなければならない場合があって、実は上の方法はcanonicalだけど常にそれが欲しいものではないことがわかったりする。

例としてcomma圏のarrowのequalityは2本のarrowのpairだから、
定義としては<f,g> as comma_map ~ <h,i> ==> f ~ h & g ~ iとしたい気がするのだけど、これは当然非自明なので使いたいならまた公理として追加しなければならない。

と、ここまでくると、実はhetero equalityは圏によってspecificなものではないかという考えが沸いてくるわけである。

Extended Category

上の方法は一旦忘れて、圏の定義にhetero equalityを含めてしまおう。
つまり、圏のデータに~を要請し、category axiomに「~を各homに制限したものはhomのequalityに等しい」ことを要請することにする。

しかし実はこれだけではだめで、compositionと~のcompatibilityが足りないことがわかる。

Formalization業界ではよくしられていることとして、圏のデータにarrow equality ==を含める場合は実はcompositionとのcompatibilityも新たに定義に含める必要があり、そもそもそういう勝手な演算とそのcompatibilityを無闇に追加することを嫌って「Setoid-enriched」という理屈では素晴らしい定義を採用したのだけれど

我々はここにきてhetero equalityとそのcompatibilityを無闇に追加することと相成ったのである

困ったことに、==はenrichmentという仕組みが上手く隠蔽してくれていたが、~はheteroなので(各homごと、ではない)enrichmentして隠蔽とかいう問題でもない。

あるいは、こういう「圏全体に対するheteroなenrichment」という概念が別にあり、今度はそれが上手く隠蔽してくれるのかもしれない。

まぁしかし私は3つのequalityを使って証明を書く気はおこらないので、素直にhetero equalityを捨てるformalizationを考えようと思った。

なお、まだいい方法は見つかってない。

あのとき知りたかったCoqの話

最近Coqをかいていて、まぁ自分は基本姿勢として「CoqにはProof Assistantの方向性として共感できないのでもっとよいものが出てきて早く駆逐してほしい」だったのだけれど、
たくさん書いてると多少偏見もなおって考えを改めたりした部分があるのでまとめることにした。

Agda/Lean/Isabelleの経験がそれなりにある人間から見た、「あのとき知りたかったCoqのハナシ」という
誰にウケるのかわかんない感じで書くけど「Agdaしか使えないけどCoq気になる」みたいな人間(いるのか?)がもしいたら参考にしてください。

強み: 圧倒的implicit parameterの強力さ

implicit parameterの推論は本当にヤバイぐらい強力でAgdaなどハナシにならないのでめっちゃ楽。
おそらくほぼ最大限の推論をしてくれる

あとCoercionとかも結構強いので積極的に使っていこう

Ltacを使うことのキモさ

Ltacはキモいわかるって感じなんだけど、別にそんなたくさんのtacticsを使い分ける必要はあんまりなくて
挙動がよくわからん謎のtacticsは使わなくてもまぁ大丈夫なので多分ナントカなると思う。

自分は実際intro, destruct, apply, rewrite, exists, constructor, refineぐらいしか使ってない。
もちろんたくさん覚えておくと便利なんだろうけど無理して使わなくても
案外なんとでもなるなと。(これは後述するreasoningを使っていることにも関係してる)

ssreflectとかよくわかんなくて使ってないけど別に困ってないので、
キモい証明を生成したくない人は使わなくてもいいんじゃないでしょうか。

Notation, 特にEquational Reasoningに関して

今やってるのが圏論なのでそれ特有の話題にはなるけど、
Notationは意外と強力で(Isabelleとかと比べても遜色ないぐらい)結構自由に定義ができる。

上手く使うとEquational Reasoning(一個前の記事とか参照)もちゃんと定義できたりするので
このへんを使うと意外と読みやすい証明がかけたりする。

証明の読みやすさ

上の話とも関連するけど、具体的に定義を与えるときはできる限り構成をわかりやすく見やすくする工夫をすると証明が読みやすくなるかもしれない。
例えば上のようにNotationを上手く使うとか。

もちろんtacticsベースな以上どうしようもない部分はあるけど。
割り切りは大事。

hole system

Agdaだとholeが作れてアレが案外便利なんだけど
Coqで若干近いことができるrefine tacticというのがある。

refineはhole(_)つきのtermを渡すことができて、その下でholeの部分の証明を要求される。
つまりhole以外の部分をまず埋めてからholeの部分を証明するということができるので
証明をsmall-stepに分割できる。

上手く使うとhole感出て便利。

CIC <-> Ltac

CICからLtacへの変換(正確にはCICのtermを適用して証明をする)はexact tacticを使えばいい。
逆にLtacをCICのtermにするにはltac: (...)と書くといい。

上手くやるとLeanみたいに複数の証明手法を混ぜて証明がかける。

auto command

Coqのauto系コマンドは雑魚です。
ほぼ役に立たないと思ったほうがいい。

Agda/Leanユーザーへ: 君のところの言語もautoはゴミ同然でしょ
Isabelleユーザーへ: ようこそauto縛りの世界へ(dependent typeベースだからしゃーないので諦めて)

sledgehammerほしいめっちゃわかる。

Text Structure

すごく長い証明を一歩ずつ進めたい場合。

Sectionを上手く使おう。
定義や定理のまとまりをSectionで分けて組み合わせていくといい。

Agdaでいうmodule相当の機能だけど、Agdaでいうwhereがないのでこういう感じになる。

performance

いい感じ。
ファイルごとにコンパイル(?)してるだけあってロードも早いのでちゃんと実用に耐えうるレベルに来ている感じがある。

環境

ProofGeneralにcompany-coqを入れるのが多分最強。
emacs使わない人は知らない。

Unicode Symbols

実はあまり知られてないことだけどUnicode symbolは普通に使える。(今すぐRequire Import Utf8.しよう)
Agda-userはProofGeneralのinput methodをagda-inputにするのもいい。
company-coqはTeXっぽいunicode input methodを提供してくれるのでこいつでも十分いい感じ。

特にAgda/Isabelleユーザーはせっかくなのでバリバリ使おう。

Formalization of Setoids-enriched category theory

最近書いてるCoqの話。

主にこれの解説をします:
Yoneda.v · GitHub

Setoidをベースにすることについて

多分圏論formalize業界(狭そう)では有名な話。
Coqの場合はSetoidのequalityに対してもrewrite tacticが使えるのでそれでやる。

Proper

Setoid morphismをここではMapoidとよぶ.
Mapoidは写像(underlying set間の写像)でsetoidのequalityを保つもの.

Structure Mapoid (S S' : Setoid) :=
  {
    mapping :> S → S';
    is_mapoid :> Proper (equality ==> equality) mapping;
  }.
Existing Instance is_mapoid.

ここでのProper (equality ==> equality) mappingがそれで、
意味としてはmappingなるfunctionによってequality relationがequality relationに写ることを表す(==>はrelationのimplication).

Proper (R ==> R') fの元で、rewrite : a R b ~> f a R' f bなる書き換えができるようになる*1のでここではExisting InstanceによってこのPropernessをトップレベルに展開している。

Proper Instance

さて上のようにProperについてのinstanceを使わないとrewriteはできないので、例えばa == bからP a == P bとするにはPがProperであることを証明する必要がある。

上のコードでは、新たに定義したS ** S'(setoidの直積)のconstructing function Spair : S -> S' -> S ** S'がProperであることなどは自力で証明を書いて補っている。

rewriteが効いて欲しい場所で効かない場合はProperのinstanceをかこう。

Category, Functor, Natの定義

圏の定義その他については

github.com

などが参考になる。

ただしCat_on_Coqでは平易に書き下しているようなPropernessも、上のコードでは「おおもとの定義」では全てSetoid上で作るようにしてある。

つまり、例えばcategoryの定義は

Structure Category :=
  {
    object :> Type;
    morphism : object → object → Setoid;
    identity : forall {x}, carrier (morphism x x);
    compose : forall {a b c}, morphism b c ** morphism a b -⇒ morphism a c;
    is_category :> Is_Category (@identity) (@compose);
  }.

となっていて、composeは2つのSetoidの直積からSetoidへのmapoidになるように定義してある。

あるいはfunctorのarrow partも同じようにfmorphism : forall {a b}, @morphism fdom a b -⇒ @morphism fcod (fobj a) (fobj b);などと、hom-setoidの間のmapoidであることを要請している。

こうするとcategoryやfunctorの定義の中に「〜のproperness」のような条件がいちいち現れてこないので、「表面上は」通常の圏論でfunctionとされている場所をmapoidに置き換えるだけでいい。

あるいは、ここではすべてSetoids-enriched category theoryをやっていると思えばいいので理論的にはすっきりする。

ただしcategoryのinstanceを与える際にいちいちmapoidで定義するのは面倒なので(データを定めてからmapoidであることを証明する、という順番で行きたい)、上のコードではsetoidベースでない(条件ベタ書きの)categoryも定義しておいて相互変換できるようにしている。

このやり方だとコードが多少長くなるのでこれが嫌な場合はCat_on_Coq方式でいいと思う。

Equational Reasoning

Agdaに毒された自分のような人間はequational reasoningがないと死んでしまうのでNotationで用意した。

参考:

gist.github.com

使用例:

Notation "`begin p" := p (at level 20, right associativity).
Notation "a =⟨ p 'at' C ⟩ pr" := (@Equivalence_Transitive (@morphism C _ _) _ _ a _ _ p pr) (at level 30, right associativity).
Notation "a =⟨ p ⟩ pr" := (@Equivalence_Transitive _ _ _ a _ _ p pr) (at level 30, right associativity).
Notation "a ↓⟨ p ⟩ pr" := (a =⟨ p ⟩ pr) (at level 30, right associativity).
Notation "a ↑⟨ p ⟩ pr" := (@Equivalence_Transitive _ _ _ a _ _ (@Equivalence_Symmetric p) pr) (at level 30, right associativity).
Notation "a `end" := (@Equivalence_Reflexive _ _ _ a) (at level 30).


(* 例 *)

...
exact (`begin
      fmap H f ∘ (β a ∘ α a)
     =⟨ ltac: (rewrite <- assoc_of; reflexivity) ⟩
      (fmap H f ∘ β a) ∘ α a
     =⟨ ltac: (rewrite (naturality_of β); reflexivity) ⟩
      (β b ∘ fmap G f) ∘ α a
     =⟨ ltac: (rewrite assoc_of; reflexivity) ⟩
      β b ∘ (fmap G f ∘ α a)
     =⟨ ltac: (rewrite (naturality_of α); reflexivity) ⟩
      β b ∘ (α b ∘ fmap F f)
     =⟨ ltac: (rewrite <- assoc_of; reflexivity) ⟩
      (β b ∘ α b) ∘ fmap F f
     `end).

ちなみにltac: (...)と書くとLtacで作った項をCICの項に変換できるので、
reasoning中ではtacticとproof termを混ぜて使うことができる。

意外と便利。

これを使って思ったこととしては、やっぱりAgdaのようなhole推論機能がないと若干苦しい(エラーメッセージからどの部分までreasoningが上手く行っているかを推測する必要がある; ただし慣れればできるようになるため問題ないとも言える)。

しかし読みやすい証明のためには致し方ない。

感想

Universe Polymorphism バンザイ!!!
setoid_rewrite バンザイ!!!!!!
equational reasoning バンザイ!!!!!!!!!!!!!!!!

*1:たぶん…これあってる?