https://twitter.com/kinaba のログ (twilog の方が便利です。)
| Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega https://t.co/BSjm87Nydg まだLtUの記事しか見てないけどかなり楽しそう。SystemFの自己インタプリタ | |
| https://t.co/3Ec2YpHkpF おおー、Ralf Hinzeこのテーマで論文書いたんか https://t.co/RFDz2swlJI 知らなかった！！ていうか The Beauty of Functional Code というお誕生日論文集丸ごと面白そうですね | |
| FωでFωする話 https://t.co/BSjm87Nydg 半分読んだ。まずインタプリタとは"λ項を表現したλ項"を適用しβ正規化すると元のλ項の正規形になる関数のことただし"λ項を表現"する先は必ず正規形で"表現"はinjectiveでないと駄目、として自明解を弾く。(続 | |
| 続) 言語自分自身のインタプリタ書くと普通は対角線論法によってインタプリタにインタプリタを自己適用してうにゃうにゃした結果が計算できるとすると矛盾なのでその計算は決して停止しないみたいなことが言えるので、型付λのような"必ず停止する体系"では自己解釈できないとされたものだが (続 | |
| 続) 「対角化してうにゃうにゃ」し始めるとすかさず型エラーを引き起こして殲滅するように表現とインタプリタを作るとどうにかなる、と。"表現"の詳細まだ読んでないけどHOASで巧くやるということなのでそもそも型付けが通るような項しか表せないような表現にするとそういうことになるんだろう | |
| @chiguri インタープリタ自身はFωの普通の項なので含まないとFωのインタプリタできたと言えないので含むんですが、「インタープリタに対角線的に何かを食わせる関数」の定義域にその「何かを食わせる関数」のencode先termがなければ避けられるとかそんな感じぽいです |