読者です 読者をやめる 読者になる 読者になる

Just $ A sandbox

プログラミングと計算機科学とかわいさ

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ともみなせるのでなんか意味はありそう.

圏論的な解釈を考えると自然にでてくるんだろうか. 謎.

gist.github.com

参考