クイズの答え

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じゃないので注意。