日々の流転

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

を読了。

λ. 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のようなより扱いやすい形が必要になるのではないかと思った。

参考:

• <URL:http://sakura.math.kyushu-u.ac.jp/algi/09/program.html>

関連エントリ

• 強い直和?

【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)

λ. 実写版エヴァンゲリオン？

をぐまさんのmixi日記より。良くできてるなぁ。

• <URL:http://www.youtube.com/watch?v=75GoCvuB8Ow>
• <URL:http://www.youtube.com/watch?v=mRB2woVxcQ4>