クイズの答え
http://d.hatena.ne.jp/sumii/20060219/1140346031の答え。http://d.hatena.ne.jp/namasute0/20060220#1140366627の追記を参照。僕が見た中では最も早い解だったので。OCamlで書けばわりとすぐにわかるけど、多相λ計算だけ見てるとhttp://d.hatena.ne.jp/wpw/20060219/1140361837みたくキレイに罠にはまるかも。
背景:デレックがピッツと僕に「この文脈等価性を貴様の理論で証明できるか? できないだろう!(反語)」みたいなメールを送ってきて、ピッツが「ナイスな例だ」とか言ったので、「はあ?」とか突っ込みを入れた訳です(嘘)。
その後も絡まれて、3回目ぐらいに
v1 = pack (nat, λf:nat→nat. f(0)=0 ∧ f(1)=1 ∧ f(2)=2) as τ v2 = pack (bool, λf:bool→bool. f(true)=true ∧ f(false)=false) as τ where τ = ∃α.(α→α)→bool
という例が出て、文脈等価かどうか誰も証明/反証できない(←今ココ)。OCamlで書くと
module type T = sig type t val g : (t -> t) -> bool end module V1 : T = struct type t = int let g = fun f -> (f 0 = 0) && (f 1 = 1) && (f 2 = 2) end module V2 : T = struct type t = bool let g = fun f -> (f true = true) && (f false = false) end
に当たるんですけど。この=はpolymorphicじゃないので注意。