# 設計思想：構成による解析可能性 Kagari は、物語についての問いに、プレイして確かめるのではなく解析によって、コンパイラが確実に答えられるように作られています。この章では、通常のスクリプト言語ではそれが不可能である理由、Kagari がそれをどう可能にしているか、スタジオが何を得て、何を代償とするかを説明します。 ## スタジオが問うこと {#the-questions-a-studio-asks} ビジュアルノベルの正しい振る舞いは作者の頭の中にあります。ある台詞がどのルートに属するか、あるシーンでどのフラグが成り立っていなければならないか、二つの分岐が合流した後にどの立ち絵が画面に出ているべきか。その知識に関わるバグは、作者以外の誰にも見えません。出荷の前に、スタジオは次のような問いの答えを知りたいはずです。 - このエンディングにそもそも到達できるか。ミオに会わずに到達できるか。 - 選択肢が一つも表示されない選択に行き着いて、プレイヤーが進めなくなることはないか。 - どのルートからも到達しないシーンや台詞はないか。 - 屋上ルートと教室ルートが合流した後、次の台詞は、どの経路でも作者の意図した背景を表示するか。 - 二回のクリックの間のコードは必ず終わるか。 - パッチの後もすべてのセーブがロードできるか。できないなら、正確にどこで食い違うのか。 テストで答えが得られるのは、誰かがプレイした経路についてだけです。*すべての* 経路についての答えには、プログラムの解析が必要です。 ## Rice の定理 {#rices-theorem} チューリング完全な言語に対しては、そのような解析は存在しえません。**Rice の定理**（1953年）は、プログラムの非自明な意味的性質はすべて決定不能であると述べています。*意味的* な性質とは、プログラムのテキストがどう見えるかではなく、プログラムが何をするかについての性質です。*非自明* とは、その性質をもつプログラムともたないプログラムがどちらも存在することです。そのような性質のどれについても、あらゆるプログラムに対してその性質をもつかどうかを判定するアルゴリズムはありません。 上の問いはすべてこの種類のものです。どの問いにも停止性問題を埋め込めます。停止するかどうか分からない計算の後にエンディングを置けば、「このエンディングに到達できるか」は「この計算は停止するか」になります。「二回のクリックの間のコードは終わるか」は、停止性問題 *そのもの* です。したがって、物語が任意のコードを実行できるエンジンでは、どんなツールも、諦めるか、推測するか、経路の一部をテストするしかありません。これは工夫で解決できる問題ではなく、定理です。 ## 決定不能性はスタックではなくデータから生じる {#data-not-stack} Rice の定理が適用されるのは、チューリング完全なプログラムです。抜け道は、物語を、チューリング完全ではないが物語には十分な表現力をもつ言語で書くことです。問題は、どこを制限するかです。 {{#include ../diagrams/philosophy-decidability.svg}} - **コールスタックだけなら無害です。** プッシュダウンシステム、つまり非有界なコールスタックをもつ有限状態機械の到達可能性は決定可能で、システムの大きさに対して多項式時間で計算できます。シーンはシーンを呼び、再帰し、呼ばれた場所へ戻ってかまいません。 - **問題は非有界なデータです。** 条件ジャンプをもつ非有界カウンタが二つあれば、スタックがなくても既にチューリング完全な Minsky 機械になります。際限なく大きくなれる整数、リスト、文字列は、どれもそのようなカウンタを持ち込みます。 そこで Kagari は、制御ではなくデータを制限します。物語は再帰、ループ、ハブマップ、共有されるサブシーンを自由に使えます。その代わり、物語が保持する値はすべて有限集合の中を動きます。 ## Kagari はどのように定理を回避するか {#how-kagari-sidesteps-the-theorem} Kagari は Rice の定理に反しているわけではありません。スタジオが問うことを、それが決定可能な部分についてだけ問うようにプログラムを構成し、その答えが残りの部分に依存しないようにしています。これを実現するのは三つの規則です。コンパイラは三つすべてを検査し、違反は警告ではなくコンパイルエラーになります。 ### 物語は有限データ上のプッシュダウンシステムである {#the-story-is-a-pushdown-system} 物語は [`pushdown fn`](../concepts/kinds.md) で書き、その内部では次のとおりです。 - すべてのローカル変数、引数、戻り値、物語変数は [有限型](../concepts/kinds.md#finite-types) をもちます。`bool`、`Int`、列挙型、および有限型からなる構造体、タプル、配列です。スタックフレームは戻り先と有限のローカル変数の組なので、スタックアルファベットは有限です。これがまさにプッシュダウンシステムの定義です。 - `pushdown fn` が呼べるのは `pushdown fn` と `const fn` だけです。物語から呼ばれる `const fn` は、コンパイル時に定数へ畳み込まれるか、引数が有限型の実行時の値であれば *表化* されます。つまり引数のすべての組み合わせについてコンパイル時に評価され、物語が渡しうるすべての入力でエラーなく終わり、有限の結果を返すことが証明されます。 - 関数ポインタは有限の値です。名前付き関数は有限個しかないからです。物語の中のクロージャは第二級（渡して呼ぶことはできるが、格納も、返却も、捕捉もできない）なので、捕捉された環境が状態の一部になることはありません。 - 制御フローは構造化されています。`goto` はないので、制御が関数を離れるのは呼び出しか戻りによってだけです。 - すべてのループとすべてのシーン呼び出しの循環はステップを通らなければなりません。入力なしで実行されるコード（即時手続き）は再帰せず、定数の上界のないループももちません。したがって、二つの入力の間のコードは必ず終わります。 このモデルでは到達可能性は決定可能です。コンパイラは、すべてのエントリーシーンとその引数のすべての値から物語を厳密に探索し、各シーンを入ったときの状態ごとに要約します。そのため、同じ状態で多くの場所から呼ばれるシーンも探索は一度で済みます。 ### 演出は純粋で、読み返されない {#the-presentation-is-pure} プレイヤーが見るものは [レンダー関数](../concepts/presentation.md) が計算します。レンダー関数は `const fn` で、チューリング完全ですが、純粋で決定的です。レンダーが受け取るのはステップの前の画面だけで、ステップの後の画面を返します。レンダーは物語変数を読めず、物語は画面を読めません。`Screen` は有限型ではないからです。したがって演出は、物語がどの状態に到達するかに影響しません。画面は、物語の解析が見つけた状態について、後から計算できます。レンダーは純粋なので、コンパイラはそれを、そのステップに到達しうるすべての画面の上で単に実行します。 ### チューリング完全なコードはエントリーシーンからしか入れない {#only-through-entry-scenes} ゲームシステムは通常の `fn` のコードです。`pushdown fn` を呼べず、物語変数を読めません。物語に入る唯一の方法は、有限型の引数で [エントリーシーン](../concepts/entry.md) を開始することで、解析はその引数が取りうるすべての値を対象とします。物語から戻ってくるのは、エントリーシーンの戻り値であるエンディングと、物語が書き込んで読み返さないメタだけです。システムが何を計算しようと、物語の振る舞いは、コンパイラが既に解析した実行のどれかになります。 ### 残る限界 {#where-limits-remain} 限界は二つ残ります。Kagari はそれを隠さずに明示します。 - **レンダーはチューリング完全です。** あるステップが表示しうる画面の集合が有限にとどまるかどうかは、一般には決定不能です。ハブのループを通るたびにキャラクターを 10 ピクセルずつ動かすレンダーは、毎回新しい画面を作ります。*暫定：* コンパイラは画面の集合を不動点として計算し、あるステップの集合を上限（現在は 64 画面）を超えて増やすレンダーを報告します（`E5005`）。受理されたプログラムの画面の集合は計算したものと厳密に一致するので、この規則は健全です。ただし、上限を超えたところでだけ有界になるレンダーは拒否されることがあります。また、すべての `const fn` の評価には固定の予算があり、使い切るとコンパイルエラーになります（`E4003`）。 - **決定可能であることは、安価であることとは違います。** 状態の数は、独立した物語変数の個数に対して指数的に増えます。解析は状態数の上限（既定は 200 000。[プロジェクト](../tools/projects.md) で設定可能）で止まり、警告 `W5006` を出します。見つかったものはそれでも報告されますが、すべての状態を必要とする検査は省略されます。 ## スタジオが得るもの {#what-studios-get} 以下の保証はすべて、ゲームのあらゆる実行、つまりすべてのエントリーシーン、その引数のすべての値、すべての選択の列について成り立ちます。どれも `kagari check` と `kagari build` が検査します。詳細は [診断](../../diagnostics/index.md) の各章にあります。 | 保証 | コンパイラが検査すること | 診断 | | ---- | ------------------------ | ---- | | **ステップ間の停止性** | すべてのループとすべてのシーン呼び出しの循環がステップを通ること。即時手続きと、物語からの `const fn` の呼び出しが終わること | `E5001`、`E5002`、`E3004`、`E3005`、`E4003` | | **行き詰まる選択肢がない** | すべてのアームのガードが偽の状態で到達できる `choice!` がないこと | `E5003` | | **死んだ物語がない** | どのエントリーシーンからも到達しないシーン、どの状態からも到達しないステップ、物語に影響しない物語変数を報告すること | `W5008`、`W5009`、`W5010` | | **物語に実行時エラーがない** | 範囲外のインデックスなどのエラーを、物語がそこに行き当たる箇所で見つけること | [定数評価](../../diagnostics/eval.md) | | **一貫した画面** | ステップが表示する画面が物語状態だけで決まり、どの経路で到達したかに依存しないこと | `W5004` | | **有界な画面** | あるステップの画面の集合を際限なく増やすレンダーがないこと | `E5005` | | **健全なゲームシステム** | すべてのモードが表示されうること、プレイヤーを閉じ込めるオーバーレイがないこと、底のページが戻らないこと、モードのスタックが有界であること、すべてのエンディングが扱われること | `W6001`、`E6002`、`E6003`、`W6004`、`E2037` | コンパイル時の検査に加えて、このモデルは、通常のエンジンにはない性質をランタイムにもたらします。 - **頑健なセーブ。** [セーブ](../concepts/saves.md) は状態ではなくトレースを記録します。エントリーシーンとその引数、すべての選択の安定した ID、最後の選択の後のステップ数、乱数のシードです。ロードはトレースを再生します。したがってセーブは、その位置が到達可能であることの *証拠* であり、到達不能な位置のセーブは存在しえません。スクリプトが変わっても、トレースが意味をなす限りセーブはロードでき、そうでなければロードは、もはや解決できない最初の選択で止まり、それがどれかを示します。 - **決定的な再生。** Kagari には浮動小数点数がありません。物語の状態は有限型を使い、それ以外のコードは正確な整数、`Rat`、`Decimal` を使います。レンダーは純粋です。乱数はシード付きの生成器から得られ、そのシードはセーブに含まれます。解析は、乱数の各抽選を、取りうるすべての値への分岐として扱います。したがって同じトレースは、どの機械でも同じ物語状態と同じ画面を生みます。 - **高速なジャンプとプレビュー。** 物語状態と論理画面はトレースの関数なので、どの位置も物語を再生することで再構築できます。ロードとバックログの巻き戻しは既にこの方法で動作しています。演出を最初から再生する必要はありません。経路上の最後の [キーフレーム](../concepts/presentation.md) より前のレンダーは、画面に影響しないからです。*暫定：* 同じモデルが想定しているエディタのカーソル位置でのライブプレビューは、まだツールチェーンに含まれていません。 ## スタジオが手放すもの {#what-studios-give-up} 保証には代償があり、それを払うのは物語だけです。 - **物語の中では有限データだけ。** `pushdown fn` では Rust の整数、`String`、`Vec`、`Rat`、`Decimal` を使えません。カウンタは、好感度 `Int<0, 5>` のような有界の `Int` の値で、複合代入は上下限で飽和します。 - **物語の中に外の世界はない。** 物語は `fn` を呼べないので、実行中に時計、ファイルシステム、画面、設定、メタを読めません。メタが物語に届くのはエントリー引数としてだけです。 - **制限された制御。** シーンのループと再帰はステップを通らなければなりません。即時手続きは定数の範囲と配列についてだけループし、再帰しません。`goto` はありません。 - **物語の中のクロージャは第二級。** クロージャは `pushdown fn` に渡して呼べますが、格納、返却、捕捉はできず、ステップを踏むこともできません。 - **一方向の演出。** ステップが表示するものが、物語がそこへ至った経緯に依存しなければならないなら、その依存はレンダーを選ぶ物語変数として表さなければなりません。画面から読み取ることはできません。 - **有界な解析予算。** 表化される呼び出しには引数の定義域の上限があり、レンダーにはステップごとの画面数の上限があり、物語には状態数の上限があります。非常に大きな物語では上限を上げる必要があるかもしれません。 - **あらゆる場所で保証を弱めてしまう言語機能。** 浮動小数点数、ユーザー定義のトレイト（標準ライブラリの固定された集合だけがあり、ジェネリクスは使えます）、マクロはありません。[フォーム](../syntax/forms.md) は構文の固定された一部です。 ## ゲームの残りが自由なままである理由 {#why-the-rest-of-the-game-stays-free} これらの制限は、物語の外には一切適用されません。ゲームシステムは、言語のすべてを使える `fn` のコードです。Rust の整数、`String`、`Vec`、第一級のクロージャ、シグナル、再帰、非有界なループを使えます。その値を対象とする解析はありません。ゲームシステムに対する検査は、型検査と、ソースに書かれた有限個のハンドラからコンパイラが集めるモードグラフの検査です。ハンドラが無限ループしてもかまいません。システムは唯一の入口を通してしか物語に影響できないので、この章のどの保証もそれに依存しないからです。 演出もチューリング完全です。`const fn` はループし、再帰し、正確な数で計算できます。純粋であり、コンパイラが必要とする時点で入力が分かっているので、コンパイラはそれを一般的に推論する必要はなく、実行すればよいのです。 結果として、役割が分担されます。正しさが作者の頭の中にある部分、つまり物語は、コンパイラが完全に検査できる部分です。それ以外はすべて、普通のプログラミングです。