週に一回は書きますよ 月に4つ記事を書けばノルマは満たされます。
上記の広告は1ヶ月以上更新のないブログに表示されています。
新しい記事を書く事で広告が消せます。

唐突にcoqで圏論の会に参加表明して行ってきました。 Thanks to mr_konnさん。

<余談>...ツイートリストを修飾するタグが欲しいなぁ。</余談>

実は半年あたり前にちょろっとだけCoqを勉強していたので、そのちょうどいい復習として行ってきました。圏論の知識はあまりありませんでしたがなんとかなった、はずです。

皆で使用していた圏論のライブラリ ConCaT が曲者で、なかなかみんな苦労していました。皆おおよそCategory.vやそこから引用されているMap2.v, Setoid.v などを眺め、書き換えたり写経したりして学習していました。

結果はtogetter「Coqで圏論の会」をご覧ください。

私の成果物は以下のとおり。

1. 要素のない圏

すでにライブラリに要素が一つしかない圏 ONE.v が書かれていたため、それを写経すればおおよそできます。そのため、練習問題として多くの人が書いていました。

私の証明には、なるべくcontradictionを使うようにしています。「異議あり! そもそも前提が狂っている!」と。ZERO.vの定義は以下の行で、要素が何も無いことを宣言するところから始まります。

Inductive Zero_ob : Type :=.

Inductive Zero_mor : Zero_ob -> Zero_ob -> Type :=.

この「何も無い」定義が Falseの定義 と同じだったので、せっかくだからFalseと同じであることをアピールしておきました。

2. Epic Monicに関する練習問題

  • EpicやMonicの合成もまたEpicやMonicである
  • 射の合成がEpic/Monicなら、合成元の射の片方もまたEpic/Monicである。どちらの片方かはEpic/Monicで逆になる。

教科書に載っている簡単な問題です。時間内には結局前半のEpicの側だけ終えました。上のリンクはその後に全部終えたものです。

はまりどころが大量にありました。Zero.vと違い殆ど写経出来なかったのでCoq力が試されたといったところです。

  • =_Sは等式じゃないからrewriteできない。かわりに直接transivitiyことTransをapplyする。
  • f o gf: a-->b, g: b-->c から a-->c を作る。普通の o 演算子と逆。
  • Epic a ba --> b なのにたいし、Monic a ba --> b と逆。

課題と関係なく感心したことを一つ。ONE.v の合成演算子結合則 Comp_One_mor はやることの割に長くて微妙な定義です。ここをもっと簡単にCoqらしく書く方法として、次のように結果の型だけ宣言してしまい、内容は証明で書くという方法があります。

Definition Comp_One_mor (a b c : One_ob) (f: One_mor_setoid a b) (g: One_mor_setoid b c) : One_mor_setoid a c.
Proof.
(省略)
Qed.

こちらのほうが試行錯誤や高度なtacticsの適用を使えるので楽です。このあたり、証明器を補助にプログラムが書けるのはCoqの便利なところだと改めて思うのでした。Coqでプログラムを書くことそのものはかなりの苦行ですが。

スポンサーサイト
上記広告は1ヶ月以上更新のないブログに表示されています。新しい記事を書くことで広告を消せます。