トップ «前の日記(2006-11-08) 最新 次の日記(2006-11-10)» 月表示 編集

日々の流転


2006-11-09 [長年日記]

λ. 『儒教—ルサンチマンの宗教』 浅野 裕一

儒教ルサンチマンの宗教 (平凡社新書 (007))(浅野 裕一) を読了。

Tags:

λ. The Theory of Parametricity in Lambda Cube by 竹内 泉

Fωでのparametricityについて興味があったので読んでいるところ。ただ、higher-order polymorphism に対する parametricity は扱いにくいように思う。おそらく、Folds, Church Encodings, Builds, and Short Cut Fusion for Nested Types: A Principled Approach でのhfoldに対してのgfoldのようなより扱いやすい形が必要になるのではないかと思った。

参考:

関連エントリ

【2006-12-20 追記】 Definition 3.17 (Conformity Relation) では、αが種のとき「 <ΠX:α. P>{θ} = ∀X1:αθl, X2:αθr. ∀Y:(|X:α|)lr,(X1,X2)/X}. <P>{θ,(X1,X2,Y)/X} 」と定義しているけど、Tが型のときの「<Πx:T. P>」と同じで「 <ΠX:α. P>{θ} = λy:(ΠX:α. P)θl, z:(ΠX:α. P)θr. ∀X1:αθl, X2:αθr. ∀Y:(|X:α|)lr,(X1,X2)/X}. <P>{θ,(X1,X2,Y)/X} (y X1) (z X2) 」と定義しないとまずいはず。そうしないと、Definition 3.9 (Kind of Conformity Relation) と種が一致しない。

このように定義を修正すると、例えば、

Nat : (*->*)->(*->*)->*
Nat = λF,G:*->*. ΠX:*. FX->GX

の Conformity Relation は以下のようになり、種がきちんと一致する。

  • <Nat> : (|Nat|)
  • (|Nat|) =
    ΠF1,F2:*→*, FR:(ΠX1,X2:*. (X1→X2→*) → (F1 X1 → F2 X2 → *) ).
    ΠG1,G2:*→*, GR:(ΠX1,X2:*. (X1→X2→*) → (F1 X1 → F2 X2 → *) ).
    (Nat F1 G1) → (Nat F2 G2) → *
  • <Nat> =
    λF1,F2:*→*, FR:(ΠX1,X2:*. (X1→X2→*) → (F1 X1 → F2 X2 → *) ).
    λG1,G2:*→*, GR:(ΠX1,X2:*. (X1→X2→*) → (G1 X1 → G2 X2 → *) ).
    λα1:Nat F1 G1, α2:Nat F2 G2.
    ∀X1,X2:*, XR:X1→X2→*.
    ∀x1:F1 X1, x2:F2 X2.
    FR X1 X2 XR x1 x2 → GR X1 X2 XR (α1 X1 x1) (α2 X2 x2)
Tags: 論文