今回は偏見の記事です。 サンデーうぇぶりというアプリで高橋留美子先生の作品を一日一話ずつ読んでいる。その作品というのは「うる星やつら」と「らんま1/2」と「犬夜叉」である。私は「めぞん一刻」は何度も読み返しているのだが、この三作品は一度もちゃ…

Troelstra先生とSchwichtenberg先生*1の"Basic Proof Theory"もまあ必読書なのでしょうな。頑張ります。 単純型付ラムダ計算の代入補題についてメモ。 代入は以下のように項の複雑性によって帰納的に定義される。 , （ でないとき*2）, , , （ でないとき。w…

Awodey先生は「アウディ」と読むらしい。数学者・数理論理学者であり数学の哲学者*1でもある。こういう人はすごいと思う。「数学の基礎付け」なんてのはいまや死語かもしれないけれど、圏論は型理論との相性が良くて、計算機科学を考慮した新機軸がいろいろ…