type theory with variable-free syntax
(追記) 解決した: variable-free type theoryの圏論的な解釈について - Just $ A sandbox
--
文献に突然登場して？ってなったので.
調べても情報がヒットしないのでよくわからないけど, simply typed lambda calculusを変数を使わずに定義するものらしい.
で, STLCかなんかでうまく解釈できるかと思ったけど思いつかなかった.
まず, 代入が変数に関数値を代入しているのかと思ったらそうじゃないっぽい(合成の順番が逆だし).
さらに適用みたいな記号で書いてるM∙sは何者なんだという感じ.
でも1はde Bruijn indexに従ってcontextの一番近くの型を取り出しているし, 1[↑] = 2ともみなせるのでなんか意味はありそう.
圏論的な解釈を考えると自然にでてくるんだろうか. 謎.
