構成的解析に基づく区間演算検証系の存在定理

概要. 本稿では、ADIC (Analytically Derived Interval Computation) システムの数学的基礎を確立する。具体的には、ある自然なクラスの実数値計算プログラムに対し、その解析的性質（不等式仕様の充足）が、一階算術（PRA 等）における $\Sigma_1$ 述語の真偽と論理的に同値になることを証明する。これは、連続的な実数計算の正当性検証を、有限かつ離散的な証明書（レジャー）の存在問題へ還元するものである。

1. 序論

実数値計算の正当性保証は、計算可能解析 (computable analysis) における中心的な課題である。本稿は、Weihrauch らの Type-2 理論や Bishop–Bridges の構成的解析を基礎とし、実数計算の検証プロセスを形式算術における $\Sigma_1$ 文「ある有限の証拠が存在し、それを原始再帰的に検証できる」という形式へ還元する。

定理 1.1 (主定理)

基本関数族 $\mathcal{O}$ が標準的な計算可能解析の仮定（定義 2.1）を満たすとする。このとき、$\mathcal{O}$ 上のプログラム $P$、停止入力 $x$、および解析的仕様 $M(P,x)$ に対し、以下の同値性が一階算術（PRA あるいは PA）の枠内で成立する。 $$ M(P,x) \iff \exists L \in \N \;.\; \Verify(P,x,L) = 1 $$ ここで $M(P,x)$ は出力値 $v_{\mathrm{out}}$ に関する固定された解析的仕様であり、 $\Verify$ はその仕様を判定する原始再帰的述語である。

1.1 関連研究と位置付け

本稿の構成は、以下の標準的な理論枠組みと整合し、それらを計算機実装可能な形式へと精密化したものである。

本稿の「ADIC の存在定理」は、これらの標準定理を実行可能な $\Sigma_1$ 形式に rephrase したものと見なせる。また、Rigorous Numerics (精度保証付き数値計算) の分野では [8, 9, 10] に見られるように、数値計算ログそのものを存在証明に用いる実践が確立しており、 ADIC はそれらを形式体系上の有限台帳として統一的に位置付ける最小単位の存在定理である。

2. 予備知識と定義

定義 2.1 (基本関数族)

$\mathcal{O} = \{ \op_j : \R^{k_j} \to \R \}_{j\in J}$ を基本関数族とする。各 $\op_j$ は定義域 $D_j \subseteq \R^{k_j}$ を持ち、以下を満たすものとする（Weihrauch [1] の標準定義と同値）。

$D_j$ 上で定義され、任意の有界部分集合上で連続。
有効な modulus of continuity $\omega$ を持つ（必要な入力精度が計算可能）。
有界領域上での値域の上界・下界が有効に計算可能。

基本関数 $\op_j$ の定義域 $D_j$ は半代数集合として記述され、 $X_1\times\cdots\times X_{k_j}\subset D_j$ の判定は PRA 内で原始再帰的に行われるものとする。

定義 2.2 ($\mathcal{O}$-プログラム)

$\mathcal{O}$-プログラムとは、有理定数・入力を葉とし、$\mathcal{O}$ の元を内部節とする計算木（または DAG）である。ループを含む一般のプログラムについては、停止入力 $x$ に対する実行トレースを展開して得られる有限の木 $\T_{P,x}$ をその実体とみなす。この木の意味論 $\denote{P}(x)$ は、各ノードに $\op_j$ を適用した合成関数の値として定義される。
木 $\T_{P,x}$ は有限列として符号化でき、その走査は原始再帰関数として定義可能である。

3. 区間拡張の構成

証明 (1) 四則演算: $I_+([a,b],[c,d]) := [a+c, b+d]$ 等の標準的な区間演算を用いればよい。除算は分母区間が $0$ を含まない場合に制限する。

(2) 代表例 $\log$: 区間 $[a,b] \subset (0,\infty)$ 上の $\log$ を考える。有効な modulus $\omega$ により、誤差 $\varepsilon$ に対する分割幅 $\delta$ を決定する。 $[a,b]$ を幅 $\delta$ 以下の小区間に分割し、各小区間の代表点 $c_i$ における近似値 $q_i$ をテイラー展開等で計算する。このとき、値域全体は $\bigcup [q_i - \varepsilon, q_i + \varepsilon]$ に含まれるため、その最小値・最大値をとることで包含区間 $[L^-, L^+]$ を構成できる。この手続きは有限回の有理演算と大小比較に還元される。

(3) 一般の $\op_j$: 定義 2.1 の仮定（一様連続性と値域評価可能性）より、上記 $\log$ と同様の区分近似手法が適用可能である。 $\square$

4. 検証の算術化と主定理の証明

定義 4.1 (レジャーと $\Verify$)

レジャー $L$ とは、計算木 $\T_{P,x}$ の各ノード $n$ に区間 $X_n$ を割り当てた有限列である。述語 $\Verify(P,x,L)$ は以下を検査する原始再帰的関数である：

