なんか、沖縄とっても寒い〜
学生の方が一段落したので、いつものように Agda いじってるんですが。今回のお題は否定。有限の射を持つ圏、つまり、たんなるグラフがうまくできなくて、
* 存在しない射に対する結合則とかは、矛盾⊥ から導くのが良いんじゃないか?
ってことで、否定について調べてたんですが、
Nope : (m n : ℕ) → Set
Nope (suc _) zero = ⊥
Nope _ _ = ⊤
nope : ∀ m n → m ≡ n → Nope m n
nope zero ._ refl = _
nope (suc m) ._ refl = _
peano : ∀ n → suc n ≡ zero → ⊥
peano _ p = nope _ _ p
http://stackoverflow.com/questions/22580842/non-trivial-negation-in-agda
とかあって、結構面白い。
なんですが、
even : ℕ -> Set
even zero = ⊤
even (suc zero) = ⊥
even (suc (suc n)) = even n
div : (n : ℕ) -> even n -> ℕ
div zero p = zero
div (suc (suc n)) p = suc (div n p)
div (suc zero) ()
とかいうのもあって。()ってなんだ?
¬_ : Set → Set
¬ A = A → ⊥
data Dec (P : Set) : Set where
yes : P → Dec P
no : ¬ P → Dec P
EvenDecidable : Set
EvenDecidable = ∀ n → Dec (even n)
isEven : EvenDecidable
isEven zero = yes _
isEven (suc zero) = no (λ ())
isEven (suc (suc n)) = isEven n
http://stackoverflow.com/questions/18347542/agda-how-does-one-obtain-a-value-of-a-dependent-type
とかやるらしく。起き得ない入力の組合せみたいなものらしい。Agdaが、これは起きないと理解してくれれば使えるらしいです。
つまり、A x B x C -> D みたいな関数で、A/B/Cのすべての入力について関数を定義する必要はないらしい。そういえば、data で規定された範囲しかみたいなみたいなことはやっていたな。どうせ、矛盾を取れる部分は規定された範囲外なんだから、実は除外できるんじゃないか?
今までは存在しない部分は Maybe で nothing とかやっていたんですが、それがいけなかったかも。で、演算定義とか結合則とから、いろいろ抜いていくと、
あれ? なんかできるじゃん
どうも、Maybe とかで record の中に入れ込んだので、Agdaが理解してくれなかったっぽい。
というわけで、要素2の圏を記述はきれいになりました。
なのだが、その後の Limit から Equalizer の証明には、はまりました。でも、定義を二重に入れてしまって、それの同一性が取れなかっただけで、定義を一部外に出したらできた。
http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/kono/Proof/category/file/fd79b6d9f350/discrete.agda
結構、苦労していたのができて、ちょっとうれしいです。
http://seeker-s-eye.blogspot.jp/2017/01/agda.html
No comments:
Post a Comment