Girard-Reynolds isomorphism

parametricityというか、logical relationって、まあ話の流れは追えるけど、どうも直感的にピンとこない。てことで、WadlerのGirard-Reynolds isomorphismを読んでみた

(自然数に対する)数学的帰納法は、P2では、
Nat(k) = Forall P.(forall n.P(n) => P(succ n))=>P(zero)=>P(k)
のように書けて(Forallはsecond-order quantification,forallはfirst-order quantification)、Girard projectionによって、F2の型
polyNat = forall a.(a->a)->a->a
が得られる。んで、これをReynolds embedding(Reynolds embeddingの定義はWadlerの論文の最後の方)でP2の命題に戻すと
R[forall a.(a->a)->(a->a)]
= \k -> Forall P.R[(a->a)->(a->a)](k)
= \k -> Forall P.(forall s.R[a->a](s) => R[a->a](k s))
= \k -> Forall P.(forall s.(forall n.P(n)=>P(s n))=>(forall n.P(n)=>P*1=>(forall m.P(m)=>P(k s m))
が得られる。便宜上、P(k)みたいな命題を、P=(\k -> P(k))みたく、ラムダ式で書いた

で、こんとき、Nat'(k)からNat(k)は言える気がする。sをsuccにmを0に特殊化して、自然数nのチャーチエンコーデイングが単に関数をn回適用することだというのを思い出すと、Nat'(k)からNat(k)が得られる(ということでいいんだろうか)。んで、逆はP2では言えないんだろう。一般にP2の命題をGirard projectionして、Reynolds embeddingで戻すと、常に、元の命題より強い命題に移るんだろうか。逆に、F2の型をembedding->projectionすると、得られる型は元と同じ。

そうなる理由(の一部)は、P2はF2のCurry-Howard像より広い体系だからってことだろうか(Wadlerの説明によれば、P2は一階の量化子も含むが、F2は二階の量化子しか含まないから)。んで、extensionalityという制限をP2に加えると、この体系は、F2と（Girard-Reynolds isomorphismを通じて)完全に同等になるってこと?

まだよくわからんな。Mairsonの論文でよく分からなかったとこは大体理解できたけど、新しい謎がいくつか。そもそも、F2のCurry-Howard像ってなんだ?

*1:k s) n))) となって、 Nat'(k) = Forall P.forall s.(forall n. P(n)=>P(s n