TaPL読書録 #3
今回は4章終わりまで。
私物ノートPCのエンターキーがぶっ壊れているため今回のメモは控えめ。
定理3.5.12.
整礎集合の1要素へとマッピングできる関数 f を用いて無限降下列にならないことを示す論法は他の箇所でも見た気がする。
演習3.5.13.
(1) 雑に一意性を損ねること、正規形に関して影響を及ぼさないことがわかればよい。
(2) 1ステップ評価の一意性は損ねるが、多ステップ評価の一意性を損ねないところがミソ。
これは解答の補題とその訳注が面白い。
補題A.1.
ダイヤモンド性について。停止尺度の観点から評価によりかならず停止尺度が下がるのにもかかわらず、s -> t, s -> u において t -> u となるようなことがあるのか疑問に感じて発言した。が、停止尺度として示されていた項のサイズは必ず1ずつ下がるわけではないので十分にありえる話だった。
訳注について具体例をもって示す。 E-IFFALSEとE-FUNNY2が同時に成り立つような項について考える。
t2 -> t2' において if false then t2 else t3
E-IFFALSE を用いて評価した場合は t3
E-IFFUNNY2 を用いて評価した場合は if false then t2' else t3 であるがこれは再度 E-IFFALSE を用いて評価することで t3 となる。
これはダイヤモンドではなく、「三角形」であると言える。
本では次に数値という概念で拡張する。
prod 0 -> 0 なる評価に意図を感じる。
演習3.5.16.
演習としては行き詰まり状態と wrong が多ステップ評価の元同値であること、すなわち 「行き詰まり状態であれば wrong と評価されること」と「wrong と評価される前の項は行き詰まり状態であること」が示せればよい。
演習3.5.17.
こちらも iff であることを示せばよい
演習3.5.18.
E-IF, E-IFTRUE, E-IFFALSE を取り除いて5つの評価規則を追加する。画像参照。
t3の評価を行う評価規則の左辺で t2 ではなく v2 であるところに注意。
補題A.8.
succ t ->* succ v のときに t ->* v とステップ数が変わってないので「他の項構築子についても同様である」が誤りでないかという指摘があった。のだけど succ の付け外しも評価に含むんじゃねーかなといまは思いつつある。
次回は5章全部。
