第19章. なぜプログラムは却下されたのか

この章の目的

この章を読み終える頃には、プログラムが却下されるとはどういうことかが分かり、それを実際に目にして、どう対応すればよいかが分かります。この章を読み終える頃には、プログラムが却下されるとはどういうことかが分かり、それを実際に目にして、どう対応すればよいかが分かります。

第1章はある約束をしました — プログラムが走り出す前から、言語は各ティックが有限の時間と有限のメモリで終わることを保証する、と。その約束を守る言語の部分が「検証器(verifier)」です。すべてのプログラムは検証器を通ります。検証器が有限と証明できなかったプログラムは、却下されてそのプログラムは走りません。第1章はある約束をしました — プログラムが走り出す前から、言語は各ティックが有限の時間と有限のメモリで終わることを保証する、と。その約束を守る言語の部分が「検証器(verifier)」です。すべてのプログラムは検証器を通ります。検証器が有限と証明できなかったプログラムは、却下されてそのプログラムは走りません。

却下は故障ではありません。約束が仕事をしている姿です。却下されたプログラムは、ただ言語がそれを「保証」できなかった、というだけのことです。却下は故障ではありません。約束が仕事をしている姿です。却下されたプログラムは、ただ言語がそれを「保証」できなかった、というだけのことです。

却下を見てみる: 再帰

少しでもプログラミングを見たことがある人は、遅かれ早かれ「自分自身を呼び出す関数」に手を伸ばします。「これをまたやれ」と表現する自然なやり方だからです。これは数えながら降りていく関数です。少しでもプログラミングを見たことがある人は、遅かれ早かれ「自分自身を呼び出す関数」に手を伸ばします。「これをまたやれ」と表現する自然なやり方だからです。これは数えながら降りていく関数です。

fn count_down(n: Word) -> Word {
    if n <= 0 { 0 } else { count_down(n - 1) }
}

fn main() -> Word {
    count_down(5)
}

keleusma runで実行します。結果は無く、エラーだけが出ます。

error: verify: VerifyError("count_down: recursive call detected during WCMU topological sort")

意味があるのは「recursive call detected(再帰呼び出しを検出)」という部分です。残りは検出した内部チェックの名前です。意味があるのは「recursive call detected(再帰呼び出しを検出)」という部分です。残りは検出した内部チェックの名前です。

再帰が却下される理由

自分自身を呼び出す関数は、何度でも自分を呼び出してしまえます。深さは入力に依存します。言語はプログラムが走る前に呼び出しがどこまで深くなるか見えないので、仕事量やメモリ量の上限を約束できません。第1章でKeleusmaに無いものとして「再帰」が挙がっていました。このエラーはそのルールが強制されている姿です。自分自身を呼び出す関数は、何度でも自分を呼び出してしまえます。深さは入力に依存します。言語はプログラムが走る前に呼び出しがどこまで深くなるか見えないので、仕事量やメモリ量の上限を約束できません。第1章でKeleusmaに無いものとして「再帰」が挙がっていました。このエラーはそのルールが強制されている姿です。

書き換え

再帰版のcount_downの裏にあった意図は「5回繰り返す」ということでした。Keleusmaでは決まった回数の繰り返しを、回数をリテラルで書いたforループで表現します。再帰版のcount_downの裏にあった意図は「5回繰り返す」ということでした。Keleusmaでは決まった回数の繰り返しを、回数をリテラルで書いたforループで表現します。

fn repeat_five() -> Word {
    for _i in 0..5 {
        let _step = 1;
    }
    0
}

fn main() -> Word {
    repeat_five()
}

これは走り、0を返します。回数5はプログラムに書かれていて、検証器から見えるので、検証器はループが有限であることを証明できます。第8章で示したとおり、fnの中のこの種のループは結果を積み上げることはできません。実際に合計が必要な場合は、第18章で示したloop関数のデータセグメントが受け持ちます。これは走り、0を返します。回数5はプログラムに書かれていて、検証器から見えるので、検証器はループが有限であることを証明できます。第8章で示したとおり、fnの中のこの種のループは結果を積み上げることはできません。実際に合計が必要な場合は、第18章で示したloop関数のデータセグメントが受け持ちます。

もう2つの却下

回数が定数でないforループも却下されます。

fn process(n: Word) -> Word {
    for i in 0..n {
        let _step = i;
    }
    0
}

これはno statically extractable iteration boundという文字列を含むエラーを出します。回数nは実行時に来る値で、検証器は事前に見られません。直し方は同じです — 定数のリミットを使うか、長さが固定の配列を巡るようにします。これはno statically extractable iteration boundという文字列を含むエラーを出します。回数nは実行時に来る値で、検証器は事前に見られません。直し方は同じです — 定数のリミットを使うか、長さが固定の配列を巡るようにします。

yieldが無いloop関数はStream block must contain at least one Yieldで却下されます。第17章の生産性ルールが、検証器によって強制されている姿です。yieldが無いloop関数はStream block must contain at least one Yieldで却下されます。第17章の生産性ルールが、検証器によって強制されている姿です。

却下の2つの分類

却下は2つのグループに分かれます。

ある種のプログラムは、そもそも上限が存在しないから却下されます。再帰がその一つです。言語の将来の改良でも、それを受け入れるようにはなりません。証明するものが無いからです。対応は、プログラムを書き換える、これしかありません。ある種のプログラムは、そもそも上限が存在しないから却下されます。再帰がその一つです。言語の将来の改良でも、それを受け入れるようにはなりません。証明するものが無いからです。対応は、プログラムを書き換える、これしかありません。
別の種のプログラムは、上限は存在するけれど、今の分析がまだそれを取り出せないから却下されます。実行時の値で回数が決まるループがその例です。将来、より鋭い検証器なら、そのまま受け入れるかもしれません。別の種のプログラムは、上限は存在するけれど、今の分析がまだそれを取り出せないから却下されます。実行時の値で回数が決まるループがその例です。将来、より鋭い検証器なら、そのまま受け入れるかもしれません。

どちらの場合でも、初心者にとって必要な対応は同じです — 検証器が受け入れる形にプログラムを書き換える、です。リポジトリ内のドキュメントWHY_REJECTED.mdに却下メッセージとその書き換え方の一覧があります。どちらの場合でも、初心者にとって必要な対応は同じです — 検証器が受け入れる形にプログラムを書き換える、です。リポジトリ内のドキュメントWHY_REJECTED.mdに却下メッセージとその書き換え方の一覧があります。

この章のまとめ

検証器はすべてのプログラムを確認し、有限であることを証明できないものを却下します。検証器はすべてのプログラムを確認し、有限であることを証明できないものを却下します。
再帰は、その深さが事前に分からないので却下されます。
回数が定数でないループも、同じ理由で却下されます。
yieldの無いloopは、生産性ルールによって却下されます。
却下は故障ではなく、言語が約束を守っている姿です。

次の章ではその約束そのもの — プログラムが収まることを証明される「予算」 — を説明します。次の章ではその約束そのもの — プログラムが収まることを証明される「予算」 — を説明します。

Keyboard shortcuts

The Keleusma Guide