トップ «前の日記(2006-12-13) 最新 次の日記(2006-12-15)» 月表示 編集

日々の流転


2006-12-14 騏驎も老いては駑馬に如かず [長年日記]

λ. Domain Theoretic Models Of Polymorphism by Thierry Coquand and Carl A. Gunter

読みかけ。

cocontinuous な functor F: C→DEP から、Grothendieck construction で圏 ΣF と射影 p:ΣF→C を定義する。CがdomainならΣFもdomainになっている。pのcoconitnuousなセクション C→ΣF とその間の自然変換からなる圏を ΠF とする。Cがdomainなら ΠF もdomainになっている。

CをDEP自身とする。このときΣFは半順序集合にならない。ΠFは半順序「集合」にはならずクラスになるが、圏同値なdomainが存在する。このΠを使って多相型を扱う。

このモデルはuniformに振舞わないような多相的な要素を含む。 admissibleな関係に限定した場合のparametricityは……やっぱり成り立たないのかな?*1

Tags: 論文 圏論

*1 もし成り立つのであれば Shortcut fusion is correct はインパクトを持たない気がするし

λ. 凄い漢字

<URL:http://www.rubyist.net/~matz/20061204.html#p02> にツッコミをいれようとしたら、spamフィルタに弾かれたみたいなので、こっちに。その「うしのあゆみがおそい」はU+3E2A(「㸪」)として既に含まれているような。