Agda で DAG

DAGは、ループのないグラフですね。

Agdaで否定やろうかどうしようか考えていて、まぁ、考えてるってことはやるんだけど、例題が何かいいものあれば。この前は対偶だったけど。

で、結局、突破したのは discrete な圏つまりグラフだったので、グラフがいいかなと。

授業の前の昼飯の前には片付かなかったんですが、授業の後でできました。ちょっとうれしい。

Agda の data で List みたいに direct につながっている奴、indirect につながっている奴を作るってのを思いついたら、あとは割と一直線でした。

いや、うそだな。場合分けの書き方が謎すぎる。当てずっぽうっぽい。

　　 dag : { V : Set } ( E : V -> V -> Set ) -> Set
　　 dag {V} E = ∀ (n : V) → ¬ ( connected E n n )

とか書けるので、それっぽい。

Agda もう少しメタ計算したいんだけどな。この場合分けを自動生成するとかはやってはくれるんですが、埋めるのは人手。埋める所まで自動化して欲しい所。Coq だとそういうのがあるらしいが...