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

日々の流転


2006-05-16 [長年日記]

λ. Towards Observational Type Theory. Thorsten Altenkirch and Conor McBride

Extensional Equality in Intensional Type Theory の話を発展させたもの。前の論文では proof irrelevance が本質的な役割を果たしていると思っていたが、実際にはそれほど本質的ではないというのにまず驚いた。

(詳しくは後で書く)

OTTは理論的にも面白いし、実用的にも便利そうな型理論だと思う。Epigramを使ってみたくなった。

λ. 高校の勉強ムズス

  • 接弦定理なんて知らね
  • 漢文の返り点の結合順位を誰か教えてくれ