日々の流転

λ. 第三十四回圏論勉強会

今日は圏論勉強会だった。 “Categories, Types and Structures” Section 2.3.6 Propositionより

写真

【2007-11-13追記】 Proposition 2.3.6 では reflexisive object V に V×V を埋め込めることを示すために、非常に面倒くさい計算をした。 CCCの射として明示的に書き下しているので煩雑すぎて本質が見えにくかったが、落ち着いて考えてみれば簡単で、CCCのinternal languageとしてラムダ計算を使うならば、単に直積型のチャーチエンコーディングに過ぎない。

関連

• 圏論勉強会 - たけをの日記＠天竺から帰ってきたよ
• デカルト閉圏におけるお絵描き計算の基礎 - 檜山正幸のキマイラ飼育記

λ. seqはHaskellの意味論では扱えない?

• <URL:http://alohakun.blog7.fc2.com/blog-entry-812.html#comment1712>
• Haskell: seqってよくわからない - lethevert is a programmer

seqの意味がHaskellの標準的な意味論で扱えないかのように思われがちなのは何故だろうかと思った。

【追記】 lethervertさんの場合は、Haskellの公式の意味論でseqの操作的意味を確定出来るかという疑問だったので、実際には違う話ではあったけど。