2005-09-28 [長年日記]
λ. signature の equality に???
β変換すれば同じになるはずの(signatureで定義された)型が同一と見なされなくて、困ってしまった。例えば以下のコードのtestの定義では、「fm A (f x)」と「fm (Ty_m f A) x」はβ変換すれば同じシグネチャになるので、一見して型チェックは通りそうに見える。だが、実際には「t has type fm A (f x) but should have type that is equal to fm (Ty_m f A) x」と型エラーになってしまう。
Ty_o (X::Set) :: Type
= X -> Set
Ty_m (|X,|Y::Set) (f::X->Y) (A::Ty_o Y) :: Ty_o X
= \(x::X) -> A (f x)
fm (|X::Set) (A::Ty_o X) (x::X) :: Set
= sig
c :: A x
test (|X,|Y::Set) (|A::Ty_o Y) (f::X->Y) (x::X)
(t::fm A (f x))
:: fm (Ty_m f A) x
= t
半日ほど悩んだ結果、この型エラーはfmの定義を以下のように書き換えれば回避出来ることに気づいた。しかし、このように書き換えなくてはならないのは直観的でないし、それに参照透明でもないように思う。何故このようになっているのだろうか?
fm' (Ax::Set) :: Set
= sig
c :: Ax
fm (|X::Set) (A::Ty_o X) (x::X) :: Set
= fm' (A x)
【2006-05-03追記】 「薔薇色の明日」の「Agdaの型チェック通らず」というエントリで書かれていた以下の話(パーマリンクが機能していないようなので勝手に引用)は、ひょっとして同じことで悩んでいるんじゃないかという気がする。
Agdaでちくちくと証明を実装していたのだが、エラーメッセージによると型が合っていない。しかし、私の記述は、システムが「この型であるべきですよー」という型の略記でしかないので、普通は同じ型とみなしてくれてもよさそうである。
仕方がないから先生にお尋ねしたところ、「ここを変えてみたら？」という助言のままに書き換えたところ、エラーメッセージが変わった。「ここは型Aと記述されてますけど、型Aになるように記述しないと駄目ですよー」と。
λ. JORDAN曲線定理の完全証明が完成！
think physically about computation. think computationally about physics. (2005-09-28) より。へぇ、Mizar使ったのか。
