# 事例研究：教科書サイトの検査系を読む（相互参照・依存の閉包・決定的な生成） > 定理に識別子を付けて相互参照する教科書サイトの検査を題材に、参照の解決の一意性、根拠のある命題の最小不動点としての特徴づけと線形時間の計算、採番の決定性、検査の健全性と完全性の限界、公開の不変条件を証明し、最小の実装と性質ベーステストで確かめる。 > https://rikai.mugen-giken.com/computer-science/software-design-testing/case-study-textbook-checks ## 0. この記事の要点 数学の教科書には「第 3 節の定理より」といった参照が何百回も出てきます。その参照先が本当に存在するか、参照をたどっていくと土台（定義や公理）までたどり着くか、ぐるぐる回って循環していないかを、人の目ではなく機械に確かめさせるにはどう作ればよいか。この記事は、そうした検査をするシステムを実例に、前の章で学んだ契約・テスト・ビルド・CI の考え方が 1 つのシステムの中でどう働くかを読みます。読み終えると、「機械に任せてよい検査」と「人が見るしかない部分」の境目を、理由つきで説明できるようになります。 - 題材は、定理・定義に識別子を付けて相互参照する教科書サイト（このサイト自身）の検査系です。前 5 章の契約・テスト・ビルド・CI が、1 つの系の中でどう組み合わさっているかを読みます。 - 識別子が文書内で一意なら、参照の解決は入力の関数になり、未解決の参照の集合は走査順によらず 1 つに決まります（）。一意性の検査は、ほかのすべての検査の前提です。 - 「公理・定義から証明をたどって到達できる命題」の集合は、単調な作用素（入力の集合が大きくなっても出力の集合が小さくならない写像）の最小不動点（これ以上増えなくなる最小の集合）です（）。これは命題の数と依存の数について線形の時間で求まります（）。 - 根拠のない命題は、証明のない命題か循環に含まれる命題に依存しているものにちょうど一致します（）。検査の報告は「証明のない葉」と「循環」の 2 種類で足ります。 - 番号を「文書内の出現順」の関数として決めれば、採番は走査順・並列度・時刻によりません（）。 - 機械が検査しているのは「証明が何に依存すると宣言しているか」であって、証明の正しさではありません。意味的な性質については、健全で完全な検査は一般に作れません（）。正しさは人と別の主体による監査が受け持ちます。 - 「検査に合格した版だけが公開される」という不変条件は、各段階が前の段階の出力だけを入力にするとき保たれます（）。 ## 1. 動機：「第 3 節の定理より」は誰が確かめるのか 数学の教科書には「第 3 節の 2 番目の定理より」「第 5 節の補題を使うと」という、番号による参照が何百回も現れます。紙の本では、この参照が正しい相手を指しているか、指された定理に証明があるか、証明の連鎖が循環していないかを確かめるのは、著者と査読者と読者の目です。章を入れ替えれば番号はずれ、定理を消せば参照は宙に浮きます。 記事が数百本、定理・定義などの環境が 1 万個を超える規模になると、目では追えません。そこで、参照を番号ではなく**識別子**で書き、番号は機械に振らせ、参照が解決するか・依存が公理までたどれるかを機械に検査させる、という設計になります。これはソフトウェアでいえば、名前の解決とリンクの検査、そして依存グラフの解析です。 この章では、そのような検査系を、前 5 章の道具で読み解きます。題材は、このサイト（Rikai）で公開している検査の仕様と設計です。スクリプトそのものは載せず、要点を自作の最小の実装で示します。問いは 4 つです。 1. 検査の結果は、入力（記事の集合）だけで決まるか。決まるための条件は何か。 2. 「公理までたどれる」は、どう定義し、どう計算するのか。 3. 機械の検査が保証することと、保証しないことの境界はどこか。 4. 検査を通ったものだけが公開されることは、何によって保たれるか。 ## 2. 題材：検査系の構成 題材のサイトは、記事を 1 本 1 ファイルの文書として書き、前処理・検査・静的サイトの生成・公開の順に処理します。記事の中の定義・定理・証明などは**環境**として書かれ、それぞれが識別子をもちます。公開されている仕様から、検査に関わる部分を抜き出すと次のとおりです。 | 仕組み | 仕様の要点 | 対応する章 | |---|---|---| | 環境の識別子 | 記事の中で一意。英小文字・数字・ハイフンだけ。接頭辞が種類を表す（`def-`、`thm-` など） | 契約（不変条件） | | 相互参照 | 同じ記事の中は識別子だけ、別の記事は「記事の識別子 `#` 環境の識別子」で指す。解決できない参照は検査が誤りにする | ビルド（名前の解決） | | 採番 | 見出し「`## N.`」を節番号とし、節の中で環境の種類をまたいで通し番号を振る。番号は手で書かない | ビルド（決定的な生成） | | 書式の検査 | 記事の先頭の属性、識別子の形、参照と内部リンクの解決、数式の構文、禁止する表現、分量 | テスト（構文的な検査） | | 閉包の検査 | 定理類（定理・命題・補題・系）ごとに、証明があるか、証明の中の参照を推移的にたどって公理・定義まで届くかを集計する（対象は数学と物理の記事） | この章の §4 | | 台帳 | 証明を書かない定理は、理由と出典を添えて台帳に登録する。台帳にない「主張のみ」が増えると検査が失敗する | CI（水準を上げる移行） | | 演習問題集の検査 | 各問題が「使う定理」として挙げた名前が、記事の定義・定理に解決するか。書式・答え・番号の連続も調べ、1 件でも問題があればビルドを止める | ビルド（依存の宣言） | | 監査 | 閉包の判定は機械的で、証明の正しさは見ない。正しさは書き手とは別の主体による監査で確かめ、結果を来歴として記録する | この章の §6 | 以下では、この構成を抽象化した模型の上で定理を述べます。 **文書の集合** $K$ とは、次のデータである。 - 文書の識別子の有限集合 $\mathrm{Doc}$。 - 各文書 $d \in \mathrm{Doc}$ に、環境の有限列 $\mathrm{env}(d) = (e_1, \ldots, e_m)$（出現順）。 - 各環境 $e$ に、**種類** $\mathrm{kind}(e)$（定義・公理・定理・命題・補題・系など）と、**局所的な識別子** $\iota(e)$（記号 `#` を含まない文字列）。 - 種類が定理・命題・補題・系である環境（**定理類**）には、証明があるかないかの別と、証明がある場合はその中に書かれた参照の文字列の有限列 $\mathrm{ref}(e)$。 対 $(d, \iota)$ を**鍵**と呼び、$d\,\texttt{\#}\,\iota$ とも書く。 **検査**とは、文書の集合 $K$ に、**違反**の有限集合 $\kappa(K)$ を対応させる手続きである。同じ $K$ に対していつ実行しても同じ集合を返すとき、検査は**決定的**であるという。違反のうち、1 件でもあればパイプラインを止めるものを**誤り**、報告するだけで止めないものを**警告**という。検査が**合格**であるとは、誤りが 1 件もないことをいう。 誤りと警告の区別は、検査の精度ではなく運用の決めごとです。たとえば §3.2 の綴り違いのような違反を、止めるべき誤りにするか、知らせるだけの警告にするか、という選び方の話です。新しい検査を入れた直後は既存の違反が多く、すべてを誤りにすると[パイプライン](/computer-science/software-design-testing/continuous-integration#def-ci-pipeline)が止まったままになります。そのときにどう移行するかは §7 で扱います。 ## 3. 参照の解決 ### 3.1. 解決は関数か 参照は文字列として書かれています。それがどの環境を指すかを決めるのが**解決**です。 文書 $d$ の中に書かれた参照の文字列 $r$ に対し、鍵 $\mathrm{key}(d, r)$ を次で定める。 - $r$ が記号 `#` を含まないとき、$\mathrm{key}(d, r) = (d, r)$（同じ文書の中の名前）。 - $r$ が `#` を含むとき、最初の `#` の前を $d'$、後ろを $\iota'$ として $\mathrm{key}(d, r) = (d', \iota')$（文書の識別子つきの名前）。 文書の集合 $K$ の**索引**を、鍵と環境の対の集合 $$ \mathrm{Idx}(K) = \bigl\{\, \bigl((d, \iota(e)),\ e\bigr) : d \in \mathrm{Doc},\ e \text{ は } \mathrm{env}(d) \text{ の成分} \,\bigr\} $$ とする。$\mathrm{Idx}(K)$ が鍵から環境への部分写像のグラフであるとき、$\mathrm{res}(d, r)$ を鍵 $\mathrm{key}(d, r)$ に対応する環境（なければ未定義）と定め、未定義のとき $r$ は**未解決**であるという。 文書の集合 $K$ が次の条件を満たすとする。 - (U) 各文書 $d$ について、$\mathrm{env}(d)$ の相異なる成分は相異なる局所的な識別子をもつ。 このとき次が成り立つ。 (a) $\mathrm{Idx}(K)$ は鍵から環境への部分写像のグラフである。すなわち、1 つの鍵に対応する環境は高々 1 つである。 (b) 空の表から始めて、$\mathrm{Idx}(K)$ の対 $(k, e)$ を任意の順序で「表の $k$ の欄に $e$ を書く（すでに値があれば上書きする）」と登録していくと、最後の表は順序によらず同じで、$\mathrm{Idx}(K)$ に一致する。したがって $\mathrm{res}(d, r)$ は $K$ と $d$ と $r$ だけで決まる。 (c) 未解決の参照の集合 $$ U(K) = \bigl\{\, (d, e, r) : e \text{ は } \mathrm{env}(d) \text{ の成分で証明をもち},\ r \text{ は } \mathrm{ref}(e) \text{ の成分},\ \mathrm{res}(d, r) \text{ は未定義} \,\bigr\} $$ は $K$ だけで決まる。 **(a)。** $\bigl((d, \iota), e\bigr)$ と $\bigl((d, \iota), e'\bigr)$ がともに $\mathrm{Idx}(K)$ に属するとします。索引の定義より、$e$ と $e'$ はどちらも $\mathrm{env}(d)$ の成分で、$\iota(e) = \iota = \iota(e')$ です。条件 (U) より、同じ識別子をもつ成分は同じ成分なので $e = e'$ です。 **(b)。** 登録した対の個数についての帰納法（）で、「対の集合 $A \subseteq \mathrm{Idx}(K)$ を登録し終えた表は、$A$ をグラフとする部分写像である」ことを示します。対が 1 つのときは成り立ちます。$A$ まで登録した表に $(k, e)$ を登録するとき、$k$ の欄にすでに値 $e'$ があれば、$(k, e') \in A \subseteq \mathrm{Idx}(K)$ なので、(a) より $e' = e$ で、上書きしても表は変わりません。欄が空なら対が 1 つ増えます。どちらの場合も、表は $A \cup \{(k, e)\}$ をグラフとする部分写像です。すべての対を登録し終えた表は $\mathrm{Idx}(K)$ で、これは登録の順序を含まない式で書かれています。 $\mathrm{key}(d, r)$ は文字列 $r$ と $d$ から、`#` の有無と最初の `#` の位置だけで決まる全域的な関数です。$\mathrm{res}(d, r)$ は、この鍵を $\mathrm{Idx}(K)$ で引いた結果なので、$K$、$d$、$r$ だけで決まります。 **(c)。** $U(K)$ の定義に現れるのは $K$ のデータと $\mathrm{res}$ だけで、(b) より $\mathrm{res}$ は $K$ で決まります。 (b) の「任意の順序」は、ファイルを読む順序、並列に読むときの完了の順序を含みます。条件 (U) があるから、索引を作る処理を並列化しても結果が変わらない、と言えます。 文書 `limits` に、同じ識別子 `thm-main` をもつ環境が 2 つあるとします。1 つ目は「極限の一意性」、2 つ目は「はさみうちの原理」です。 (b) の登録の手続きは、後から書いたものが勝つので、 - 出現順に登録すると、`limits#thm-main` は「はさみうちの原理」を指し、 - 逆順に登録すると、「極限の一意性」を指します。 1 つの文書を前から読むかぎり順序は固定されますが、文書を分割して並列に処理する、環境の種類ごとに別々に集めてから合わせる、といった実装の変更で、指す相手が黙って入れ替わります。参照元の記事には何の変更もないのに、表示される定理番号と、たどった先の証明が変わるわけです。 したがって、条件 (U) は「できれば守りたい作法」ではなく、ほかの検査がすべて前提にしている**不変条件**です。題材のサイトが識別子の重複を誤りにしているのはこのためです。[契約による設計](/computer-science/software-design-testing/contracts-and-invariants) の言葉でいえば、(U) は索引というデータ構造の[表現不変条件](/computer-science/software-design-testing/contracts-and-invariants#def-rep-invariant)で、索引を作る処理の入口で検査して、破れていれば先に進まないのが筋です（）。 ### 3.2. 参照の検査の 4 つの最小例 次の 4 つは、以下の節で繰り返し使う最小の例です。 1. **綴り違い。** 証明の中に `lem-eucild` と書いたが、文書にあるのは `lem-euclid` である。$\mathrm{res}$ は未定義で、未解決の参照として報告される。 2. **存在しない識別子。** 別の文書 `order` の `thm-max` を参照しているが、`order` にその環境はない（消された、または最初からなかった）。これも未解決の参照である。 3. **循環する 2 つの補題。** 補題 A の証明が補題 B を参照し、補題 B の証明が補題 A を参照している。参照はどちらも解決するので、§3 の検査では見つからない。 4. **証明のない定理に依存する系。** 系の証明が定理 Z を参照し、定理 Z には証明がない。参照は解決するので、やはり §3 の検査では見つからない。 1 と 2 は名前の問題、3 と 4 は依存の構造の問題です。後者を扱うのが次節です。 ## 4. 根拠のある命題：依存の閉包 ### 4.1. 定義 条件 (U) を満たす文書の集合 $K$ について、環境の全体を $N$ とし、次のように分ける。 - $B \subseteq N$：**基礎**。定義と公理（証明を要しないと決めた種類の環境）。 - $S = N \setminus B$：定理類。そのうち証明をもつものの全体を $P \subseteq S$ とする。 $s \in P$ に対し、証明の中の参照のうち解決できたものが指す環境の集合を $$ \mathrm{prem}(s) = \{\, \mathrm{res}(d, r) : r \text{ は } \mathrm{ref}(s) \text{ の成分で、} \mathrm{res}(d, r) \text{ が定義される} \,\} \subseteq N $$ （$d$ は $s$ のある文書）とし、$s$ の**前提**と呼ぶ。有向グラフ $G_K = (N, E)$、$E = \{(u, s) : s \in P,\ u \in \mathrm{prem}(s)\}$ を**命題の依存グラフ**という。辺 $(u, s)$ は「$s$ の証明が $u$ を使う」ことを表す。 環境の有限列 $(s_1, \ldots, s_m)$ が**導出列**であるとは、各 $i$ について - $s_i \in B$ であるか、 - $s_i \in P$ かつ $\mathrm{prem}(s_i) \subseteq \{s_1, \ldots, s_{i-1}\}$ である ことをいう。ある導出列の成分として現れる環境を**根拠のある**環境といい、その全体を $\mathrm{Gr}(K)$ と書く。$\mathrm{Gr}(K)$ を求めることを**依存の閉包**の計算という。依存グラフ $G_K$ の有向閉路を**循環論法**という。 導出列は「前から順に読めば、どの証明も、すでに確立した事実しか使っていない」という並べ方です。教科書の章立てが満たすべき条件そのものです。証明のない定理類（$S \setminus P$ の元）は、どの導出列にも現れません。 ### 4.2. 最小不動点としての特徴づけ $N$ の部分集合の全体 $2^{N}$ は、包含関係を順序として半順序集合になり（）、どんな部分集合族も和集合を上限にもつので完備束です（）。ここでは、「集合どうしを包含で比べられ、いくつ集めても和集合が取れる」という性質だけが使われます。 次の定理のねらいは、「公理までたどれる命題の集合」を、手で数え上げずに 1 つの規則から決めることです。規則は「前提がすべて集まっているなら、その結論も集合に加える」です。この規則を空集合から繰り返し適用すると、集合は広がっていき、やがてそれ以上は増えなくなります。止まったところが求める集合で、それが最小不動点（もう変わらない集合のうち最小のもの）です。たとえば、定義 $D$、$D$ だけを使う補題 $L_1$、$L_1$ だけを使う補題 $L_2$ があれば、集合は $\{D\}$、$\{D, L_1\}$、$\{D, L_1, L_2\}$ と 1 段ずつ広がります。 写像 $\Phi : 2^{N} \to 2^{N}$ を $$ \Phi(X) = B \cup \{\, s \in P : \mathrm{prem}(s) \subseteq X \,\} $$ で定める（「前提がすべて $X$ に属するなら、結論を加える」）。 (a) $\Phi$ は単調である。すなわち $X \subseteq Y$ ならば $\Phi(X) \subseteq \Phi(Y)$。 (b) $X_0 = \emptyset$、$X_{k+1} = \Phi(X_k)$ とおくと、$X_0 \subseteq X_1 \subseteq X_2 \subseteq \cdots$ で、ある $k \le |N|$ で $X_{k+1} = X_k$ となる。この $X_k$ を $X^{*}$ と書くと、$X^{*}$ は $\Phi$ の最小不動点である。 (c) $X^{*} = \mathrm{Gr}(K)$。 **(a)。** $X \subseteq Y$ とし、$s \in \Phi(X)$ を取ります。$s \in B$ なら $s \in \Phi(Y)$ です。$s \in P$ かつ $\mathrm{prem}(s) \subseteq X$ なら、$\mathrm{prem}(s) \subseteq Y$ なので $s \in \Phi(Y)$ です。 **(b)。** $X_k \subseteq X_{k+1}$ を $k$ についての帰納法（ を $k + 1$ に適用）で示します。$X_0 = \emptyset \subseteq X_1$ です。$X_k \subseteq X_{k+1}$ なら、(a) より $X_{k+1} = \Phi(X_k) \subseteq \Phi(X_{k+1}) = X_{k+2}$ です。 $X_0, X_1, \ldots, X_{|N|+1}$ のすべての包含が真の包含だとすると、元の個数が毎回 $1$ 以上増えるので $|X_{|N|+1}| \ge |N| + 1$ となり、$X_{|N|+1} \subseteq N$ に反します。よって、ある $k \le |N|$ で $X_{k+1} = X_k$ です。このとき $\Phi(X_k) = X_k$ で、$X^{*} = X_k$ は不動点です。 $\Phi(Y) \subseteq Y$ を満たす任意の $Y \subseteq N$ について、$X_j \subseteq Y$ を $j$ についての帰納法で示します。$X_0 = \emptyset \subseteq Y$ です。$X_j \subseteq Y$ なら、(a) より $X_{j+1} = \Phi(X_j) \subseteq \Phi(Y) \subseteq Y$ です。よって $X^{*} \subseteq Y$ です。 Knaster–Tarski の定理（）より、単調な $\Phi$ の最小不動点は $a = \bigcap \{Y : \Phi(Y) \subseteq Y\}$ です（完備束 $2^{N}$ の下限は共通部分です）。いま示したことから $X^{*}$ はこの族のすべての元に含まれるので $X^{*} \subseteq a$ で、$X^{*}$ 自身が $\Phi(X^{*}) = X^{*}$ よりこの族に属するので $a \subseteq X^{*}$ です。よって $X^{*} = a$ です。 **(c)。** $\mathrm{Gr}(K) \subseteq X^{*}$ を示します。導出列 $(s_1, \ldots, s_m)$ について、「$s_i \in X^{*}$」を $i$ についての完全帰納法（）で示します。$s_i \in B$ なら $s_i \in \Phi(X^{*}) = X^{*}$ です。$s_i \in P$ かつ $\mathrm{prem}(s_i) \subseteq \{s_1, \ldots, s_{i-1}\}$ なら、帰納法の仮定より $\mathrm{prem}(s_i) \subseteq X^{*}$ なので $s_i \in \Phi(X^{*}) = X^{*}$ です。 $X^{*} \subseteq \mathrm{Gr}(K)$ を示します。(b) の後半より、$\Phi(\mathrm{Gr}(K)) \subseteq \mathrm{Gr}(K)$ を示せば十分です。$s \in \Phi(\mathrm{Gr}(K))$ とします。$s \in B$ なら、1 項の列 $(s)$ が導出列なので $s \in \mathrm{Gr}(K)$ です。$s \in P$ かつ $\mathrm{prem}(s) \subseteq \mathrm{Gr}(K)$ なら、$\mathrm{prem}(s)$ の各元 $u$ について、$u$ を含む導出列 $\lambda_u$ があります。有限個の導出列をつなげた列は導出列です（各成分の条件は、自分より前に必要な前提が現れていることで、前に別の列が付いても保たれます）。そこで、$\mathrm{prem}(s)$ のすべての元についての $\lambda_u$ をつなげ、最後に $s$ を付けた列を作ると、$s$ の前提はすべて前に現れているので、これは導出列です。よって $s \in \mathrm{Gr}(K)$ です。 (b) は、そのまま算法になります。$\Phi$ を、集合が変わらなくなるまで繰り返し適用すればよいのです。ただし 1 回の適用で全命題の前提を調べ直すので、依存の総数を $M$ として 1 回に $O(|N| + M)$、反復が最大 $|N|$ 回で、最悪の場合は $O(|N|(|N| + M))$ 時間かかります。実際の反復の回数は依存の鎖の長さで決まるので、教科書の規模ではこの素朴な反復でも足り、題材のサイトの閉包の計算もこの形（集合をその場で更新しながら、変わらなくなるまで繰り返す反復）です。それでも、入力の大きさに比例する時間で済むという保証のある算法を知っておく価値はあります。 ### 4.3. 線形時間の算法 素朴な反復は毎回全体を調べ直すので、無駄があります。次の算法は、各命題について「まだ根拠が揃っていない前提があと何個か」を数えておき、根拠が 1 つ確定するたびに、それを使う命題の数だけを 1 減らします。数が 0 になった命題は、前提が全部揃ったので根拠をもちます。次の証明の (J1)〜(J4) は、この数え方が各時点で正しいことを言うための 4 つの記録です。(J2) が「数は残りの前提の個数に等しい」、(J3) が「待ち行列の中身は確定済みで未処理のもの」、(J1) が「確定したものは本当に根拠をもつ」、(J4) が「数が 0 であることと確定は同じこと」という意味です。 次の算法を考える。 > 各 $s \in P$ について計数 $c[s]$ を $|\mathrm{prem}(s)|$ で初期化し、各 $u \in N$ について、$u$ を前提にもつ $s \in P$ の一覧 $\mathrm{users}[u]$ を作る。集合 $G$ を $B \cup \{s \in P : c[s] = 0\}$ で初期化し、$G$ の元をすべて待ち行列に入れる。待ち行列が空でないかぎり、$u$ を 1 つ取り出し、$\mathrm{users}[u]$ の各 $s$ について $c[s]$ を $1$ 減らし、$0$ になったら $s$ を $G$ に加えて待ち行列に入れる。 この算法は止まり、止まったとき $G = \mathrm{Gr}(K)$ である。依存の総数を $M = \sum_{s \in P} |\mathrm{prem}(s)|$ とすると、計算時間は $O(|N| + M)$ である（）。 待ち行列から取り出し終えた環境の集合を $D$ と書きます。算法の各時点で、次の 4 つが成り立つことを示します。 - (J1) $G \subseteq X^{*}$（$X^{*}$ は の最小不動点）。 - (J2) すべての $s \in P$ について $c[s] = |\mathrm{prem}(s) \setminus D|$。 - (J3) $D \subseteq G$ で、$G \setminus D$ はちょうど待ち行列の中身である。同じ環境が待ち行列に 2 度入ることはない。 - (J4) $s \in P$ について、$s \in G$ と $c[s] = 0$ は同値である。 **初期状態。** $D = \emptyset$ なので (J2) は $c[s] = |\mathrm{prem}(s)|$ で、初期化のとおりです。(J3)(J4) も初期化のとおりです。(J1) は、$B \subseteq \Phi(X^{*}) = X^{*}$ と、$\mathrm{prem}(s) = \emptyset$ である $s \in P$ について $\mathrm{prem}(s) \subseteq X^{*}$ より $s \in \Phi(X^{*}) = X^{*}$ であることから成り立ちます。 **1 回の反復。** $u$ を取り出して $D$ に加えます。(J2) の右辺は、$u \in \mathrm{prem}(s)$ である $s$、すなわち $\mathrm{users}[u]$ の $s$ についてちょうど $1$ 減り、算法も同じ $s$ の $c[s]$ を $1$ 減らすので、(J2) が保たれます。$c[s]$ が $0$ になったとき $s$ を $G$ に加えるので (J4) が保たれます。$c[s]$ は減る一方で、$0$ になるのは 1 度だけなので、$s$ が待ち行列に入るのは高々 1 度で、(J3) が保たれます。新しく $G$ に入る $s$ については、(J2) より $\mathrm{prem}(s) \subseteq D$ で、(J3) と (J1) より $D \subseteq G \subseteq X^{*}$ なので、$s \in \Phi(X^{*}) = X^{*}$ です。よって (J1) が保たれます。 **停止と計算時間。** (J3) より各環境が待ち行列に入るのは高々 1 度なので、反復は高々 $|N|$ 回です。$u$ を取り出したときの仕事は $1 + |\mathrm{users}[u]|$ に比例し、$\sum_u |\mathrm{users}[u]| = \sum_{s \in P} |\mathrm{prem}(s)| = M$ です。初期化も $O(|N| + M)$ でできるので、全体は $O(|N| + M)$ 時間です。 **正しさ。** 止まったとき待ち行列は空なので、(J3) より $G = D$ です。$\Phi(G) \subseteq G$ を示します。$B \subseteq G$ は初期化からです。$s \in P$ かつ $\mathrm{prem}(s) \subseteq G = D$ なら、(J2) より $c[s] = 0$ で、(J4) より $s \in G$ です。 (b) の後半（$\Phi(Y) \subseteq Y$ ならば $X^{*} \subseteq Y$）より $X^{*} \subseteq G$ で、(J1) と合わせて $G = X^{*}$ です。 (c) より $G = \mathrm{Gr}(K)$ です。 この証明は、ループの不変条件を立て、初期状態で成り立つこと・各反復で保たれること・停止時に欲しい結論が出ることを示すという、[契約による設計](/computer-science/software-design-testing/contracts-and-invariants) の方法そのものです（）。算法の形は、前々章の[トポロジカル順](/computer-science/software-design-testing/build-systems-and-dependencies#def-topological-order)を求める Kahn の算法（ (b)）と同じで、違いは、証明のない命題と循環に含まれる命題が最後まで待ち行列に入らずに残る点です。命題論理の Horn 節（「前提がすべて成り立てば結論も成り立つ」という形の規則）の充足可能性を線形時間で判定する Dowling と Gallier の算法も、同じ構造をしています（参考文献）。 ### 4.4. 根拠のない命題の特徴づけ 検査が利用者に報告すべきなのは、「根拠のない命題の一覧」よりも、その**原因**です。次の系は、原因が「証明のない定理類」と「循環」の 2 種類に尽きることを示します。証明では、根拠のある命題に、集合が広がる何段目で入ったかという「階数」を付けます。依存の辺をさかのぼると階数が必ず小さくなるので、循環の上では階数が自分自身より小さくなってしまい、矛盾します。つまり循環の上の命題は根拠をもてません。 環境 $s \in N$ について、次の 2 つは同値である。 (i) $s \notin \mathrm{Gr}(K)$。 (ii) 依存グラフ $G_K$ の頂点 $z$ で、「$z$ は証明のない定理類である（$z \in S \setminus P$）」か「$z$ は $G_K$ のある有向閉路の上にある」のどちらかを満たし、かつ $z = s$ であるか $z$ から $s$ へ $G_K$ の歩道があるものが存在する。 $X^{*} = \mathrm{Gr}(K)$（）を使います。まず 3 つの事実を示します。 **事実 1：証明のない定理類は根拠をもたない。** $z \in S \setminus P$ は $B$ にも $P$ にも属さないので、どの $X$ についても $z \notin \Phi(X)$ で、$z \notin \Phi(X^{*}) = X^{*}$ です。 **事実 2：根拠のない前提をもつ命題は根拠をもたない。** $u \notin X^{*}$ かつ $(u, s) \in E$ とします。辺の定義より $s \in P$、$u \in \mathrm{prem}(s)$ で、$\mathrm{prem}(s) \not\subseteq X^{*}$ です。$s \notin B$ なので $s \notin \Phi(X^{*}) = X^{*}$ です。 **事実 3：有向閉路の上の頂点は根拠をもたない。** 根拠のある環境 $t$ の**階数**を、$t \in X_k$ となる最小の $k \ge 1$ とします（$X_k$ は (b) の列）。$(u, t) \in E$ で $t$ が根拠をもち階数が $k$ なら、$t \in P$ かつ $t \in X_k = \Phi(X_{k-1})$ より $\mathrm{prem}(t) \subseteq X_{k-1}$ で、$u \in X_{k-1}$ です。$X_0 = \emptyset$ なので $k \ge 2$ で、$u$ は根拠をもち、階数は $k - 1$ 以下です。つまり、辺の終点が根拠をもてば、始点も根拠をもち、階数は真に小さくなります。 有向閉路 $(z_0, z_1, \ldots, z_m)$、$z_m = z_0$、$m \ge 1$ の上のある頂点が根拠をもつとします。上のことを辺 $(z_{i-1}, z_i)$ に順に使って閉路を逆向きに 1 周すると、すべての頂点が根拠をもち、階数が $z_0$ から $z_m$ へ向かって真に増えます。$z_m = z_0$ なので、$z_0$ の階数が自分自身より大きいことになり、矛盾です。 **(ii) $\Rightarrow$ (i)。** $z$ は事実 1 または事実 3 より根拠をもちません。$z = s$ ならそれで終わりです。$z$ から $s$ への歩道があるなら、歩道の辺に沿って事実 2 を順に使い、$s$ も根拠をもちません。 **(i) $\Rightarrow$ (ii)。** $s \notin X^{*}$ とします。$u_0 = s$ とおき、次の操作を繰り返します。$u_i$ は根拠をもたないので $u_i \notin B$、すなわち $u_i \in S$ です。$u_i \notin P$ なら、$z = u_i$ として止めます。$u_i \in P$ なら、$u_i \notin \Phi(X^{*})$ より $\mathrm{prem}(u_i) \not\subseteq X^{*}$ なので、根拠をもたない前提 $u_{i+1} \in \mathrm{prem}(u_i)$ を 1 つ選びます。このとき $(u_{i+1}, u_i) \in E$ です。 操作が $u_i \notin P$ で止まった場合、$z = u_i$ は証明のない定理類で、$(u_i, u_{i-1}, \ldots, u_0)$ は $z$ から $s$ への歩道です（$i = 0$ なら $z = s$）。止まらずに $u_0, \ldots, u_{|N|}$ まで続いた場合、$|N| + 1$ 個の頂点の中に同じものがあります（鳩の巣原理、）。$u_i = u_j$、$i < j$ で $j - i$ が最小の組を取ると、$u_i, \ldots, u_{j-1}$ は相異なり、$(u_j, u_{j-1}, \ldots, u_i)$ は有向閉路です。$z = u_i$ はその上にあり、$(u_i, u_{i-1}, \ldots, u_0)$ は $z$ から $s$ への歩道です（$i = 0$ なら $z = s$）。 この系により、閉包の検査の報告は 2 種類に帰着します。**証明のない定理類の一覧**と、**循環の一覧**です。それ以外の根拠のない命題は、この 2 つのどれかを直せば（あるいは依存を外せば）根拠をもつようになります。循環は、根拠のない命題のうち証明をもつものに限ったグラフの上で、深さ優先探索の後退辺として見つかります（）。 題材のサイトの「証明のない定理は、理由と出典を添えて台帳に登録する」という規則は、この系の言葉でいえば、「根拠のなさの原因のうち、意図したものを明示的に列挙しておき、列挙にないものが現れたら誤りにする」ということです。題材のサイトで誤りになるのはこの「台帳にない、証明のない定理類」だけで、証明はあるのに基礎まで届かない定理類（循環に依存するものを含みます）は、それを止めている参照先とともに一覧として報告されます。循環を閉路として取り出す処理は、下の最小の実装で足したものです。 ### 4.5. 最小の実装 19 個の環境をもつ人工の文書の集合に、§3.2 の 4 つの例をすべて仕込みます。 ```yaml # 文書 id → 環境の並び。proof があれば「証明つき」で、中身は証明が参照する名前の並び sets: - {id: def-set, kind: definition} - {id: ax-ext, kind: axiom} - {id: lem-subset, kind: lemma, proof: [def-set, ax-ext]} - {id: prop-union, kind: proposition, proof: [def-set, lem-subset]} - {id: thm-cantor, kind: theorem, proof: [lem-subset, def-set]} order: - {id: def-order, kind: definition} - {id: lem-a, kind: lemma, proof: [def-order, lem-b]} - {id: lem-b, kind: lemma, proof: [lem-a]} - {id: prop-chain, kind: proposition, proof: [def-order, lem-a]} - {id: thm-zorn, kind: theorem} - {id: cor-max, kind: corollary, proof: [thm-zorn, def-order]} numbers: - {id: def-nat, kind: definition} - {id: ax-induction, kind: axiom} - {id: def-prime, kind: definition} - {id: thm-wo, kind: theorem, proof: [ax-induction, def-nat, "sets#lem-subset"]} - {id: lem-euclid, kind: lemma, proof: [thm-wo]} - {id: prop-div, kind: proposition, proof: [thm-wo, lem-eucild]} - {id: cor-gcd, kind: corollary, proof: [lem-euclid, "order#thm-max"]} - {id: thm-prime, kind: theorem, proof: [cor-gcd, prop-div, def-prime]} ``` 参照の解決（）、待ち行列の算法（）、循環の検出を実装します。これは題材のサイトのスクリプトではなく、この記事のために書いた最小の実装です。 ```python # Python 3.9.6 / PyYAML 6.0.3（ファイル名 checks.py） from collections import deque import yaml BASE = {"definition", "axiom"} # 証明がなくても根拠をもつ種類 def load(corpus): """索引（鍵 → 環境）と、重複した鍵の一覧を返す。鍵は「文書 id#環境 id」""" index, duplicates = {}, [] for doc, envs in corpus.items(): for env in envs: key = f"{doc}#{env['id']}" if key in index: duplicates.append(key) index[key] = env return index, duplicates def resolve(index): """証明の中の参照を鍵に直す。prem: 鍵 → 解決できた前提の集合、unresolved: (参照元, 書かれた名前)""" prem, unresolved = {}, [] for key, env in index.items(): doc = key.split("#")[0] prem[key] = set() for name in env.get("proof", []): target = name if "#" in name else f"{doc}#{name}" # 文書内の名前には文書 id を補う if target in index: prem[key].add(target) else: unresolved.append((key, name)) return prem, unresolved def grounded(index, prem): """待ち行列の算法。根拠のある鍵の集合を返す""" proved = {k for k, e in index.items() if "proof" in e} count = {k: len(prem[k]) for k in proved} # まだ処理されていない前提の数 users = {k: [] for k in index} for k in proved: for u in prem[k]: users[u].append(k) ok = {k for k, e in index.items() if e["kind"] in BASE} | {k for k in proved if count[k] == 0} queue = deque(sorted(ok)) while queue: u = queue.popleft() for k in users[u]: count[k] -= 1 if count[k] == 0: ok.add(k) queue.append(k) return ok def find_cycle(nodes, prem): """nodes の中で前提をたどる深さ優先探索。閉路を 1 つ返す（なければ None）""" color, stack = {}, [] def visit(k): color[k] = "gray"; stack.append(k) for u in sorted(prem[k] & nodes): if color.get(u) == "gray": return stack[stack.index(u):] + [u] if u not in color: found = visit(u) if found: return found color[k] = "black"; stack.pop() for k in sorted(nodes): if k not in color: found = visit(k) if found: return found if __name__ == "__main__": index, duplicates = load(yaml.safe_load(open("corpus.yaml", encoding="utf-8"))) prem, unresolved = resolve(index) ok = grounded(index, prem) bad = set(index) - ok unproved = sorted(k for k in bad if "proof" not in index[k]) print("環境の数:", len(index), " 重複した鍵:", duplicates) print("未解決の参照:", unresolved) print("根拠のある命題:", len(ok), " 根拠のない命題:", sorted(bad)) print(" うち証明のないもの:", unproved) print(" 循環:", " ← ".join(find_cycle(bad - set(unproved), prem))) ``` ```text 環境の数: 19 重複した鍵: [] 未解決の参照: [('numbers#prop-div', 'lem-eucild'), ('numbers#cor-gcd', 'order#thm-max')] 根拠のある命題: 14 根拠のない命題: ['order#cor-max', 'order#lem-a', 'order#lem-b', 'order#prop-chain', 'order#thm-zorn'] うち証明のないもの: ['order#thm-zorn'] 循環: order#lem-a ← order#lem-b ← order#lem-a ``` （循環の表示の `x ← y` は「`x` の証明が `y` を使う」の意味です。） 4 つの例が、それぞれ別の報告として現れています。綴り違い `lem-eucild` と存在しない `order#thm-max` は未解決の参照に、循環する `lem-a`・`lem-b` は循環に、証明のない `thm-zorn` は証明のない定理類に出ました。根拠のない 5 つの命題のうち、残りの `prop-chain` は循環の上の `lem-a` に、`cor-max` は証明のない `thm-zorn` に依存しています。 のとおり、原因は 2 種類に尽きます。 1 つ注意があります。この実装は、未解決の参照を前提から外して閉包を計算しています（ の定義どおりです）。そのため、未解決の参照を含む `prop-div` と `cor-gcd` は「根拠のある命題」に数えられています。閉包の検査の結果が意味をもつのは、参照の検査に合格している、つまり未解決の参照が 1 つもないときだけです。検査の間にも依存関係があり、実行の順序は「一意性 → 参照の解決 → 閉包」でなければなりません。 ### 4.6. 実装を性質ベーステストで確かめる は算法の正しさを証明していますが、上の Python の実装がその算法を正しく写しているかは別の問題です。そこで、[性質ベーステスト](/computer-science/software-design-testing/property-based-testing) の方法で、「待ち行列の実装の結果は、 (b) の素朴な反復の結果と一致する」という性質を、乱数で作った依存グラフで調べます。素朴な反復は遅いですが、定義をそのまま書いただけなので誤りにくく、**参照実装**の役をします。 比較のために、わざと誤りを入れた版も用意します。前提の数を、集合の大きさではなく参照の出現回数で数える、という誤りです。生成と[縮約](/computer-science/software-design-testing/property-based-testing#def-shrinking)は標準ライブラリの `random` で自作しました（専用のライブラリは使っていません）。 ```python # Python 3.9.6 / PyYAML 6.0.3／乱数種 20261008 import random from collections import deque from checks import BASE, grounded def naive(index, prem): """素朴な不動点反復: X ← 基礎 ∪ {証明つきで前提がすべて X に入る命題} を変わらなくなるまで""" x = set() while True: y = {k for k, e in index.items() if e["kind"] in BASE or ("proof" in e and prem[k] <= x)} if y == x: return x x = y def grounded_buggy(index, prem, refs): """故意の誤り: 前提の数を「参照の出現回数」で数える（同じ前提を 2 度参照すると 0 にならない）""" proved = {k for k, e in index.items() if "proof" in e} count = {k: len(refs[k]) for k in proved} users = {k: [] for k in index} for k in proved: for u in prem[k]: users[u].append(k) ok = {k for k, e in index.items() if e["kind"] in BASE} | {k for k in proved if count[k] == 0} queue = deque(sorted(ok)) while queue: u = queue.popleft() for k in users[u]: count[k] -= 1 if count[k] == 0: ok.add(k); queue.append(k) return ok def random_case(rng, size): """size 個の環境と、重複・循環・未証明を含みうる参照をもつ人工の文書集合""" keys = [f"d#e{i}" for i in range(size)] index, refs = {}, {} for k in keys: r = rng.random() if r < 0.25: index[k] = {"kind": "definition"} elif r < 0.35: index[k] = {"kind": "theorem"} # 証明なし else: index[k] = {"kind": "lemma", "proof": True} refs[k] = [rng.choice(keys) for _ in range(rng.randint(0, 3))] if "proof" in index[k] else [] return index, refs def shrink(index, refs, fails): """失敗を保つかぎり、参照を 1 つ消す・環境を 1 つ消す、を繰り返す（大きさが真に減るので止まる）""" changed = True while changed: changed = False for k in list(index): for i in range(len(refs[k])): cand = {**refs, k: refs[k][:i] + refs[k][i + 1:]} if fails(index, cand): refs, changed = cand, True break rest = {j: e for j, e in index.items() if j != k} cand = {j: [u for u in refs[j] if u != k] for j in rest} if rest and fails(rest, cand): index, refs, changed = rest, cand, True return index, refs def run(candidate, cases=2000): rng = random.Random(20261008) fails = lambda index, refs: candidate(index, {k: set(v) for k, v in refs.items()}, refs) != naive(index, {k: set(v) for k, v in refs.items()}) for n in range(cases): index, refs = random_case(rng, rng.randint(1, 12)) if fails(index, refs): index, refs = shrink(index, refs, fails) return f"{n + 1} 件目で不一致。縮約後: " + ", ".join(f"{k}({index[k]['kind']}){refs[k]}" for k in index) return f"{cases} 件すべて一致" print("待ち行列の算法 :", run(lambda index, prem, refs: grounded(index, prem))) print("誤りを入れた算法 :", run(grounded_buggy)) ``` ```text 待ち行列の算法 : 2000 件すべて一致 誤りを入れた算法 : 45 件目で不一致。縮約後: d#e1(lemma)['d#e3', 'd#e3'], d#e3(definition)[] ``` 正しい実装は 2000 件で参照実装と一致しました。誤りを入れた版は 45 件目で食い違い、縮約の結果、「1 つの補題が同じ定義を 2 度参照している」という 2 つの環境だけの反例が残りました。誤りの原因がそのまま読める大きさです。実際の記事でも、1 つの証明が同じ定理を何度も参照するのは普通のことなので、この誤りは実物の入力で必ず現れます。 2000 件の一致は、実装が正しいことの証明ではありません。この生成の仕方では見つからない誤りがないとは言えないからです（）。算法の正しさは定理が、実装が算法を写していることはテストが、それぞれ別の強さで支えています。 ## 5. 決定的な生成：番号と期待出力 ### 5.1. 採番 文書の集合 $K$ から成果物（番号の表、索引、ページ）を作る手続きが**決定的**であるとは、成果物が $K$ だけの関数であること、すなわちファイルを読む順序・並列度・実行時刻・実行する計算機によらないことをいう。 これは [ビルドと依存関係](/computer-science/software-design-testing/build-systems-and-dependencies) の再現可能なビルドと同じ要求です。 各文書 $d$ は節に分かれ、各環境 $e$ はある節 $\mathrm{sec}(e) \in \mathbb{N}$ に属するとする。 (a) 環境 $e$（文書 $d$ の成分）の番号を $$ \mathrm{num}(e) = \bigl(\mathrm{sec}(e),\ \ 1 + \#\{\, e' : e' \text{ は } \mathrm{env}(d) \text{ の中で } e \text{ より前にあり、} \mathrm{sec}(e') = \mathrm{sec}(e) \,\}\bigr) $$ と定めると、$\mathrm{num}(e)$ は文書 $d$ の内容だけで決まる。したがって採番は決定的である。 (b) サイト全体で 1 つのカウンタを持ち、文書をある順序 $\pi$ で読みながら、環境に出会うたびにカウンタを $1$ 増やしてその値を番号にする方式を考える。文書が 2 つ以上あり、どの文書も環境を 1 つ以上もつならば、この方式の番号は $\pi$ に依存する。 (c) 文書 $d'$ のページが、文書 $d$ の環境 $e$ への参照を「定理 $\mathrm{num}(e)$」と表示するならば、$d'$ のページを作るタスクの出力は $d$ の内容に依存する。このタスクが番号の表（索引）を依存に宣言していれば、増分ビルドの結果はクリーンビルドの結果と一致する。 **(a)。** 右辺に現れるのは、$\mathrm{env}(d)$ の中での $e$ の位置と、$\mathrm{env}(d)$ の各成分の節だけです。どちらも文書 $d$ の内容で、ほかの文書にも、$d$ がいつ・何番目に読まれたかにもよりません。 **(b)。** 相異なる 2 つの文書 $d_1, d_2$ を取り、$d_1$ の最初の環境を $e_1$ とします。$d_1$ を最初に読む順序 $\pi$ では $e_1$ の番号は $1$ です。$d_2$ を最初に、$d_1$ を 2 番目に読む順序 $\pi'$ では、$e_1$ の番号は $1 + |\mathrm{env}(d_2)| \ge 2$ です。 **(c)。** 前半は表示の仕方から従います。$d$ の中で $e$ より前に同じ節の環境を 1 つ足すと $\mathrm{num}(e)$ が変わり、$d'$ のページの文字列が変わるからです。後半は、番号の表を作るタスク（すべての文書を依存にもつ）と、各ページを作るタスク（自分の文書と番号の表を依存にもつ）からなるビルドの記述が密閉的なので、 から従います。 題材のサイトの採番は (a) の形です。見出し「`## N.`」が節番号になり、節の中で定理・定義・例などの種類をまたいで通し番号が振られます。(c) は、[ビルドと依存関係](/computer-science/software-design-testing/build-systems-and-dependencies) の §5 の実行例で、文書 `a.md` の識別子を足すと `page_b` まで再実行された理由です。逆に、本文だけを直して環境の並びが変わらなければ、番号の表は変わらず、ほかの文書のページは作り直されません（早期打ち切り）。 2 つの方式を、ファイルの列挙順を変えて比べます。 ```python # Python 3.9.6（標準ライブラリのみ） DOCS = { # 文書 → (節番号, 環境 id) の出現順の並び "limits.mdx": [(2, "def-limit"), (3, "thm-unique"), (3, "prop-sum")], "series.mdx": [(2, "def-series"), (2, "thm-comparison")], "integral.mdx": [(3, "thm-ftc")], } def number_by_scan(file_order): """走査順に依存する採番: サイト全体で 1 つのカウンタを回す""" out, counter = {}, 0 for doc in file_order: for _, env in DOCS[doc]: counter += 1 out[f"{doc}#{env}"] = str(counter) return out def number_by_position(file_order): """出現順の関数としての採番: 「節番号.節内の通し番号」。文書の中身だけで決まる""" out = {} for doc in file_order: seen = {} for section, env in DOCS[doc]: seen[section] = seen.get(section, 0) + 1 out[f"{doc}#{env}"] = f"{section}.{seen[section]}" return out orders = [["limits.mdx", "series.mdx", "integral.mdx"], ["integral.mdx", "limits.mdx", "series.mdx"]] for fn in (number_by_scan, number_by_position): a, b = (fn(o) for o in orders) diff = sorted(k for k in a if a[k] != b[k]) print(fn.__name__, "→ 列挙順で番号が変わる環境:", len(diff), "/", len(a)) print(" ", {k.split("#")[1]: (a[k], b[k]) for k in sorted(a)}) ``` ```text number_by_scan → 列挙順で番号が変わる環境: 6 / 6 {'thm-ftc': ('6', '1'), 'def-limit': ('1', '2'), 'prop-sum': ('3', '4'), 'thm-unique': ('2', '3'), 'def-series': ('4', '5'), 'thm-comparison': ('5', '6')} number_by_position → 列挙順で番号が変わる環境: 0 / 6 {'thm-ftc': ('3.1', '3.1'), 'def-limit': ('2.1', '2.1'), 'prop-sum': ('3.2', '3.2'), 'thm-unique': ('3.1', '3.1'), 'def-series': ('2.1', '2.1'), 'thm-comparison': ('2.2', '2.2')} ``` 1 つのカウンタを回す方式では、列挙順を変えただけで 6 個すべての番号が変わりました。ディレクトリの中のファイルが返ってくる順序はファイルシステムによって違うので、この方式は「私の環境では定理 3 だった」という食い違いを生みます。出現順の関数にした方式では 1 つも変わりません。番号が文書をまたいで一意でなくなる（`thm-ftc` と `thm-unique` がどちらも 3.1）のは、番号を「文書の名前と組にして」表示することで補います。 ### 5.2. 黄金テスト 生成の結果が変わっていないことを確かめるのに、期待出力を保存しておいて比べるテストがよく使われます。 生成の手続き $\mathrm{gen}$ の出力を、保存しておいた期待出力 $g$ と比べ、等しければ合格とするテストを**黄金テスト**という。 (a) $\mathrm{gen}$ が決定的ならば、黄金テストは決定的な検査である。 (b) 同じ入力 $K$ に対して、$\mathrm{gen}$ の出力が相異なる 2 つの値 $o_1, o_2$ をそれぞれ正の確率 $\pi_1, \pi_2$ でとるならば、どんな $g$ を保存しても、合格する確率は $1 - \min(\pi_1, \pi_2)$ 以下である。入力もコードも変えていないのに落ちることがあるので、[前章](/computer-science/software-design-testing/continuous-integration) の意味で不安定なテストである（合格する確率が $0$ の場合は、決して通らないテストである）。 (c) 写像 $\nu$（**正規化**）を挟んで「$\nu(\mathrm{gen}(K)) = \nu(g)$ ならば合格」とするテストは、$\nu \circ \mathrm{gen}$ が決定的ならば決定的である。このテストが検出する誤った出力は $\nu(o) \ne \nu(g)$ を満たす $o$ にちょうど一致し、$o \ne g$ であっても $\nu(o) = \nu(g)$ である誤りは検出されない。 **(a)。** $\mathrm{gen}(K)$ が $K$ だけの関数なら、「$\mathrm{gen}(K) = g$ か」も $K$ と $g$ だけで決まります。 **(b)。** $o_1 \ne o_2$ なので、$g$ はこの 2 つのうち高々一方としか等しくありません。$g \ne o_1$ なら、確率 $\pi_1$ で出力が $o_1$ となって不合格になり、$g \ne o_2$ なら確率 $\pi_2$ で不合格になります。どちらの場合も不合格の確率は $\min(\pi_1, \pi_2)$ 以上で、合格の確率は $1 - \min(\pi_1, \pi_2) < 1$ 以下です。 **(c)。** 前半は (a) と同じです。後半は合格の条件の言い換えで、出力 $o$ が不合格になるのは $\nu(o) \ne \nu(g)$ のときで、そのときに限ります。 出力を非決定的にするものは、生成物に埋め込んだ日時、辞書や集合の走査順（ハッシュ値に依存する順）、並列に処理した結果を完了順に並べること、一時ファイルの名前などです。対策は 2 通りあります。1 つは生成そのものを決定的にすること（鍵を整列して出力する、日時を入力として渡す）、もう 1 つは比べる前に正規化することです。 (c) は、正規化が安全でない場合を示しています。たとえば、行の順序のゆらぎを消すために「行を整列してから比べる」正規化を入れると、定理の一覧が誤った順序で出力されるようになっても検出されません。日時を取り除く正規化は、更新日が誤って表示される不具合を隠します。正規化は「この違いは誤りではない」という宣言なので、消す範囲は非決定性の源にちょうど合わせ、広げすぎないようにします。[変成関係](/computer-science/software-design-testing/property-based-testing#def-metamorphic)による検査が「関係を保つ誤り」を検出できないのと同じ構造です（[性質ベーステスト](/computer-science/software-design-testing/property-based-testing) の章を参照してください）。できるなら、正規化より生成の決定化を選ぶのがよいと思います。決定的な生成は、テストだけでなく、キャッシュと増分ビルドの前提でもあるからです。 ## 6. 検査にできること、できないこと ### 6.1. 健全性と完全性 各文書の集合 $K$ に「本当の違反」の集合 $V(K)$ を対応させる規則 $V$ を**性質**と呼ぶ。検査 $\kappa$ が性質 $V$ について - **健全**であるとは、すべての $K$ で $\kappa(K) \subseteq V(K)$（報告された違反は本当に違反である）、 - **完全**であるとは、すべての $K$ で $V(K) \subseteq \kappa(K)$（違反はすべて報告される） が成り立つことをいう。 健全でない検査は誤検出を出し、完全でない検査は見逃しを出します。誤検出の多い検査は無視されるようになり、見逃しのある検査は安心の根拠になりません。 次の命題は、「綴りや参照の有無のような文字列の形で決まる性質」なら両方を満たす検査が作れるが、「プログラムを実行したときの振る舞い」で決まる性質ではそれが作れない、と述べています。(b) の証明は、そのような検査があれば、別の章で示された「必ず止まる健全な検査は取りこぼしを避けられない」という結果に反する、という形で進みます。 (a) 条件 (U) を満たす文書の集合について、「解決できない参照」という性質 $V(K) = U(K)$ に対し、索引を作って各参照を引く検査は、必ず止まり、健全かつ完全である。 (b) チューリング完全なプログラミング言語 $\mathcal{L}$ を固定し、各環境が $\mathcal{L}$ のプログラムを 1 つ含むとする。性質 $V$ を「実行すると型エラーで停止するプログラムを含む環境」の集合とする。このとき、どんな入力に対しても必ず止まる検査で、$V$ について健全かつ完全なものは存在しない。 **(a)。** より、索引 $\mathrm{Idx}(K)$ は有限の表で、各参照 $r$ について $\mathrm{key}(d, r)$ を計算して表を引けば、$\mathrm{res}(d, r)$ が定義されるかどうかが有限の手間で分かります。未定義のものをすべて報告すれば、報告の集合は定義により $U(K)$ に等しく、健全かつ完全です。 **(b)。** 必ず止まり、$V$ について健全かつ完全な検査 $\kappa$ があったとします。プログラム $p$ に対し、$p$ を含む環境 1 つだけからなる文書の集合を $K_p$ とし、 $$ C = \{\, p \in \mathcal{L} : \kappa(K_p) = \emptyset \,\} $$ とおきます。$\kappa$ は必ず止まるので、$p \in C$ かどうかは有限時間で判定できます。$\mathcal{P}$ を「実行しても型エラーで停止しないプログラム」の全体とします。$\kappa$ が完全なので、$p \notin \mathcal{P}$（型エラーで停止する）ならば $p$ の環境は報告され、$p \notin C$ です。すなわち $C \subseteq \mathcal{P}$ です。 $C$ は決定可能で $C \subseteq \mathcal{P}$ なので、健全な静的検査の不完全性の定理（）より $C \subsetneq \mathcal{P}$ で、$p_0 \in \mathcal{P} \setminus C$ が存在します。$p_0 \notin C$ なので $\kappa(K_{p_0}) \ne \emptyset$、つまり $p_0$ の環境が報告されています。しかし $p_0 \in \mathcal{P}$ なので、これは本当の違反ではありません。$\kappa$ が健全であることに反します。 (a) と (b) の違いは、性質が文字列の形だけで決まるか（構文的）、プログラムの振る舞いで決まるか（意味的）です。(b) の $V$ を「この証明は正しい」に置き換えると、事情はさらに悪くなります。自然言語で書かれた証明の「正しさ」は、そもそも機械が扱える形に定義されていません。 そこで題材のサイトは、意味的な性質の**代理**として、構文的に検査できる性質を選んでいます。 | 本当に欲しい性質（意味的） | 実際に検査している性質（構文的） | |---|---| | すべての定理が正しく証明されている | すべての定理類に証明の環境がある（ないものは台帳にある） | | 証明が使っている事実は、すべて先に確立されている | 証明の中の参照がすべて解決し、たどると基礎に届く | | 演習問題は、記事の定理だけで解ける | 問題が「使う定理」として挙げた名前がすべて解決する | 右の列の検査は、右の列の性質については健全かつ完全です（ (a) と ）。左の列の性質については、健全でも完全でもありません。 次の補題を考えます。 > **補題。** すべての実数 $x$ について $x^2 > 0$ である。 > **証明。** 実数の順序の公理（参照あり）より、$x > 0$ なら $x \cdot x > 0$。$x < 0$ なら $-x > 0$ なので $x^2 = (-x)(-x) > 0$。∎ 証明は実数の順序の公理を参照していて、参照は解決し、公理は基礎です。閉包の検査は、この補題を「根拠のある命題」に数えます。しかし補題は偽です。$x = 0$ の場合が抜けていて、$0^2 = 0$ は正ではありません。依存の宣言は正しいのに、推論が誤っています。 逆向きのずれもあります。 - **参照のない依存。** 証明が、ある定理を使っているのに、参照を書かずに「よく知られているように」と述べている。依存グラフにその辺がないので、使われた定理に証明がなくても検査は通る。 - **見かけの違反。** 定理の証明が、定理の直後ではなく付録にまとめて書かれていて、証明の環境として対応づけられていない。検査は「証明のない定理」と報告するが、証明は実際にはある。 機械の検査が見ているのは「証明が何に依存すると**宣言している**か」です。宣言と実際の推論が一致しているか、推論の各段が正しいかは、人が読んで確かめるしかありません。題材のサイトでは、書き手とは別の主体が独立に監査し、その結果（合格・修正・要対応）を記事ごとの来歴として記録する、という分担にしています。機械は「全件を、毎回、同じ基準で」調べることに、人は「この段は本当に成り立つか」を判断することに向いています。 証明の正しさまで機械に検査させる道もあります。証明を Lean や Coq などの証明支援系の言語で書けば、検査器は各推論の段が規則に合っているかを確かめます。その場合、検査しているのは形式的な導出の構文で、やはり構文的な検査ですが、形式体系の健全性を通じて意味的な保証が得られます。代償は、証明を形式言語で書く手間です。題材のサイトのような自然言語の教科書は、その手間をかけずに「依存の宣言」という一段弱い性質だけを機械に任せる、という中間の設計を取っています。識別子で定理を指し、番号を機械に振らせる仕組みそのものは、Stacks Project のような大規模な数学の文書でも使われています（参考文献）。 ### 6.2. 文書ごとの検査と、文書をまたぐ検査 (a) 検査 $\kappa$ が、各文書 $d$ の内容だけから決まる違反の集合 $\kappa_d$ の和集合 $\kappa(K) = \bigcup_{d \in \mathrm{Doc}} \kappa_d$ であるとする。このとき、文書をどの順序で、いくつに分けて並列に処理しても $\kappa(K)$ は同じである。また、文書 $d$ だけが変更されたとき、$\kappa_d$ だけを計算し直して和集合を取り直せば、全体を計算し直した結果に一致する。 (b) 参照の検査の、文書 $d$ に関する部分 $U_d = \{(d, e, r) \in U(K)\}$ は、$d$ の内容と索引 $\mathrm{Idx}(K)$ の定義域（鍵の集合）から決まる。「鍵の集合を作るタスク」が全文書を依存に、「$U_d$ を作るタスク」が $d$ と鍵の集合を依存に宣言していれば、増分的な実行の結果は全体を計算し直した結果に一致する。さらに、内容の比較による早期打ち切りのもとでは、文書 $d'$ の変更が鍵の集合を変えないかぎり、$d \ne d'$ の $U_d$ は再計算されない。 **(a)。** 和集合は、取る順序にも、まとめ方にもよりません。増分化については、各 $d$ に「$\kappa_d$ を作るタスク」（依存は $d$ だけ）と、「和集合を作るタスク」（依存はすべての $\kappa_d$）を置いたビルドの記述を考えます。$\kappa_d$ が $d$ の内容だけで決まるという仮定は、この記述が密閉的であることを意味します。$d$ だけが変わったとき、$d$ から到達できるタスクは $\kappa_d$ のタスクと和集合のタスクだけなので、 より、この 2 つを再実行した結果はクリーンビルドの結果に一致します。 **(b)。** $(d, e, r) \in U(K)$ かどうかは、$r$ が $d$ の環境 $e$ の証明に書かれていること（$d$ の内容）と、$\mathrm{key}(d, r)$ が索引の定義域に属さないこと（鍵の集合）で決まります。よって、述べた依存の宣言のもとで記述は密閉的で、 より増分的な実行は正しい結果を与えます。最後の主張は です。$d'$ を変更して鍵の集合を作り直した結果が前回と同じなら、$U_d$ のタスク（$d \ne d'$）の依存はどれも変わっていないので、実行されません。 書式の検査（数式の構文、禁止する表現、分量）は (a) の形で、文書ごとに独立です。参照の検査と閉包の検査は (b) の形で、索引という中間生成物を通して全文書に依存します。 (b) の依存の宣言を忘れると、次のような見逃しが起きます。文書 `order` から定理 `thm-max` を消したとします。変更されたのは `order` だけなので、「変更された文書だけを検査する」という素朴な増分化は `order` だけを調べ、何も見つけません。しかし `numbers` の中の `order#thm-max` への参照は、いま切れました。参照の検査では、**変更していない文書が違反になる**のです。題材のサイトが、検査を変更されたファイルだけに限らず全記事に対して実行するのは、検査が十分速いことに加えて、この種の見逃しを構造的に避けるためだと読めます。 ## 7. 公開の不変条件と、検査の水準を上げる移行
検査（版 c） 生成 gen(c) 公開 合格 同じ c 不合格なら、ここで止まる
版 $c$ に対する決定的な検査を $\chi$、生成を $\mathrm{gen}$ とし、公開されている成果物の時間的な列を $a_0, a_1, a_2, \ldots$ とする。 (a) 次の 3 つを仮定する。(G1) 公開物が更新されるのは、パイプライン「検査 → 生成 → 公開」が最後まで成功したときだけである。(G2) 生成は、検査が合格を返したのと同じ版 $c$ を入力にする。(G3) 公開は、その生成の出力 $\mathrm{gen}(c)$ をそのまま公開物にする。このとき、$a_0$ が「ある版 $c$ について $\chi(c) = \text{合格}$ かつ $a_0 = \mathrm{gen}(c)$」を満たせば、すべての $k$ について $a_k$ も同じ条件を満たす。 (b) （台帳つきの検査）違反の集合を返す決定的な検査 $\kappa$ と、許容する違反の集合 $A$（**台帳**）に対し、$\chi_A(c) = \text{合格}$ を $\kappa(c) \subseteq A$ で定める。検査を導入する時点の版を $c_0$ とし、$A_0 = \kappa(c_0)$ とおく。以後、合格した版の列 $c_1, c_2, \ldots$ について、台帳を $A_{k} = A_{k-1} \cap \kappa(c_k)$ と更新する（$c_k$ は $\chi_{A_{k-1}}$ に合格したものとする）。このとき - $\chi_{A_0}(c_0) = \text{合格}$（導入した瞬間にパイプラインは止まらない）、 - すべての $k \ge 1$ で $\kappa(c_k) = A_k \subseteq A_{k-1} \subseteq \cdots \subseteq A_0$（台帳にない違反は 1 件も入らず、台帳は増えない）、 - $A_k = \emptyset$ となった後は、$\chi_{A_k}$ は「違反が 1 件もない」という台帳なしの検査に一致する。 **(a)。** 公開物が更新された回数 $k$ についての帰納法（ を $k + 1$ に適用）です。$k = 0$ は仮定です。$a_k$ が条件を満たすとします。$a_{k+1}$ への更新は、(G1) より、ある版 $c$ についてパイプラインが最後まで成功したときに起きます。検査の段階が成功しているので $\chi(c) = \text{合格}$ で、(G2) より生成の入力は同じ $c$、(G3) より $a_{k+1} = \mathrm{gen}(c)$ です。よって $a_{k+1}$ も条件を満たします。これは、マージキューが主ブランチの不変条件を保つことの証明（ (a)）と同じ形の帰納法です。 **(b)。** $\kappa(c_0) = A_0$ なので $\kappa(c_0) \subseteq A_0$ で、$\chi_{A_0}(c_0)$ は合格です。$k \ge 1$ について、$c_k$ は $\chi_{A_{k-1}}$ に合格しているので $\kappa(c_k) \subseteq A_{k-1}$ で、$A_k = A_{k-1} \cap \kappa(c_k) = \kappa(c_k)$ です。したがって $A_k \subseteq A_{k-1}$ で、これを繰り返して $A_k \subseteq A_0$ です。$A_k = \emptyset$ のとき、$\chi_{A_k}(c) = \text{合格}$ は $\kappa(c) \subseteq \emptyset$、すなわち $\kappa(c) = \emptyset$ と同値です。 (a) の 3 つの仮定は、それぞれ具体的な事故に対応します。(G1) が破れるのは、手元で生成したものを直接公開先に置く経路が残っている場合です。(G2) が破れるのは、検査のあとで生成の段階が「最新の」ソースを取り直す場合で、検査と生成の間に別の変更が入ると、検査していない版が生成されます。版をコミットのハッシュで指定すれば、検査した内容と生成する内容が同じであることが保証されます（）。(G3) が破れるのは、生成物に公開の直前で手を入れる処理（後から差し込むスクリプトなど）が、検査の対象になっていない場合です。 (b) は、既存の違反が多数あるところに新しい検査を入れるための定石です。違反をすべて直してから検査を入れようとすると、直している間に新しい違反が増えます。先に検査を入れ、いまある違反を台帳に登録して凍結すれば、その瞬間から新しい違反は増えなくなり、台帳は減るだけになります。題材のサイトの「証明のない定理の台帳」はこの形で、台帳にない主張のみの定理が現れると検査が失敗します。 台帳に項目を**足す**操作は、(b) の更新の規則の外にあります。題材のサイトでは、研究の最前線の結果のように証明を載せられない定理に限り、理由と出典を定理の直後に書いたうえで台帳に足すことを認めています。これは検査を弱める操作なので、機械的に行わず、理由を記録に残す人の判断として扱う、という設計です。単調性を破る操作を禁止するのではなく、破るときに必ず痕跡が残るようにしているわけです。 ## 8. まとめ：4 つの層が 1 つの系でどう組み合わさるか | 層 | このテーマの章 | 検査系での現れ方 | |---|---|---| | 契約と不変条件 | [契約による設計](/computer-science/software-design-testing/contracts-and-invariants) | 識別子の一意性は索引の表現不変条件（）。待ち行列の算法の正しさはループ不変条件で証明する（）。公開の不変条件は帰納法で保つ（） | | テスト | [テストの理論](/computer-science/software-design-testing/testing-theory)、[性質ベーステスト](/computer-science/software-design-testing/property-based-testing) | 検査は「文書の集合から違反の集合への関数」で、健全性と完全性で評価する（）。検査の実装は参照実装との一致で確かめ、期待出力との比較は決定性を前提にする（） | | ビルド | [ビルドと依存関係](/computer-science/software-design-testing/build-systems-and-dependencies) | 命題の依存グラフは、タスクの依存グラフと同じ算法で解析する。索引と番号の表は中間生成物で、依存として宣言する（、） | | CI | [継続的インテグレーション](/computer-science/software-design-testing/continuous-integration) | 検査 → 生成 → 公開の段階と、台帳による水準の引き上げ（） | この検査系が教えてくれることを 1 つにまとめるなら、**「機械に任せる性質を、機械が健全かつ完全に検査できる形に選ぶ」**ということです。証明の正しさは検査できませんが、依存の宣言は検査できます。番号が正しいことは検査しにくいですが、番号を出現順の関数として定義してしまえば、検査の必要がなくなります。検査できない部分は消えるわけではなく、人の監査に残ります。どこまでが機械の保証で、どこからが人の判断かが仕様に書かれていることが、この種の系の信頼性を決めます。 ## 9. 演習 基礎が $B = \{D\}$（定義 1 つ）、証明をもつ定理類が $P = \{L_1, L_2, L_3, T\}$ で、 $$ \mathrm{prem}(L_1) = \{D\},\quad \mathrm{prem}(L_2) = \{L_1, L_3\},\quad \mathrm{prem}(L_3) = \{L_2\},\quad \mathrm{prem}(T) = \{L_1, Z\} $$ とする。$Z$ は証明のない定理である。 1. (b) の列 $X_0, X_1, X_2, \ldots$ を、変わらなくなるまで求めよ。 2. 根拠のない各環境について、 (ii) の $z$ を挙げよ。 3. $Z$ に、$D$ だけを参照する証明を付けた。根拠のある環境の集合はどう変わるか。 1. $X_0 = \emptyset$。$X_1 = \Phi(\emptyset) = B \cup \{s \in P : \mathrm{prem}(s) = \emptyset\} = \{D\}$。$X_2 = \Phi(\{D\}) = \{D, L_1\}$（$\mathrm{prem}(L_1) = \{D\} \subseteq X_1$）。$X_3 = \Phi(\{D, L_1\})$ では、$L_2$ は $L_3$ が入っていないので加わらず、$L_3$ は $L_2$ が入っていないので加わらず、$T$ は $Z$ が入っていないので加わらない。よって $X_3 = \{D, L_1\} = X_2$ で、$X^{*} = \{D, L_1\}$。 2. 根拠のない環境は $L_2, L_3, T, Z$。$Z$ は証明のない定理類なので $z = Z$ 自身。$T$ は $Z$ を前提にもつので $z = Z$（辺 $(Z, T)$）。$L_2$ と $L_3$ は有向閉路 $(L_2, L_3, L_2)$ の上にあるので、$z$ は自分自身でよい。 3. $\mathrm{prem}(Z) = \{D\}$ となり、$Z \in P$。列は $X_1 = \{D\}$、$X_2 = \{D, L_1, Z\}$、$X_3 = \{D, L_1, Z, T\}$、$X_4 = X_3$。$T$ が根拠をもつようになる。$L_2$ と $L_3$ は循環のままで、根拠をもたない。循環は、どちらかの証明を、もう一方を使わない形に書き直さないかぎり解消しない。 次の 2 つの場合について、§4.5 の実装（待ち行列の算法）がどう振る舞うかを、計数 $c[s]$ の動きで説明せよ。 1. 補題 $A$ の証明が、定義 $D$ と $A$ 自身を参照している。 2. 基礎に「例」を含めることにし、定理 $T$ の証明が例 $E$ だけを参照している。例 $E$ の本文には、証明のない主張が書かれている。 2 について、検査の設計としてどう対処すればよいかも述べよ。 1. $\mathrm{prem}(A) = \{D, A\}$ なので $c[A] = 2$ で始まる。$D$ が待ち行列から取り出されると $c[A] = 1$ になる。残る前提は $A$ 自身で、$A$ は $c[A] = 0$ にならないかぎり待ち行列に入らず、待ち行列に入らないかぎり $c[A]$ は減らない。$c[A] = 1$ のまま算法は止まり、$A$ は根拠をもたない。依存グラフでは自己ループ $(A, A)$ が長さ $1$ の有向閉路で、 の循環の場合に当たる。なお、題材のサイトの閉包の計算は、証明の中で自分自身を指す参照（「この補題の主張の前半より」のような書き方）を依存に数えないことにして、この見かけの循環を避けている。 2. $E$ は基礎なので最初から $G$ に入り、待ち行列から取り出されたときに $c[T]$ が $1$ から $0$ になって、$T$ は根拠のある命題に数えられる。しかし $T$ の証明が実際に使っている事実（例の中の主張）には証明がない。検査は、定義した性質（基礎から参照をたどって届く）については正しく判定しているが、基礎の取り方が広いために、欲しい性質（証明の連鎖が公理まで届く）からずれている。対処は 2 通りある。基礎から例を外す（例を参照する証明はすべて根拠なしになるので、書き手は事実を補題として切り出すことになる）か、基礎は広いままにして、「定理類の証明が例・注意・演習を参照している箇所」を別の点検で全件列挙し、人が確認するかである。題材のサイトは後者を取っている。 索引を生成する手続きが、次の形の出力を書き出すとする。1 行目は生成の日時、2 行目以降は「鍵と番号」の行で、行の順序は内部の辞書の走査順（実行ごとに変わりうる）である。 1. この出力をそのまま期待出力と比べる黄金テストは、なぜ不安定になるか。 の言葉で説明せよ。 2. 「1 行目を取り除き、残りの行を整列する」という正規化 $\nu$ を挟んだ。このテストが検出できない誤りの例を 1 つ挙げよ。 3. 正規化を使わずにテストを安定させるには、生成の手続きをどう直せばよいか。 1. 同じ入力でも、日時は実行のたびに違い、行の順序も変わりうる。出力は 2 つ以上の値を正の確率でとるので、(b) より、どんな期待出力を保存しても合格の確率は $1$ より小さい。日時が秒の単位で入っていれば、合格の確率は事実上 $0$ である。 2. $\nu$ は行の順序の違いと 1 行目の違いを同一視する。たとえば、生成の手続きに「日時の欄に 1970 年 1 月 1 日を書いてしまう」不具合が入っても、1 行目は取り除かれるので検出されない。また、仕様が「鍵の辞書順に出力する」に変わったのに実装が従っていなくても、整列してから比べるので検出されない。(c) のとおり、検出されるのは $\nu$ の値が変わる誤りだけである。 3. 日時を手続きの中で取得せず、引数（入力）として受け取るようにし、テストでは固定した値を渡す。行は、書き出す前に鍵で整列する。こうすると出力は入力の関数になり（）、正規化なしの黄金テストが決定的になる（(a)）。同時に、出力の内容ハッシュが入力だけで決まるので、ビルドの早期打ち切りとキャッシュも効くようになる。 ## 参考文献 - A. Tarski, "A lattice-theoretical fixpoint theorem and its applications", *Pacific Journal of Mathematics* 5(2) (1955), 285–309 — 単調な写像の最小不動点の存在。 の背景です。 - B. A. Davey, H. A. Priestley, *Introduction to Lattices and Order*, 2nd ed., Cambridge University Press, 2002 — 束と不動点定理の入門。有限の場合の反復による計算も扱われています。 - W. F. Dowling, J. H. Gallier, "Linear-time algorithms for testing the satisfiability of propositional Horn formulae", *The Journal of Logic Programming* 1(3) (1984), 267–284 — と同じ構造の、計数と待ち行列による線形時間の算法。 - H. G. Rice, "Classes of recursively enumerable sets and their decision problems", *Transactions of the American Mathematical Society* 74 (1953), 358–366 — プログラムの意味的な性質の判定不能性。 (b) の背景です。 - The Stacks Project Authors, *The Stacks Project*, [https://stacks.math.columbia.edu/](https://stacks.math.columbia.edu/) — 定理ごとに変わらない識別子（タグ）を割り当て、番号の変動から参照を守っている大規模な数学の文書の実例。 - The mathlib Community, "The Lean mathematical library", *Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020)* — 証明そのものを機械に検査させる方式の実例。 で触れた対比の相手です。