トップ «前の日記(2005-09-14) 最新 次の日記(2005-09-17)» 月表示 編集

日々の流転


2005-09-15 [長年日記]

λ. Propositional equality の証明の equality

Propositional equality の型である Id a b の要素はせいぜい一つしかないので、要素が二つ与えられたらそれらは等しいに決まっている。それを証明したい。が、以下のコードは内側のcaseの部分で「Error in the definition of eqId because: cannot case: exps [x, x] must be distinct variables.」というエラーになってしまう。(e1へのcaseでa,b,xがunifyされているためこのようなエラーメッセージになってる。2005-05-16 の case on non-var でも書いたが、この制約は必要以上に厳しい気がする)

eqId (|A::Set) (|a,|b :: A) (e1,e2 :: Id a b)
  :: Id e1 e2
  = case e1 of
    (ref x)->
      case e2 of
      (ref y)->
        ref@_ (ref@_ x)

Agdaでこの命題を証明する方法はあるだろうか? SET.alfa では Id a b の Collapsed も定義されてないし、やっぱり無理なのか? Per Martin-Löfの Intuitionistic Type Theory でもこれは証明できるので、「Martin-Löf. の型理論に基づく対話型定理証明支援系」と呼ばれているAgdaでこれが証明できないとしたら、納得いかん。

(2005-09-17 追記) Intuitionistic Type Theory は propositional equality type の strong elimination を含む extensional な型理論だから、「Agdaでも証明できるべき」という理由にはならない気がしてきた。というか、私はその辺りの話が全然分かってない。Intuitionistic Type Theory 以降の Martin-Löf 流の型理論を学ぶには何を読めば良いのだろう? Bengt Nordström, Kent Petersson, Jan M. Smith の Programming in Martin-Löf's Type Theory - An Introduction ?

(2006-02-05 追記) Thierry Coquand の Pattern matching with dependent types の p.9 には次のように書いてあった。

By contrast, it is not clear how to represent the following computation rule in term of the usual elimination rules4. We have seen that the unique contextual mapping

{y := x, p := refl(N,x), q := refl(N,x)}: (x : N) → Δ,

is a covering of Δ = x,y : N; p,q : Id(N, x, y). It follows that it is correct to add a new constant f : (x,y : N; p,q : Id(N,x,y))Id(Id(N,x,y),p,q) together with the computation rule

f(x, x, refl(N,x), refl(N,x)) = refl(Id(N,x,x), refl(N,x)) (x : N).


4 This problem has been independently suggested by Thomas Streicher.

(2006-04-18 追記) Michael Hedberg の A coherence theorem for Martin-Löf's type theory には次のように書かれていた。というわけで、elimIdではいくら頑張っても証明できないことになります。証明するにはAgdaに対して何らかの拡張が必要になるでしょう。

Although one might expect the identity sets to be collapse, it is impossible to prove in general that they are, as long as type theory is restricted to the standard elimination rules. This negative result is proved by Hofmann and Streicher [11], using a groupoid interpretation of type theory.


[11] M. Hofmann and T. Streicher. A groupoid model refutes uniqueness of identity proofs. In Proceedings of the 9th Symposium on Logic in Computer Science (LICS), Paris, 1994.

(2006-05-14追記) この「A groupoid model refutes uniqueness of identity proofs」を読んだ。20060514#p01を参照。

Tags: agda
本日のツッコミ(全2件) [ツッコミを入れる]
ψ ikegami (2005-09-17 14:24)

Id にかぎらずあらゆる idata は case できないかわりに elimination rule でなんとかすることになってます。<br>参照: http://www.cs.chalmers.se/Cs/Research/Logic/TypesSS05/Extra/catarina_sl.pdf<br>しかし、ElimId をつかってこれを解くのはそんなに簡単じゃなさそうですねえ、、、思いつく?

ψ さかい (2005-09-17 21:44)

なるほど。case よりも elimination rule を使わせる方針であれば、case の制約が強いのも納得できます。ありがとうございます。<br>で、これなんですが、実はelimId を使った方法も試してはいたのですが、ちょっと考えた限りでは無理っぽい気がします。