https://twitter.com/kinaba のログ (twilog の方が便利です。)
"An operational semantics for Scheme" http://dx.doi.org/10.1017/S0956796807006478 のイントロを読んだりしている。 | |
一言で言うと「表示的意味論むずかしい」。特に非決定性を表現するときとか、(引数の評価順序etcのために返値がvalueじゃなくてsetになるのが著しく面倒いとかかな)、type soundness が操作的意味論ならずっと楽に証明できたのに…みたい文献が引かれている | |
"denotational semantics requires much more mathematical sophistication"。dynamic_wind とか eval とかをR5RSの意味論の発展系で真剣にやろうとすると死ぬみたいなのも引かれている | |
@m0h1can 僕も知りたいです。実行委員のひとに聞いてみよう… | |
http://en.wikipedia.org/wiki/Type_safety "Type Safety = Progress + Preservation" という操作的なアプローチ/証明技法/定義とがもの凄く成功したので、そゆ風に使うことを考えるなら現状操作的意味論が楽。 | |
で、あとはそーゆー風に使いたい人が今のSchemeの仕様をdriveしている |