TaPL読む５ - も！

10章まで読んだ。実装はまだ（来年かな…）

のっけからあまり関係ない話だが、ラムダ抽象について、λx. a bをx. a bのようにしていたのを、そのうち他の束縛子（forallとか）を使うかもしれないと考え>x$ a bのような形に変更した。本当はHaskellと同様に\xとしたかったが、（少なくともGHCiで入力するときは）エスケープしないとだめで面倒だったので、λに似た文字として>を選んだ。.を$に変えたのは、まあHaskellの関数適用を真似したんだが、文末まで適用する意味が似てるので借用した。ただちょっと字面がうるさいのでこれはやめるかもしれない。ところでなぜ関数適用がドルマークなのかを検索すると「括弧とそれを打ち消した図」といった説明があって、真偽は怪しいけど面白いと思った。

ここからはTaPLの感想（というか内容の抜き出し、全然整理できてないし理解も間違ってそう）。

8章は算術式に型をつける話。ウォーミングアップ的な感じだと思うけど、背伸びしたがりなので色々調べてたらこんがらがってきた。

型付き規則（型付き項の構築）と対応する逆転補題・生成補題（項の型付け）について；逆転補題が成り立つのは、型付き規則の導出木の形に被りがないとき？逆転補題が成り立つとき、ある型に型付けられた項の型は一意に定まる（矛盾しない↔正しい？）。
型システムの健全性（安全性）；正しく型付けされた項は行き詰まり状態（正規形（評価が静止する）かつ値ではない）にならない↔論理体系の健全性；（構文論的に）証明できる命題は（意味論的に）成り立つ
健全性を証明する性質が、進行（正しく型付けされた項は行き詰りでない）と保存（評価によって型付けが正しくなくなることはない）
逆の（意味論的）完全性は、正しい（値になる？）項は正しく型付けできるということになるのかな。「保存は項（主部）の簡約について成り立つが、逆に型付けされた値を得る主部を展開したとき正しく型付けされるとは限らない」という話を見るとこれは一般には成り立たなさそう。逆転補題と矛盾してる気がしたけど、あれは項が正しく型付いた上での話で、主部展開の話は（簡約が存在する）任意の項についてどうかという違いっぽい？
「（意味論的に）正しい項」が指すものは（操作的）意味論によって異なるらしい。小ステップ意味論の場合は「進行によって行き詰まり状態にならない」だが、大ステップ意味論では「進行によって評価が停止し値となる」。この場合、停止しないが行き詰まり状態でない状態を区別できないが、行き詰まり状態を特別にwrongに評価することで回避できる。
Wikipediaを見ると、不完全性定理の完全性は構文論的完全性と言われ、形式体系において任意の式の真否が証明できること（第一不完全性）らしい。紛らわしいので決定性とか言ってほしいけど、決定性にも別の意味があり、与えられた式がある理論の定理に属するかを有限時間で判定できるかを表す。こっちは判定性と呼びたい…

9章・10章はラムダ計算を単純型付きラムダ計算に進化させる。全然単純じゃなかった。

純粋なラムダ計算が型解析できないのはチューリング完全は関係なくて、基本型がないので精々関数型を用いて→とだけ評価されるしかないからでは？if式の例はすでにthen節とelse節の型は同じになるべきと言ったので不適切な気がする。任意の型となるtを入れると型が型無しラムダ計算と同じ構造になるので、こうすればチューリング完全うんぬんの話になりそう。
ラムダ束縛された引数に型注釈が必要な理由がよくわからない。質問を投げてみたら「T1 -> T2 という型を持つ関数は仮引数が 1 つで T1 型を持ち返り値は T2 型、というのは関数の定義から自明…それを…前置きなく暗黙の前提にはできなさそう」ということらしい。上で書いた構文で>x:T1$t2:T1->T2とするとさすがに字面がうるさいからあまりそうしたくないけど…
型付き文脈の並び替えは、これ証明いるの？リストだとするとそういうのあるかもしれないけど、その前に有限の関数だとみなしてるから並び替えも何もないのでは…弱化も定義域の拡張じゃないの？私がおおざっぱすぎなのかな
型保存の定理がここまで一般的でなくていいという訳注は、値呼びであることとに加えて小ステップなことも必要じゃない？
型消去を用いて型付け可能の定義をしている。健全性もこれで定義できそう
型検査で失敗するときを考えると実装をさぼってた項の細かい情報もいりそう…

来年どころか再来年でも読み終わってなさそう。