トップ «前の日記(2004-03-31) 最新 次の日記(2004-04-04)» 月表示 編集

日々の流転


2004-04-03 [長年日記]

λ. Polymorphism is not set-theoretic

を読んだ。Polymorphic lambda calculus の集合論的なモデルが存在しない理由をこれまで vicious circle のためだと思い込んでたのだけど実は違った。集合の圏ではPと(P->B)->Bが同型にはならないのが原因。

Tags: 論文 圏論
本日のツッコミ(全4件) [ツッコミを入れる]
ψ so1 (2004-04-06 23:55)

えーっと、コレ↓に出てくるcoherence spaceを使った表示的意味論は集合論ベースじゃないってコトなんですかね?まだそこまでやってないのでわかんないんですけど。<br><br>http://nick.dcs.qmul.ac.uk/~pt/stable/Proofs+Types.html

ψ さかい (2004-04-08 18:24)

ここでの話は、集合の圏そのもので解釈出来るかという話なので、coherence space を使った表示的意味論が集合論ベースかどうかとは直接は関係ないと思います。<br><br>> http://nick.dcs.qmul.ac.uk/~pt/stable/Proofs+Types.html<br><br>coherence space が出てくるということは、線形論理の上で話をしてるんですね。<br>Girard だもんなぁ...

ψ あぁ〜 (2005-02-05 15:20)

あぁ〜なんでやねん

ψ さかい (2005-02-08 06:29)

なんでやねん、と言われても〜