13.txt

# 1.1

a = {    ,    }
      ↓     ↓
     [0]   [0]

b = {   ,   }
      ↓   ↙
     [0]

（等幅フォントでご覧ください）


# 1.2

しない。
`let oldf`によるコピーを取らない場合、aが指す関数はupdateの呼び出しごとに書き換えられる。
そのため、このupdateはm!=nのとき無限に再帰呼び出しをしてしまう。

（仮に同じ動作なら問題になってない）


# 1.3

補題8.3.1 (p.72)が成り立たないので、進行と保存も成り立たない。

保存の定理8.3.3 (p.73) 「t:Tかつt->t'ならば、t':Tとなる」にも反する例:

r: Ref Nat と s: Ref Boolが同じ領域を指しTRUEが格納されている場合、
succ (!r) は型システム上正しく評価が行われているが、
実際はsucc TRUEとなり行き詰まり状態になる。

（「安全性」 = 進行 + 保存  (p.72)）


# 3.1

リファレンスカウントを利用したGCを考える。

ストアで参照カウンタと値を持つように変更する。
E-REFでrefを生成する際にはカウンタを1に、変数束縛などで同じ箇所を指すrefが増えた場合はカウンタをインクリメントするよう評価規則を変更する。
カウンタが0であれば使用されていないので、その領域は解放できる。
全コードを見て参照が最後に利用された式を特定し、その後にカウンタのデクリメントを行う。

## 問題点

「参照が最後に利用された」ことをどのように特定するのか。
ifのthen節など、実際には実行されない部分式がある場合でも利用にあたるので、false-positiveが発生する。
要は動的ではない。

スコープがあれば多少改善されるが、全コードを見て解放位置を探す羽目になる。
最初に全コードを舐めるならO(N)、逐次後続のコードを見るならO(N^2)か。

（GCと縁遠い。そろそろ本腰を入れたいけど、今書いてるのもRustだった）


# 4.1

let f1 = ref (\x:T.x)  // T -> T, whatever
let f2 = ref (\x:T.(!f1) x)  // T -> T
f1 := \x:T.(!f2) x   // T -> T

f1を評価すると!f2が呼ばれるが、片付け導出の構築過程でさらに!f1が呼ばれる


# 5.2

再帰的に自身の位置を参照するストアを考える。
μ(l) = (l = \x:T.(!l) x; l)
これは下記のような複数の型付けを取れる。
∑(l) = T -> T
∑(l) = T -> (T -> T)
∑(l) = T -> (T -> (T -> T))
...


# 5.8

13.4.1の例は循環しているので正規化できない（？）