2006-05-18 [長年日記]
λ. John Major's equality
最近のAgdaにはagda-show-contextというコマンド(キーバインディングは「C-c |」)が実装されていて、これを使うと現在のコンテキストから見えるシンボルの一覧が表示できる。で、何も読み込んでいない状態で、これを実行してみたところ、幾つかの基礎的なデータ型やモナドと一緒に以下のようなシンボルが表示されているのを見つけた。
JMeq :: (A::Set) -> (x1::A) -> (B::Set) -> (x2::B) -> Set same :: (A::Set) |-> (x1::A) |-> JMeq A x1 A x1
どうやらJMeqの唯一のデータ構築子(あるいは導入規則)がsameのようだが……これは何じゃ!? JMeqで検索してみると、Coq-Clubメーリングリストの[Coq-Club] Playing with equalityというスレッドが見つかった。
なるほど。予め型が等しいと分かっていない二つの値を等号で結ぶための型で、(inductive familyとしての)通常の除去規則とは異なった除去規則を持っている。そして、通常の等号の型IdにUIPを追加したものと等しいと。この辺りから想像がつくが、内包的な型理論の内部では定義出来ない。そこで、CoqのCoq.Logic.JMeqではAxiomを使って定義している。agdaでもpostulateを使って同様に定義する方法もあったと思うが、agdaは組み込みの型としてJMeqのパターンマッチを特別扱いしているようだ。JMeq A a A aのような型の値には通常はcaseが使えないようチェックされているが、JMeqの場合には引っかからずにcaseが使えるできる。
それから、John Major's equality という名前が最初に使われたのは C. Mc Bride 氏の PhD thesis の Dependently Typed Functional Programs and their proofらしい。そのページのp.119に由来が書いてあった。John Major ってどっかで聞いたことのある名前だと思ったら……
It is now time to reveal the definition of ≃, the ‘John Major’ equality relation.2 John Major's ‘classless society’ widened people's aspirations to equality, but also the gap between rich and poor. After all, aspiring to be equal to others than oneself is the politics of envy. In much the same way, ≃ equations between members of any type, but they cannot be treated as equals (ie substituted) unless they are of the same type. Just as before, each thing is only equal to itself.
2 John Major was the last ever leader of the Conservative Party to be Prime Minister (1990-1997) of the United Kingdam, in case he slipped your mind.
classless society ってメージャー首相の言っていたいわゆる「階級なき社会」ってやつですね。それから、Epilogue に書いてあった「telescopic」という言葉についても p.120 に書いてあった。
