名無し項に直しているだけ

なんか 1 日中寝ていた気がする.

単純型付きラムダ計算の CCC (Cartesian Closed Category) の意味論が,地味に Semantics of Programming Languages: Structures and Techniques の圏論の章に載ってて,読み直しているんだけど, Var と Abs と App しかない至極単純なラムダ項を考える限り,表記上は結局 DeBrujin index による名無し項に直しているだけだなということに気づいて面白かった.まあもちろん,それが圏の操作と対応付いているというのが重要で本質なんだけども.うーん,でもやはり意味論は不動点を使い始めてからが面白くなる話な気がする.

閑話休題.そのうちきちんと感想を書こうかとか思っているけど,ふと見始めた某ドラマが面白い.道徳の時間に見せられるビデオみたいな感じになってもおかしくない題材だけど,丁寧に差別的な表現を取り除きつつ,王道的に面白い感じになってる.これ脚本書いた人とかちょっと只者じゃないのではという感じがする.