静的段階の全域性は構文制限だけでは得られない
「静的段階の評価が必ず停止する」という性質は、一般再帰を禁じてループを有限に限るだけでは出てこない。構文制限と参照グラフの非循環性強制という二本の柱で初めて成り立つ。
一本目の柱は構文制限である。CarinaのDSLに一般再帰はなく、forは有限コレクション上の展開しかできない。ここまでは言語仕様を小さく保てば得られる。
しかし構文制限だけでは停止は出ない。値の流れの循環という、構文では塞げないもう一つの発散源があるからである。相互に参照し合う束縛やリソースがそれで、二本目の柱である参照グラフの非循環性強制で塞ぐ。具体的には:
- 循環するlet束縛はfixed-point評価の前に静的に拒否される(
Cyclic let binding detected)。letのfixed-point自体にも束縛数+1の反復上限がある。 - リソース間の参照については、評価器がそもそも式を収束まで反復しない。静的段階で解決できない参照はdeferredのまま残り、動的段階が依存グラフの位相順で解決する。その上でグラフの循環は明示エラーで拒否される(
Circular dependency detected: a -> b -> a)。「自分の出力に依存するリソースへの参照」は、このDAG強制が遮断する形になっている。
全域性に加えて、評価結果がソースとstateだけの関数であるという純粋性も同時に立っている。この二つが言語の性質として成り立っているために、「プログラムを完全評価してから、出てきた値を全数検査する」が完全な決定手続きになる。
つまり全域性は言語を制限することでしか得られず、その制限は構文の形をしたものだけではない。値の流れというグラフ上の制約が必ず要る。