日々の流転

λ. Howto translate combinators into CPL

こないだのアイディアをもう少し整理して、具体的に翻訳を定義してみた。memo-0125.pdf

このメモを書いてから気が付いたのだけど、CCCは型付きλ計算のモデルなので、翻訳できるのは当たり前といえば当たり前なのか。

……というあたりで更に気が付いたのだけど、この翻訳結果にβ変換等の簡約規則に対応する書き換え規則を定義してやって、書き換えの間で対応が保存されている事を示せば、CCCの上で型付きλ計算のモデルを具体的に作ったことになるよね?

CCCが型付きλ計算のモデルであることの証明の中身自体は全然知らなかったので、自力でここまで到達出来たのは嬉しい。