Thursday, 15 August 2013

外延性

昨日も(っていうか今朝まで) Agda いじてっていて、なんか珍しく口内炎くらいました。

Monad のいつもの例題をいじっているだけ。しかも、

* T : A -> M x A ( A は集合、Mは Monoid 、x は直積)

という極めて簡単なものなんだけど、ある意味で簡単なものほど難しいものだよね。こいつは Haskell では簡単に書けたのに、
Agda では、まったく歯が立たず。 http://seeker-s-eye.blogspot.jp/2013/08/monad.html

Haskell にそって data とかを定義して、それを圏にしてとかいうのは、途中まで頑張ったのですが、どんどん違う方向に
いってしまう。でも、そこで Monoid の要素が Carrier という名前の Set だというのがわかりました。

そこで、最初の頃に作った、Sets (既に定義されている圏で、射が Agda の関数 ) と直積を組み合わせる方向に戻って、
みたら、あっさり、T と ηとμが定義できた。しかも、

*  結局、教科書に書いてあるとおりの定義

いや、もちろん、そうでなければならないんだけどさ。

* FObj = λ a → (Carrier Monoid) × a
* TMap = λ a → λ(x : a) → ( ε , x ) ;
* muMap a ( m , ( m' , x ) ) = ( m m' , x )

なんとなく、信用してなかったようです。で、そこから楽勝。だと思ったのだが、Monad の性質を満たすことの証明が、まったくできない。全然できない。

* ( λ x → (( ε (proj x)) , proj x )) = ( λ x → x )

を示せば良いだけで、εが Monoid の単位元で、( ε (proj x)) が (proj x) を返すとわかれば、

* ((proj x) , proj x ) = x

つまり、直積はその成分の直積だってことで、これ自体は簡単。なんだけど、どうしても証明できない。λ x -> x のλ x を
cong で構成するとかやってたのに歯が立たず。で、証明できない式自身、

* (f x ≡ g x) -> (( λ x -> f x) ≡ (λ x -> g x)

でググってみたら、

http://math.stackexchange.com/questions/154704/if-fx-gx-for-all-xa-why-is-it-not-true-that-lambda-x-fx-lambda
* If f(x)=g(x) for all x:A, why is it not true that λx.f(x)=λx.g(x)?

え? 証明できないの? はぁ?

http://homotopytypetheory.org/2011/04/23/running-circles-around-in-your-proof-assistant/
* function extensionality

というものらしい。

* ∀x -> (f x ≡ g x) -> f ≡ g

ってのを公理して仮定しろと。確かに、Agda の library にも仮定(postulate)するように式が書いてある。超良くある質問らしいです。

そう言われて見ると、ZFの 外延性の公理 (extensional principle )

* ∀ {x} x∈ f ⇔ x ∈ g → f ≡ g

と(要素がすべて同じなら同じ集合)にクリソツ。これを仮定したら、ちゃんと証明出来ました。朝の5時に。あだだだ。 これも元の本では三行なんだよな。
Post a Comment