実行の上限を設定する
budget、停止性、Div を区別します。
11.1 無限ループがないとは限らない
一般のループや再帰は、止まらないことがあります。Tauto は、その可能性を effect の Div に反映します。ただし、Div がないことは、「あらゆる実行環境で、時間やメモリが足りなくなることなく完了する」ことと同じではありません。
11.2 ステップ予算による中断
ch11-budget.taut
let value := handle {
budget(steps: 3) { 7 }
} with {
exceeded(info), k => info.more(100)
}
perform show("value", value)
実行結果
value = 7
value = 7
budget(steps: n) { body } は、実行のステップ数に予算を設けます。予算が尽きると exceeded が起き、ハンドラは info.more(100) のように追加のステップを与えて、続きを実行できます。
ステップの数え方は実装依存です。steps: 3 が「命令を 3 つ実行する」ことを意味するわけではありません。
予算の外側にも制限があります。tauto run --steps N で実行全体のステップ数に上限を付けると、それに達したとき、実行は exceeded ではなく「interrupted」で止まります。
tauto run --steps 5 ch11-budget.taut
ch11-budget.taut: interrupted: the step limit ran out
11.3 「予算を足す」と「必ず止まる」
info.more を繰り返せば、止まらない計算はいつまでも続きます。また、処理系の外側にある、時間やメモリの制限、OS の終了要求は、exceeded とは別のものです。
安全性を考えるときは、次の三つを分けてください。
- 型と effect が示す、静的な性質。
- ステップ予算が与える、動的な制限。
- ホストが与える、リソースの上限。
演習 11.1：無限に回る処理を budget で包んでも、その処理自体が止まることの証明にはならないのはなぜでしょうか。