TaPL読書録 #2
引き続きTaPL読書録です。今回は3.4.まで。
この項の構文は
succ trueやif 0 then 0 else 0のような怪しげな項の形成を許すことに注意されたい(p.18)
怪しげw
「型なし算術式」なのでこの手のものを許可せざるを得ない。
評価のところまですすめたとき、評価の左辺(辺か？)にマッチせず捨て置かれることがわかる。
... この定義は複合的な部分式に付ける括弧の使用について何もいっていない(p.19)
else のない if などが導入された場合に曖昧性が出始める、とのこと。
定義3.2.3.
演習3.2.5. より、 lim のような記法が定義されていれば i -> ∞ における S_i が S と一致するはずだがそのような記法が導入されていないので和集合をとる記法になっているのかな？という話が出た。
深さなのだろうか？ size に関する演算が多く、サイズに関する帰納法なのでは？という指摘があったが、おそらくこれは深さに関する帰納法で正しい。
「t = succ t1 を満たす t, t1 において depth(t) > depth(t1) が常に成立する」 ということを暗黙的に用いて帰納法を用いている、と解釈した。
定理3.3.4. 証明(演習)
しれっと演習がまじっていて気づいていない人もいた。
基本的には補題3.3.3.の証明と同じ形式で進めればよい。のだが、基底部のケースがちょっと不明瞭……
例えば述語 P を iszero とおくと iszero 0 は true であるが、iszero true や iszero false は評価できないので成り立たない1。
しかし、s = true, false, 0 のとき depth(r) < depth(s) なる r は存在しないため、仮定法で用いる命題は成立するので、なにかおかしい気がする……。
定数群に対して必ず成り立つ述語でないといけないのかな？
この定理がどう役に立つのか？全てに成り立つ性質が示せて嬉しいか？という疑問も出た。おそらく、今後拡張が進むなかで定数部にxを含まないときにはこの性質が示せるがxを含むときには示せない、みたいな使われ方をするのでは？という話になった。
...書き出された証明を確認するより 簡単 である(p.23)
原文でも easier と書かれていることを確認した。
表示的意味論にとっての鬼門は... (p.24 †3)
鬼門は原文では "bête noire"だそうで。 https://ejje.weblio.jp/content/b%C3%AAte+noire
項
if true then (if false then false else false) else true) はif true then false else true` には評価されない(p.26)
if true then t1 else t2 でt1, t2から評価する規則はなく、E-IFTRUE のみしか使えないということを言っている。
次回は4章の終わりまで。
-
true に評価されないならば成り立たない、でいいよね？↩
