2006-12-11 [長年日記]
λ. Shortcut fusion is correct by Patricia Johann
以前から読まなくちゃと思ってはいたのだけど、<URL:http://d.hatena.ne.jp/m-a-o/20061206#p1>で見かけたのをきっかけに読んでみた。操作的(operational)なモノの見方に慣れていなかったので苦戦。証明は追えたけど、いまいち実感がわかない。
TT-closedness の定義は面白い。 スタックの関係と項の関係の間の sT⊇s ⇔ r⊆rT という随伴から定義されるclosure。
「lazy PolyPCF」の lazy の意味は lazy λ-calculus (20040102#p03 を参照)のと同じ意味。lazy PolyPCF を扱うには、Free Theorems in the Presence of seq でのように inequational logical relation にすればよいのだろうけど、もう結果は出てるのかな?
結局、operational に考えることのメリットは何か? impredicative polymorphism があるとモデルを考えるのが大変なのに対して、operational semantics と contextual equivalence に基づけば、複雑なモデルを考えなくて済むということか? しかし、fix と impredicative polymorphism を持つ言語のモデルで、admissibleな関係に限定したparametricityが成り立つモデルは知られていないのだろうか? もしそのようなモデルが知られているのなら、同程度の労力で short-cut fusion の正しさを示すことは可能であるように思う(TT-closednessを示すのも領域理論的なadmissibilityを示すのも似たようなものだろう)。