$L$ が計算木 $\T_{P,x}$ と同型であること。
各ノードで局所健全性 $\op(X_{child}) \subseteq X_{parent}$ が満たされること。
出力区間 $X_{\mathrm{out}}$ が仕様 $M(P,x)$ を満たすこと。

例 4.3 ($\log$ の有界誤差近似)

仕様 $M$ の具体例として、「$\log(q)$ を誤差 $\varepsilon$ 以内で近似せよ」という命題 $$ M_{\log}(P, (q,\varepsilon)) \iff |\denote{P}(q,\varepsilon) - \log(q)| \le \varepsilon $$ を考える。ADIC においてこれは、出力区間 $X_{\mathrm{out}}$ が $[\log(q)-\varepsilon, \log(q)+\varepsilon]$ に包含されることを以て検証される。

証明 (健全性 $\Leftarrow$): $\Verify=1$ とする。定義 4.1 より全てのステップで局所健全性が保たれている。木構造に関する帰納法により、根ノードの真値 $v_{\mathrm{out}}$ は区間 $X_{\mathrm{out}}$ に含まれる（グローバル健全性）。 $\Verify$ は $X_{\mathrm{out}}$ が仕様を満たすことを確認済みであるため、真値 $v_{\mathrm{out}}$ も仕様を満たす。

(実現可能性 $\Rightarrow$): $M(P,x)$ が真であるとする。補題 3.2 の区間拡張を用い、計算木の葉から根へ区間を伝播させる手続き $\Ledger$ を構成する。構成的解析の原理より、計算精度（分割幅など）を高めることで、出力区間 $X_{\mathrm{out}}$ の幅は任意に小さくできる。 $M(P,x)$ が真であるため、十分な精度をとれば $X_{\mathrm{out}}$ は仕様の許容範囲内に収まる。このとき生成される $L$ は $\Verify=1$ を満たす。 $\square$

5. 結論

以上の議論により、ADIC の数学的実在性が証明された。解析的な実数計算の正当性は、一階算術上で記述可能な有限の証明書（レジャー）の存在問題と等価である。これにより、$\zeta$ 関数の零点計算等の高度な数学的対象に対しても、厳密な計算機証明を与える理論的基盤が確立された。

付録 A. $\log$ の区間拡張の素朴な構成

証明誤差 $\varepsilon>0$ を固定し、$\delta = \omega(\varepsilon/2)$ を求める。区間 $[a,b]$ を幅 $\le \delta$ の $N$ 個の等分点 $u_i$ で分割する。各小区間の代表点 $c_i$ での近似値 $q(c_i)$ を十分な精度（誤差 $\le \varepsilon/4$）で計算する。
modulus の性質より、任意の $x \in [u_{i-1}, u_i]$ に対し $|\log x - \log c_i| < \varepsilon/2$。三角不等式より $|\log x - q(c_i)| < \varepsilon$ となり、 $\log x \in [q(c_i)-\varepsilon, q(c_i)+\varepsilon]$。よって、全体の包含区間は $$ L^- := \min_i (q(c_i)-\varepsilon), \quad L^+ := \max_i (q(c_i)+\varepsilon) $$ とすればよい。これらは全て有限回の有理演算で完結するため、原始再帰的である。 $\square$

理論の実証 (Implementation)

本稿で証明された ADIC の理論に基づく、インタラクティブな計算デモを公開しています。
$\pi(x)$ の明示公式に対する区間演算の挙動を実際に確認できます。

ADIC 計算デモを起動する

参考文献

Core References: Computable Analysis & Exact Real Computation

[1] K. Weihrauch, Computable Analysis, Springer, 2000.
[2] E. Bishop and D. Bridges, Constructive Analysis, Springer, 1985.
[3] V. Brattka, P. Hertling, K. Weihrauch (eds.), Handbook of Computability and Complexity in Analysis, Springer, 2021.
[4] D. Bridges et al. (eds.), Handbook of Constructive Mathematics, Cambridge Univ. Press, 2023.
[5] M. Konečný, S. Park, H. Thies, "Extracting efficient exact real number computation from proofs in constructive type theory", J. Logic Comput. (2024).
[6] S. Park et al., "Semantics, Specification Logic, and Hoare Logic of Exact Real Computation", LMCS 20(2), 2024.
[7] F. Steinberg and H. Thies, "Computable analysis, exact real arithmetic and analytic functions in Coq", Coq Workshop 2019.

Applied Verification & Rigorous Numerics

[8] S. M. Rump, "Verification methods: Rigorous results using floating-point arithmetic", Acta Numerica 19, 2010.
[9] A. Matsue, A. Takayasu, "Rigorous numerics of blow-up solutions for ODEs with exponential nonlinearity", J. Comput. Appl. Math. 372, 2020.
[10] K. Ozaki et al., "Verified numerical computations for large-scale linear systems in double precision", Appl. Math. 66(2), 2021.

Constructive Logic & Proof Relevance

[11] H. Diener, H. Ishihara, "Bishop-Style Constructive Reverse Mathematics", in Handbook of Computability and Complexity in Analysis [3].
[12] A. Petrakis, "Proof-relevance in Bishop-style constructive mathematics", Ann. Pure Appl. Logic 173(1), 2022.