TaPL読む２

3章読んだ。 1章の日本語が過剰にごつかったけど今のところそれ以降は普通だな。 ふんわりと雰囲気を書くと逆にごつくなるのか。 前まではてな記法だったけどMarkdownにしてみる。

• 3.2.4で、簡約したものを考えると思ったけど、この時点ではなにも規則を定めてなくてif True then t1 else t2が直ちにt2になるわけではない。succは置いといてもpredやiszeroは関数として書けちゃうから勘違いしてたけど、全部ただの値コンストラクタなのね。

• 導出木の向きって上から下に証明を書いてるよね？最後の結果が根であってるかな。けど証明を構築してるときは下から伸ばして考えるか…？

• 定数は評価されない、というのはそれを評価しようとすると不正とみなすべきか、単に自身を返せばいいのかちょっとわからない。「t->t'となるt'が存在しない」だと前者かな。

• すでに実装するだけで限界で、証明はしばらく悩んでから解答を流し見になっててよくない…

多ステップと声に出すとリステップを思い出してしまう。

追記190917 4章が実装の話だった…本では元の項の位置をinfoとして値コンストラクタに持たせるt(info, t1, ...)ことと、未定義のときに例外を返すようになっていた。演習4.2.2の大ステップスタイルだけはやっておくか。