有限機器與無限實數之間：浮點數、精確實數與跨域算子的完成—投影雙向語義

摘要

$0.999\ldots=1$ 常被視為初等實分析的習題；但若目標是建立可用於程式語言、數值計算、精確實數、符號系統與一般算子本體論的跨域框架，它其實是一個最小但完整的壓力測試。此案例迫使我們同時處理：有限字串、有限小數前綴、有向近似鏈、無限數位流、實數的完成、不同表示的商同一、有限機器浮點格式、捨入誤差、區間包絡、特殊值與物理執行。任何框架若不能區分這些載體與箭頭，便無法嚴格說明「一個算子如何跨域轉換」，只能以自然語言把生成、極限、投影、商化與狀態變化混為一談。

本文建立「跨域橋接算子」的型別化語義。其最低資料為：

\mathfrak B = (X,Y,\llbracket-\rrbracket_X,\llbracket-\rrbracket_Y, B,\overline B,\kappa,\varepsilon,\mathsf{Exc},\mathsf{Exec}),

其中 $X,Y$ 是原始載體， $\llbracket-\rrbracket_X,\llbracket-\rrbracket_Y$ 是各自的語義映射， $B$ 是原始跨域算子， $\overline B$ 是語義層對應， $\kappa$ 指定橋接類型， $\varepsilon$ 是誤差或包絡證書， $\mathsf{Exc}$ 處理例外值，而 $\mathsf{Exec}$ 區分抽象語義與機器執行。本文區分七類橋接：精確重編碼、餘遞歸展開、完成提升、商同一化、捨入投影、區間包絡與例外逃逸。

核心結果是：由有限全 $9$ 前綴到 $1$ 的正確箭頭不是單一狀態更新：

x_n\longmapsto1,

而是作用於整條有向鏈的完成：

\mathsf{Comp}: \operatorname{Dir}_\uparrow(\mathbb Q\cap[0,1]) \longrightarrow \mathbb R,

\mathsf{Comp}\bigl((1-10^{-n})_{n\in\mathbb N}\bigr) =1.

另一方面，全 $9$ 流與 $1.000\ldots$ 的關係是表示求值與商化：

\operatorname{Val}(0,9^\omega) = \operatorname{Val}(1,0^\omega) =1,

[(0,9^\omega)] = [(1,0^\omega)].

兩者皆不是「在實數域內多執行一步」。

本文進一步分析 IEEE 754 式浮點系統。有限浮點值可經解碼嵌入有理數再嵌入實數；反向的實數到浮點轉換則是依格式與捨入模式決定的多對一投影。 $+\!0$ 與 $-\!0$ 、 $\mathrm{NaN}$ 、 $\pm\infty$ 說明浮點格式既不等於 $\mathbb R$ ，也不能只以單一數值等號處理。本文以精確實數的 Cauchy name／近似 oracle 與區間語義補足兩個方向：前者以有限程序表示可任意精化的實數語義，後者以保守包絡保存可驗證誤差。

本文的結論是，算子本體論若要成為通用而非修辭性的框架，必須內建「完成—投影雙向語義」：從有限近似或有限規格到精確／無限語義的提升，與從精確語義到有限機器表示的投影，兩者皆須標註資訊方向、同一性準則、誤差界、例外域與可組合性。它不取代領域論、範疇論、型別論、數值分析或浮點標準；它的任務是把這些理論提供的局部保證編織成可檢驗的跨域接口。

關鍵詞： 算子本體論、跨域算子、浮點數、IEEE 754、精確實數、區間算術、完成、投影、捨入、商型別、數位流、操作語義、指稱語義、誤差證書

一、問題的真正形式：不是一個等式，而是一個轉換協議

1.1 為何上一輪總論仍不夠

《生成、展開、完成與同一化：從十進位邊界到算子本體論》已經分開四個結構：

\text{生成} \longrightarrow \text{展開} \longrightarrow \text{完成} \longrightarrow \text{同一化}.

它回答了標準實數中：

0.999\ldots=1

為何沒有證明缺口，也回答了有限前綴、無限流、極限與商類為何不是同型對象。

但若算子本體論要進入計算機語言與一般跨域操作，還有一個更嚴格的問題：

當一個算子從一種載體移到另一種載體時，究竟改變了什麼？它保存什麼？失去什麼？何時是精確等值，何時只是近似，何時根本離開了實數域？

這不是上一輪的附註，而是通用性的關卡。

1.2 不能再寫「 $0.999\ldots$ 變成 $1$ 」

若沒有額外型別，句子：

0.999\ldots\longrightarrow1

至少可能指六件不同的事：

有限前綴值鏈收斂於 $1$ ；
一條無限流經求值映射指稱 $1$ ；
Cauchy 序列的等價類在完成中代表 $1$ ；
兩個十進位表示在商後同一；
某個有限十進位字面值被編譯器捨入成浮點數 $1$ ；
一個物理機器的暫存器內容在時間中變為另一個位元模式。

這六者的來源、目標、正確性條件和可逆性都不同。

1.3 本文的中心主張

本文的中心主張是：

$0.999\ldots=1$ 不是單純的實分析邊角案例；它是任何通用算子框架是否能區分「狀態算子、軌跡算子、完成算子、表示算子、捨入算子與執行算子」的最小跨域測試。

若一個框架只允許：

T:X\to X,

它只能描述同一載體內的狀態轉移。它無法直接表達：

\mathsf{Comp}:\operatorname{Chain}(X)\to\widehat X,

也無法表達：

\operatorname{round}:\mathbb R\to\mathsf{Float},

或：

Q:\mathsf{Rep}\to\mathsf{Rep}/{\sim}.

因此，它尚未具有跨域語義。

1.4 本文的邊界

本文不主張：

所有跨域轉換都可由同一個函子統一；
所有投影都是相變；
所有有限程式都能精確表示任意實數；
所有浮點運算都可安全替代實數運算；
$0.999\ldots=1$ 單獨證明「萬物皆計算」；
抽象完成自動對應物理過程的完成。

本文主張的是一個較強但可檢查的接口要求：每個跨域算子都必須攜帶自己的型別、語義相干、誤差或包含關係、例外處理與執行條件。

二、七個載體：同一個符號實際跨過哪些域

2.1 有限十進位字

令：

D=\{0,1,\ldots,9\}.

有限字空間為：

\mathsf{FinStr}_{10}=D^\ast.

一個元素 $p\in D^\ast$ 是有限符號物件。它可以被儲存、傳輸、比較字串相等，也可以作為程式輸入。

例如：

9,\qquad99,\qquad999

都是不同的有限字。

2.2 有限前綴的有理值

對長度為 $n$ 的字：

p=d_1d_2\ldots d_n\in D^n,

定義有限求值：

v_n(p) = \sum_{k=1}^{n}d_k10^{-k} \in \mathbb Q.

對全 $9$ 前綴：

p_n=9^n,

有：

v_n(p_n) = 1-10^{-n}.

它是一個有理數，不是尚未完成的實數，也不是浮點數位元模式。

2.3 無限數位流

無限流空間為：

\mathsf{Stream}_{10}=D^{\mathbb N}.

元素：

s=(d_1,d_2,d_3,\ldots)

是一個餘歸納對象。全 $9$ 流記作：

9^\omega=(9,9,9,\ldots).

它不是任何有限字的最後一項：

9^\omega\notin D^\ast.

2.4 完整十進位表示

為了處理整數部分，令：

\mathsf{Rep}_{10} = \mathbb Z\times D^{\mathbb N}.

兩個特別的表示為：

r_9=(0,9^\omega), \qquad r_0=(1,0^\omega).

原始表示上：

r_9\neq r_0.

2.5 精確實數語義

本文以：

\mathbb R

表示標準實數語義域。它不是具體程式語言的一個原生固定大小型別。

有限前綴鏈可以在實數域中取得極限：

\lim_{n\to\infty}(1-10^{-n})=1.

無限流則可以經求值：

\operatorname{Val}(k,s) = k+\sum_{j=1}^\infty s_j10^{-j}.

得到：

\operatorname{Val}(r_9) = \operatorname{Val}(r_0) =1.

2.6 有限浮點格式

令：

\mathsf{Float}_{b,p,E}

表示一個基數 $b$ 、有效位數 $p$ 、有限指數範圍 $E$ 的浮點格式。若使用 IEEE 754 類格式， $b$ 可以是 $2$ 或 $10$ 。

它不應直接被識別為：

\mathbb R.

應至少分解為：

\mathsf{Float} = \mathsf{Float}_{\mathrm{finite}} \sqcup \{+\infty,-\infty\} \sqcup \mathsf{NaN}.

其中：

有限二進位浮點數可精確解碼為 dyadic rational；
$+\infty$ 與 $-\infty$ 屬於擴張語義，不是有限實數；
$\mathsf{NaN}$ 不是實數值；
$+\!0$ 與 $-\!0$ 提醒我們原始位元表示與數值等值不是同一關係。

2.7 區間與保守近似

令：

\mathsf{Int}(\mathbb R) = \{[a,b]\mid a,b\in\mathbb R,\;a\le b\}.

一個區間不是單一近似數值，而是對未知精確值的保守包絡：

x\in[a,b].

它在跨域語義中非常重要，因為它把「近似」改寫成可驗證的包含關係，而非未標記的數值猜測。

2.8 七域總表

載體	典型元素	可直接表達	不能自動表達
$\mathsf{FinStr}_{10}$	$999$	有限符號	無限流或實數值
$\mathbb Q$	$0.999$	有限精確有理值	極限完成
$\mathsf{Stream}_{10}$	$9^\omega$	無限行為規格	機器已物理展開
$\mathsf{Rep}_{10}$	$(0,9^\omega)$	表示與進位歷史	原始表示相等
$\mathbb R$	$1$	完整數值語義	有限儲存形式
$\mathsf{Float}$	binary64 位元模式	有限機器運算	任意實數精確性
$\mathsf{Int}(\mathbb R)$	$[0.99,1]$	可驗證包絡	唯一精確值

最後一行不是多餘的第七域；它提醒我們，跨域橋接不只分為「精確」和「錯誤」兩種，還有保守近似這一種第三語義。

三、跨域不是一種箭頭：七類橋接算子

3.1 精確重編碼

精確重編碼是來源與目標保留同一語義的表示變換：

E:X\to Y,

若存在語義映射使：

\llbracket E(x)\rrbracket_Y = \llbracket x\rrbracket_X,

則稱 $E$ 為精確重編碼。

例如，把一個有限十進位字解析為其精確有理值：

\operatorname{parse}_{\mathbb Q}:D^n\to\mathbb Q.

3.2 餘遞歸展開

餘遞歸展開從有限規格取得整體無限行為：

\mathsf{Unf}:\mathsf{Spec}\to\mathsf{Stream}_{10}.

若 $\mathsf{nine}$ 是「輸出 $9$ 後回到自身」的有限狀態規格，則：

\mathsf{Unf}(\mathsf{nine})=9^\omega.

這是無限行為的規定，不是將所有位數寫入有限記憶體。

3.3 完成提升

完成提升的輸入不是單點，而是圖表、鏈或近似系統：

\mathsf{Comp}:\operatorname{Diag}(\mathcal C)\to\widehat{\mathcal C}.

對本例：

\mathsf{Comp}\bigl((1-10^{-n})_n\bigr)=1.

這不是：

1-10^{-n}\mapsto1

的逐項函數。

3.4 商同一化

給定等價關係 $\sim$ ：

Q:X\to X/{\sim},

把原始不同但語義等價的表示辨識為同一商類。

十進位案例：

Q(0,9^\omega) = Q(1,0^\omega).

3.5 捨入投影

捨入是從精確或高精度語義到有限格式的投影：

\operatorname{round}_{F,\rho}:\mathbb R\to\mathsf{Float}_{F},

其中 $\rho$ 是捨入模式。

通常：

\operatorname{round}_{F,\rho}(x) = \operatorname{round}_{F,\rho}(y)

並不推出：

x=y.

所以這不是精確重編碼。

3.6 區間包絡

區間包絡把精確值映射到含有它的可驗證區間：

\operatorname{enc}_\delta:\mathbb R\to\mathsf{Int}(\mathbb R),

x\longmapsto[a,b], \qquad x\in[a,b], \qquad b-a\le\delta.

它不選擇唯一近似點，而保存可證包含。

3.7 例外逃逸

某些機器運算不再落於原預期數值域。例如除以零、溢位或無效操作可能產生：

\mathsf{NaN}, \qquad \pm\infty.

這應表達為：

T:\mathsf{Float}\to\mathsf{Float},

而非誤寫成：

T:\mathbb R\to\mathbb R.

例外值不是誤差條的一個普通端點；它們可能使相等、排序與後續算子規則改變。

四、完成與投影：兩個方向相反的跨域運動

4.1 有限近似到精確語義

第一個方向是：

\text{有限前綴／有限規格} \longrightarrow \text{無限或精確語義}.

在全 $9$ 案例：

(9,99,999,\ldots) \longrightarrow (0.9,0.99,0.999,\ldots) \xrightarrow{\mathsf{Comp}} 1.

此方向通常增加語義完成度；它不能被理解為一個一般可逆的有限計算。

4.2 精確語義到有限機器表示

第二個方向是：

\text{精確實數語義} \longrightarrow \text{有限機器表示}.

例如：

\operatorname{round}_{\mathrm{binary64},\rho}(x).

這通常減少資訊，並依格式、捨入模式與範圍限制決定結果。

4.3 兩個箭頭不是互逆

最危險的錯誤是把完成與捨入畫成同一條可逆箭頭：

\mathbb R \rightleftarrows \mathsf{Float}.

事實上，有限浮點解碼可以是精確嵌入：

\operatorname{decode}_F: \mathsf{Float}_{\mathrm{finite}}/\!\sim_{\mathrm{value}} \hookrightarrow \mathbb Q_b \hookrightarrow \mathbb R,

但反向的 $\operatorname{round}_{F,\rho}$ 通常多對一。

其中 $\sim_{\mathrm{value}}$ 至少可處理：

+0\sim_{\mathrm{value}}-0

在純數值相等下的辨識，也可依格式處理其他同值原始編碼；若語義任務保留符號方向或原始格式資訊，則不應過早作此商。

4.4 「有限中的無限」與「無限中的有限」

這兩個常被混淆的短語應分開。

有限中的無限：一個有限程式、餘遞歸規格或 Cauchy name 可以有限地描述可任意展開或任意精化的無限語義。

無限中的有限：一個浮點值或有限區間是無限實數域中的有限資訊切片、近似或包絡。

前者是規格或名稱的有限性；後者是表示精度的有限性。它們不是彼此的反面，更不是同一種「無限壓縮」。

五、 $0.999\ldots$ 的四條精確路徑

5.1 有限字到有理值

對：

p_n=9^n,

有精確解析：

v_n(p_n) = 1-10^{-n}.

這一箭頭是：

D^n\to\mathbb Q.

每個輸出都嚴格小於 $1$ 。

5.2 有理鏈到實數完成

令：

\gamma_9:\mathbb N\to\mathbb Q\cap[0,1],

\gamma_9(n)=1-10^{-n}.

則：

\mathsf{Comp}_{\sup}(\gamma_9) = \sup_n\gamma_9(n) =1.

這是：

\operatorname{Dir}_\uparrow(\mathbb Q\cap[0,1]) \to \mathbb R

的箭頭。

5.3 有限規格到無限流再到實數

令 $\mathsf{nine}$ 為全 $9$ 餘遞歸規格：

\mathsf{Unf}(\mathsf{nine}) = 9^\omega.

再以：

\operatorname{Val}:D^{\mathbb N}\to[0,1]

求值：

\operatorname{Val}(9^\omega) = \sum_{k=1}^{\infty}9\cdot10^{-k} =1.

5.4 表示商到同一實數

在完整表示域中：

(0,9^\omega) \neq (1,0^\omega).

但：

\operatorname{Val}(0,9^\omega) = \operatorname{Val}(1,0^\omega).

因此在求值核商中：

[(0,9^\omega)] = [(1,0^\omega)].

5.5 四路相干條件

真正需要的不是把四條路徑混為一條，而是證明它們相干：

\operatorname{Val}(9^\omega) = \mathsf{Comp}_{\sup}(\gamma_9) = \lim_n v_n(p_n) = 1.

這是跨域橋接的最小可交換圖。若一個算子本體論無法寫出並檢查這張圖，它便無法安全宣稱「有限的東西跨入了無限／完成域」。

六、精確實數不是無限記憶體中的小數

6.1 Cauchy name

一種常見的精確實數表示不是儲存全部小數，而是給出可任意要求精度的近似器：

N:\mathbb N\to\mathbb Q,

滿足對某個實數 $x$ ：

|N(k)-x| \le 2^{-k}.

$N$ 稱為 $x$ 的 Cauchy name 或 approximation oracle。

6.2 程式有限，語義可任意精化

一段有限程式可以計算：

k\longmapsto N(k),

而不需一次存放 $x$ 的全部數位。這正是「有限規格承載無限語義」的可計算版本。

但必須避免超譯：

\text{有限程式存在} \not\Rightarrow \text{所有實數都可由它表示}.

可計算實數在 $\mathbb R$ 中只是特殊子集。

6.3 相等判定的非對稱

若有兩個精確實數名稱 $N_x,N_y$ ，且：

x\neq y,

那麼一旦精度足夠高，可能找到有限證據分離兩者。

但對任意可計算實數名稱，一般不能期待一個總會終止的程序判定：

x=y.

因此「能任意逼近」不等於「能以固定有限資源判定所有相等」。這與十進位雙重表示的問題相呼應：語義上的等號與有限觀察的可判定性不是同一件事。

6.4 精確實數算子的正確型別

精確實數函數通常不應被理解為：

f:\mathbb R\to\mathbb R

在機器內直接操縱不可見的完整實數，而應實作為名稱變換：

\widehat f: \mathsf{Name}(\mathbb R) \to \mathsf{Name}(\mathbb R),

並滿足：

\llbracket\widehat f(N_x)\rrbracket = f(\llbracket N_x\rrbracket).

這正是跨域橋接的相干要求。

七、浮點數不是失敗的實數，而是另一種操作域

7.1 有限浮點的精確解碼

對一個有限二進位浮點值 $f$ ，可定義：

\operatorname{decode}_2(f)\in\mathbb Q_2,

其中：

\mathbb Q_2 = \left\{\frac{m}{2^n}\middle|m\in\mathbb Z,\;n\in\mathbb N\right\}.

因此，有限浮點值本身通常不是「近似而無法說清的數」，而是一個完全精確的 dyadic rational；近似發生在它相對於目標實數時。

7.2 二進位 $0.1$ 的典型分離

十進位有理數：

\frac1{10}

不是 dyadic rational。因此，在有限二進位浮點格式中通常無法被精確表示。某個 binary64 值可以很接近 $1/10$ ，卻仍是另一個精確有理數。

這不是硬體壞掉，而是：

\mathbb Q_2 \subsetneq \mathbb Q.

7.3 有限 $9$ 字面值被捨入成 $1$ 的陷阱

在某一格式與捨入模式下，足夠接近 $1$ 的有限十進位字面值可能被解析或捨入為浮點數 $1$ 。這個現象不是：

0.\underbrace{99\ldots9}_{n\text{ 位}} =1

在精確實數中突然成立；它是：

\operatorname{round}_{F,\rho}(1-10^{-n}) = \operatorname{round}_{F,\rho}(1)

在有限格式中成立。

兩種等號不能互換。

7.4 $+\!0$ 與 $-\!0$

IEEE 754 類格式可保留兩個零的原始表示：

+0, \qquad -0.

在通常數值比較中它們相等；但符號複製、某些倒數、分支或 total order 任務可能保留差異。

這提供一個很小但直接的教訓：

是否商化 $+\!0$ 與 $-\!0$ ，取決於指定觀察與任務；不能由「它們都代表零」推出所有算子都應忽略符號。

7.5 $\mathsf{NaN}$ 與無限大

浮點域含有不應直接塞回 $\mathbb R$ 的資料：

\mathsf{NaN}, \qquad \pm\infty.

尤其 $\mathsf{NaN}$ 的比較與傳播規則顯示，單一「數值相等」不是所有操作的共同底層。若模型需要處理機器實作，例外域必須成為明示的和型別，而不是註腳。

八、區間語義：把誤差改寫為包含關係

8.1 點近似的不足

若寫：

\widetilde x\approx x,

卻未指定誤差度量、上界或方向， $\approx$ 幾乎沒有可計算內容。

8.2 區間 concretization

對區間：

I=[a,b],

定義其 concretization：

\gamma(I) = \{x\in\mathbb R\mid a\le x\le b\}.

若計算結果 $I'$ 滿足目標語義：

y\in\gamma(I'),

則它是保守正確的，即使 $I'$ 不退化成單點。

8.3 有向捨入與可驗證包絡

以向下與向上捨入計算端點，可構造包住精確結果的區間。例如對 $x,y$ ：

\operatorname{round}_{\downarrow}(x+y) \le x+y \le \operatorname{round}_{\uparrow}(x+y).

這把浮點捨入由「不可靠誤差」轉化為「可證包絡」。

8.4 抽象解釋形式

若 $\mathcal A$ 是抽象域，則可使用：

\alpha:\mathcal P(\mathbb R)\to\mathcal A,

\gamma:\mathcal A\to\mathcal P(\mathbb R),

並要求：

\alpha(S)\sqsubseteq a \iff S\subseteq\gamma(a).

這提供有限抽象狀態與無限語義集合之間的嚴格橋梁。

8.5 區間不是實數的低級替代

區間保留的是不同資訊：

[a,b]

表達「值尚未精確定位，但保證位於此範圍」。在不確定性、錯誤控制與物理量測中，它常比一個未附誤差的浮點點值更強。

九、跨域橋接算子的正式規格

9.1 為何普通函數簽名不夠

一個普通函數簽名：

B:X\to Y

只能保證輸入輸出型別相符。它沒有告訴我們：

$X$ 與 $Y$ 中的元素各自代表什麼；
$B$ 是否保留語義；
$B$ 是否捨入、遺失資訊或加入不確定性；
$B$ 是否只對某些輸入定義；
例外值是否仍屬原語義域；
多個橋接是否可安全複合。

因此，跨域算子必須比裸函數攜帶更多資料。

9.2 橋接規格

定義一個跨域橋接規格：

\mathfrak B = (X,Y,S_X,S_Y, \llbracket-\rrbracket_X,\llbracket-\rrbracket_Y, B,\overline B,\kappa,\mathcal C,\varepsilon,\mathsf{Exc},\mathsf{Exec}),

其中：

$X,Y$ 是原始載體；
$S_X,S_Y$ 是各自的語義域；
$\llbracket-\rrbracket_X:X\rightharpoonup S_X$ 與 $\llbracket-\rrbracket_Y:Y\rightharpoonup S_Y$ 是可能部分定義的語義映射；
$B:X\rightharpoonup Y$ 是原始層橋接；
$\overline B:S_X\rightharpoonup S_Y$ 是語義層對應；
$\kappa$ 是橋接種類；
$\mathcal C$ 是正確性證書；
$\varepsilon$ 是誤差、精度或包含資料；
$\mathsf{Exc}$ 是例外值與例外傳播資料；
$\mathsf{Exec}$ 是執行語義及資源條件。

本文允許部分函數，因為解析失敗、除以零、超出格式範圍與不終止計算都不能誠實地偽裝成全函數。

9.3 六種正確性證書

跨域算子至少可能具有下列六種證書。

證書	形式	含義
精確相干	$\llbracket Bx\rrbracket_Y=\overline B(\llbracket x\rrbracket_X)$	語義嚴格保留
商相干	$Q_YB=\overline BQ_X$	原始差異在商後良定義
誤差界	$d(\llbracket Bx\rrbracket_Y,\overline B\llbracket x\rrbracket_X)\le\varepsilon(x)$	近似誤差可控
包含相干	$\overline B\llbracket x\rrbracket_X\in\gamma(Bx)$	結果保守包絡真值
精化關係	$B_{k+1}(x)\sqsubseteq B_k(x)$	精度提高、資訊增加
例外相干	$\mathsf{Exc}(x)$ 明示	離開普通語義域的原因可追溯

這六種證書不可混用。例如「數值看起來很接近」不是誤差界；「代表同一商類」也不是原始相等。

9.4 橋接種類 $\kappa$

本文採用：

\kappa\in \{ \mathsf{Encode}, \mathsf{Unfold}, \mathsf{Complete}, \mathsf{Quotient}, \mathsf{Project}, \mathsf{Enclose}, \mathsf{Escape} \}.

各類型分別是：

類型	資訊方向	典型例子
$\mathsf{Encode}$	同語義換表示	十進位字到有理數
$\mathsf{Unfold}$	有限規格到無限行為	迭代規則到 $9^\omega$
$\mathsf{Complete}$	近似圖表到完成物件	鏈到上確界
$\mathsf{Quotient}$	遺忘指定差異	雙重十進位表示
$\mathsf{Project}$	精確／高階到有限格式	實數捨入為 float
$\mathsf{Enclose}$	精確值到保守集合	實數到區間
$\mathsf{Escape}$	普通域到例外域	除零到 $\infty$ 或 $\mathsf{NaN}$

9.5 圖表輸入與狀態輸入

必須明確區分：

T:X\to X

與：

\mathsf{Comp}:\operatorname{Diag}(X)\to\widehat X.

$T$ 作用於一個狀態； $\mathsf{Comp}$ 作用於一個由多個狀態與過渡構成的圖表。

所以：

\mathsf{Comp}\bigl((x_n)_n\bigr)=L

不表示：

\exists n,\;T(x_n)=L.

這是從 $0.999\ldots$ 推出的第一條跨域型別律。

十、相干圖：跨域轉換何時真正成立

10.1 精確可交換圖

若 $B$ 是精確橋接，應有：

\begin{array}{ccc} X & \xrightarrow{\;B\;} & Y\\ \Big\downarrow{\llbracket-\rrbracket_X} & & \Big\downarrow{\llbracket-\rrbracket_Y}\\ S_X & \xrightarrow{\;\overline B\;} & S_Y \end{array}

以公式表示：

\llbracket B(x)\rrbracket_Y = \overline B(\llbracket x\rrbracket_X).

例如，有限十進位字的精確有理解析可取：

\overline{\operatorname{parse}}_{\mathbb Q} = \operatorname{id}_{\mathbb Q}.

10.2 完成圖

完成圖的來源不是 $X$ ，而是圖表範疇：

\begin{array}{ccc} \operatorname{Dir}_\uparrow(\mathbb Q\cap[0,1]) & \xrightarrow{\;\mathsf{Comp}_{\sup}\;} & \mathbb R\\ \Big\downarrow{\operatorname{pointwise\;embed}} & & \Big\downarrow{\operatorname{id}}\\ \operatorname{Dir}_\uparrow(\mathbb R) & \xrightarrow{\;\sup\;} & \mathbb R \end{array}

對全 $9$ 鏈：

\mathsf{Comp}_{\sup} \bigl((1-10^{-n})_n\bigr) =1.

10.3 近似可交換圖

對浮點捨入，要求通常應改寫為：

d\left( \operatorname{decode}_F(\operatorname{round}_{F,\rho}(x)), x \right) \le \varepsilon_{F,\rho}(x).

如果 $x$ 可表示，則：

\varepsilon_{F,\rho}(x)=0.

若不可表示，誤差界依格式、捨入模式與 $x$ 所在的 binade 而變。

10.4 包含可交換圖

對區間計算，正確性不是點等式，而是：

\overline B(\llbracket x\rrbracket_X) \in \gamma(B(x)).

對區間加法：

[a,b]\oplus[c,d] \supseteq \{u+v\mid u\in[a,b],\;v\in[c,d]\}.

若端點使用有向捨入，這個包含可成為機器可驗證保證。

10.5 商相干圖

令：

Q_X:X\to X/{\sim_X}, \qquad Q_Y:Y\to Y/{\sim_Y}.

若 $B$ 要下降為商算子 $\overline B_Q$ ，需要：

\begin{array}{ccc} X & \xrightarrow{\;B\;} & Y\\ \Big\downarrow{Q_X} & & \Big\downarrow{Q_Y}\\ X/{\sim_X} & \xrightarrow{\;\overline B_Q\;} & Y/{\sim_Y} \end{array}

亦即：

x\sim_Xx' \Rightarrow B(x)\sim_YB(x').

10.6 例外圖

若 $B$ 可能離開普通語義，應把目標寫成和型別：

B:X\to Y+\mathsf{Exc}.

而非假裝：

B:X\to Y

永遠成立。

這對浮點 $\mathsf{NaN}$ 、溢位、除零、字串解析失敗及未終止計算都重要。

十一、橋接的複合：精確、誤差與包絡如何累積

11.1 精確橋接可複合

令：

\mathfrak B_1:X\to Y, \qquad \mathfrak B_2:Y\to Z

皆具有精確相干：

\llbracket B_1x\rrbracket_Y = \overline B_1\llbracket x\rrbracket_X,

\llbracket B_2y\rrbracket_Z = \overline B_2\llbracket y\rrbracket_Y.

則：

\llbracket B_2(B_1x)\rrbracket_Z = (\overline B_2\circ\overline B_1) \llbracket x\rrbracket_X.

這是跨域算子可以形成範疇式組合的最低條件。

11.2 誤差橋接的複合

若：

d_Y( \llbracket B_1x\rrbracket_Y, \overline B_1\llbracket x\rrbracket_X ) \le \varepsilon_1(x),

且 $\overline B_2$ 在相關區域為 $L_2$-Lipschitz：

d_Z(\overline B_2(u),\overline B_2(v)) \le L_2d_Y(u,v),

再假定第二橋接誤差不超過 $\varepsilon_2$ ，則由三角不等式：

d_Z( \llbracket B_2B_1x\rrbracket_Z, \overline B_2\overline B_1\llbracket x\rrbracket_X ) \le L_2\varepsilon_1(x) + \varepsilon_2(B_1x).

這給出跨域誤差如何累積的最低公式。它也是為何「大致相近」不足以做通用算子語言：沒有誤差型別與複合律，長鏈一旦變長便失去可判定性。

11.3 包絡橋接的複合

若：

\overline B_1(x)\in\gamma_Y(B_1x),

且：

\overline B_2(y)\in\gamma_Z(B_2y)

對所有允許 $y$ 成立，則必須額外驗證 $B_2$ 對 $\gamma_Y(B_1x)$ 的全部可能值均保守。不能只把中間區間的中點送入下一步。

這是區間分析中依賴關係、過度包絡與分割策略出現的結構原因。

11.4 例外的複合

若：

B_1(x)=\mathsf{Exc},

則 $B_2(B_1x)$ 可能未定義、傳播例外或進行恢復。這必須由例外代數指定：

\mathsf{propagate}, \qquad \mathsf{handle}, \qquad \mathsf{retry}.

不應把所有例外都折疊成某個巨大數值或 $0$ 。

11.5 跨域鏈的信任預算

一條實作鏈：

\text{文字} \to \text{解析} \to \text{浮點} \to \text{區間} \to \text{決策}

只有在每一箭頭都具有明示證書時，終點的可信度才可以回溯。這可稱為跨域鏈的信任預算：

\mathsf{Trust} = \bigcap_i \mathsf{Certificate}(B_i).

任一未聲明箭頭都可能成為整條鏈的真實 GAP。

十二、程式語言中的 $0.999\ldots$ ：解析、求值與執行必須分開

12.1 省略號不是一般程式字面值

在大多數程式語言中：

\texttt{0.999...}

不是一個普通有限浮點字面值。它要麼是語法錯誤，要麼必須被解釋為某種延遲資料結構、生成器、符號表達式或自訂精確實數語法。

因此，直接問「電腦裡的 $0.999\ldots$ 等不等於 $1$ 」先缺少型別。

12.2 有限十進位字面值

一個有限字面值可先解析為精確十進位有理數：

\operatorname{parse}_{10}: \mathsf{Lit}_{10}^{\mathrm{fin}} \to \mathbb Q.

再依目標型別轉換：

\mathbb Q \xrightarrow{\operatorname{round}_{F,\rho}} \mathsf{Float}_{F}.

此時：

\texttt{0.999999}

代表某個有限有理數；它在精確語義中小於 $1$ ，即使在特定浮點格式中可能捨入為同一個機器值。

12.3 無限流字面值

若語言提供 lazy stream：

\mathsf{repeat}(9)

可作為有限程式描述：

9^\omega.

但此物件的型別應是：

\mathsf{Stream}\;D,

而非：

\mathsf{Float}.

若要取得其實數語義，需另外給：

\operatorname{evalStream}: \mathsf{Stream}\;D \to \mathsf{ExactReal}.

12.4 近似請求式求值

精確實數不必把全部數位計算完。可提供：

\operatorname{approx}: \mathsf{ExactReal} \times \mathbb N \to \mathbb Q,

使：

|\operatorname{approx}(x,k)-x| \le 2^{-k}.

這是「無限語義可以被有限請求逐步顯化」的正確工程形式。

12.5 整體語義與物理執行

一個程式中的：

\mathsf{repeat}(9)

可以在指稱語義中代表 $9^\omega$ ；但某次執行只會在有限時間輸出有限前綴：

\operatorname{trace}(t) = 9^{N(t)}.

因此：

\operatorname{evalStream}(\mathsf{repeat}(9))=1

不表示硬體在有限時間內已經列印無限個 $9$ 。

12.6 編譯器與語義模型不可互相偷換

若編譯器把一個有限小數 literal 直接轉為 binary64，這是一條：

\mathsf{Text} \to \mathsf{Float}

的捨入鏈。

若定理把 $0.999\ldots$ 定義為實數極限，這是一條：

\mathsf{Chain}(\mathbb Q) \to \mathbb R

的完成鏈。

兩者都可合法，但其正確性條件根本不同。把前者拿來證明後者，或把後者當成前者的執行描述，都會產生型別錯置。

十三、同一實數系統中的轉換，到底改變了什麼

13.1 三種「同一」

說「都在同一個實數系統下」時，至少有三種可能。

名稱	形式	十進位例子
原始相等	$p=q$	$(0,9^\omega)\neq(1,0^\omega)$
指稱相等	$\operatorname{Val}(p)=\operatorname{Val}(q)$	兩者皆為 $1$
商後相等	$[p]=[q]$	求值核商中相等

三者均可被稱為「同一」，但只有後兩者在此例成立。

13.2 在 $\mathbb R$ 中沒有數值狀態跳躍

若：

x_n=1-10^{-n},

那麼每個 $x_n$ 是 $\mathbb R$ 的元素，且：

x_n<1.

完成：

\sup_nx_n=1

不是 $x_n$ 在某個有限 $n$ 經由內部算子跳成 $1$ 。它是由整條鏈決定的新對象或新判定。

因此：

\text{完成} \neq \text{同一載體內的有限狀態更新}.

13.3 但確實存在結構改變

雖然不是一個物理跳躍，完成與商化仍可改變結構：

載體改變：

\operatorname{Dir}_\uparrow(\mathbb Q) \to \mathbb R;

資訊序改變： 有限近似鏈被其上確界完成；
同一性改變：

\mathsf{Rep}_{10} \to \mathsf{Rep}_{10}/{\sim_{\operatorname{Val}}};

拓樸結構改變： 十進位流的全不連通表示經端點黏合後可得到連通區間；
可用算子改變： 某些表示算子可下降，有些則不能。

這些可稱為表示—語義結構轉換。若要使用「相變」一詞，必須聲明它是結構層的命名，而非熱力學或物理時間中的相變。

13.4 五種狀態變化不能混寫

類型	形式	是否在同一載體內
動力狀態更新	$T:X\to X$	是
跨型別轉換	$B:X\to Y$	否
完成	$\mathsf{Comp}:\operatorname{Diag}(X)\to\widehat X$	否，且輸入是圖表
商同一化	$Q:X\to X/{\sim}$	否，改變同一性
投影／捨入	$\operatorname{round}:\mathbb R\to F$	否，通常失資訊

任何「算子導致狀態改變」的理論都必須先判斷自己在說哪一列。

13.5 相變的最低技術條件

若要稱一條轉換為某種相變，至少要給：

(X,\Lambda,T_\lambda,I,\mathcal E),

其中 $\Lambda$ 是控制參數， $I$ 是不變量或序參量， $\mathcal E$ 是相的等價準則。

單獨的：

\mathsf{Comp}(\gamma)=L

只證明完成。它不自動給出 $\lambda_c$ 、相分類或不變量跳變。

13.6 十進位案例的正確命名

因此，本例可以精確稱為：

一個由有限前綴生成、餘遞歸展開、實數完成與表示商化共同構成的跨域相干系統。

它可以成為相變、語義轉換、程序本體論與跨域算子的測試模型；但自身不是一個已證物理相變。

十四、型別論表達：讓跨域錯接在語法層失敗

14.1 最小型別族

可用抽象型別區分：

\mathsf{FinDecimal}, \quad \mathsf{DecimalStream}, \quad \mathsf{Rational}, \quad \mathsf{ExactReal}, \quad \mathsf{Float}, \quad \mathsf{Interval}.

它們不應被隱式強制轉型為同一個「Number」。

14.2 基本算子簽名

核心算子可寫成：

\operatorname{prefixEval}: \mathsf{FinDecimal} \to \mathsf{Rational},

\operatorname{unfoldNine}: \mathsf{Unit} \to \mathsf{DecimalStream},

\operatorname{streamEval}: \mathsf{DecimalStream} \to \mathsf{ExactReal},

\operatorname{complete}: \mathsf{BoundedDirectedChain}(\mathsf{Rational}) \to \mathsf{ExactReal},

\operatorname{round}_{F,\rho}: \mathsf{ExactReal} \to \mathsf{Float}_{F},

\operatorname{decode}_{F}: \mathsf{FiniteFloat}_{F} \to \mathsf{ExactReal},

\operatorname{enclose}_{k}: \mathsf{ExactReal} \to \mathsf{Interval}.

僅由簽名即可阻止三種錯誤：

\operatorname{complete}(0.999)

沒有型別，因為單一有理數不是 directed chain；

\operatorname{round}(9^\omega)

沒有型別，除非先給流的實數語義；

\operatorname{streamEval}(999)

沒有型別，除非先給有限字到流的延拓規則。

14.3 和型別處理浮點例外

不應把：

\mathsf{NaN}

塞進：

\mathsf{ExactReal}.

可使用：

\mathsf{MachineResult}(F) = \mathsf{FiniteFloat}(F) + \mathsf{PosInf} + \mathsf{NegInf} + \mathsf{NaN}.

若一個演算法要求其結果為實數，型別系統應迫使它處理：

\mathsf{NaN} \quad\text{與}\quad \pm\infty

的分支。

14.4 商型別處理表示同一

對十進位表示，設：

\mathsf{DecReal}_{10} = \mathsf{Rep}_{10}/{\sim_{\operatorname{Val}}}.

則：

\eta: \mathsf{Rep}_{10} \to \mathsf{DecReal}_{10}

把進位等價建成型別內路徑。

浮點中若任務只關心數值，也可定義：

\mathsf{FloatValue}_F = \mathsf{FiniteFloat}_F/{\sim_{\mathrm{num}}},

但這一商不應自動套用到需要保留 $+\!0/-\!0$ 或原始位元模式的任務。

14.5 依賴型誤差證書

若 $B$ 是近似橋接，輸出不應只是：

y:Y,

而應攜帶：

(y,\pi),

其中：

\pi: d(\llbracket y\rrbracket_Y,\overline B(x)) \le \varepsilon(x).

如此，誤差不再是文件末尾的口頭保證，而是算子輸出型別的一部分。

14.6 計算效應與執行層

解析失敗、例外、非終止、捨入模式讀取、硬體旗標與資源消耗都可被視為效應。抽象地：

\operatorname{run}: \mathsf{Program}\;A \to \mathsf{Effect}\;A.

它不能與純語義函數：

\llbracket-\rrbracket: \mathsf{Program}\;A \to A

不加條件地混同。

十五、完成—投影雙向語義作為算子本體論的必要層

15.1 先前框架的擴充

前一篇總論的框架為：

\mathfrak O = (\Sigma,M,\mathfrak I,\mathsf{Comp},V,\mathcal G_V,Q,\mathsf{Exec}).

為了處理有限機器與精確語義，本文加入：

\mathfrak O_{\leftrightarrow} = (\mathfrak O, \mathsf{Name}, \mathsf{Lift}, \mathsf{Project}, \mathsf{Enclose}, \mathsf{Err}, \mathsf{Exc}).

其中：

$\mathsf{Name}$ ：有限程序對精確／無限對象的名稱或規格；
$\mathsf{Lift}$ ：從近似圖表或名稱到完成語義的提升；
$\mathsf{Project}$ ：從精確語義到有限格式的投影；
$\mathsf{Enclose}$ ：保守近似的包絡；
$\mathsf{Err}$ ：誤差與精化資料；
$\mathsf{Exc}$ ：例外域。

15.2 為何這不是多加幾個模組

若沒有 $\mathsf{Lift}$ ，框架不能區分：

\text{有限前綴} \quad\text{與}\quad \text{完成實數}.

若沒有 $\mathsf{Project}$ ，框架不能區分：

\text{實數語義} \quad\text{與}\quad \text{機器格式}.

若沒有 $\mathsf{Err}$ ，框架不能判斷一條近似鏈可否安全複合。

若沒有 $\mathsf{Exc}$ ，框架會把非數值結果錯塞回數值域。

所以這不是擴張名詞，而是使跨域算子真正可操作的最低結構。

15.3 通用性不等於脫離所有數學

「算子本體論不完全依賴其他數學理論」不應理解成它可以不依賴任何證明工具。那樣只會失去可驗證性。

正確的目標是：

算子本體論提供一個通用接口語言；領域論、拓樸、範疇論、型別論、數值分析與標準規格為各種橋接提供局部存在、相干與誤差證明。

其關係可寫成：

\text{算子本體論} = \text{跨域協議層},

而非：

\text{算子本體論} = \text{取代全部數學的單一理論}.

15.4 可移植的核心，不可偷渡的結論

可移植的核心是：

型別；
算子；
語義；
相干證書；
資訊方向；
誤差或包含；
商與下降；
例外；
執行條件。

不可偷渡的結論是：

所有完成都存在；
所有投影都可逆；
所有語義等值都可有限判定；
所有浮點結果都安全；
所有跨域相似都是同構；
所有數學完成都是物理完成。

15.5 最小跨域完備性原則

本文提出以下方法論原則。

最小跨域完備性原則。 一個宣稱通用的算子框架，至少應能把「有限表示／規格、近似圖表、無限或精確語義、有限機器投影、表示商與例外域」放入不同型別，並為各橋接指定精確、誤差、包絡、商或例外證書。

$0.999\ldots$ 正好是能同時觸發全部要求的最小測試例。

十六、IEEE 754 式浮點格式作為跨域測試場

16.1 浮點格式不只是「精度較低的實數」

一個浮點格式同時規定：

可表示的有限數值集合；
原始位元編碼；
捨入模式；
算術運算；
轉換規則；
例外與旗標；
比較與排序規則。

所以：

\mathsf{Float} \neq \text{一個僅少幾位小數的 }\mathbb R.

它是一個有額外操作語義的有限機器域。IEEE 754-2019 明確規定二進位與十進位浮點格式、捨入、特殊值與運算方法，正好體現本文所說的「一個表示域需要完整操作協議」。IEEE 754-2019

16.2 有限值、零、無限與 NaN 的分型

可將浮點原始值概念化為：

\mathsf{Float} = \mathsf{Normal} \sqcup \mathsf{Subnormal} \sqcup \mathsf{SignedZero} \sqcup \mathsf{Infinity} \sqcup \mathsf{NaN}.

不同部分需要不同語義橋接：

原始類別	典型語義域	橋接狀態
normal／subnormal	$\mathbb Q_b\hookrightarrow\mathbb R$	可精確解碼
$+\!0,-\!0$	$0\in\mathbb R$ 或帶符號零語義	是否商化取決於任務
$+\infty,-\infty$	擴張實數或例外域	不屬有限 $\mathbb R$
$\mathsf{NaN}$	例外／未定義／payload 域	不應嵌入 $\mathbb R$

16.3 解碼不是反向捨入

對可解碼有限值：

\operatorname{decode}_F: \mathsf{FiniteFloat}_F \to \mathbb R

可精確給出它所代表的有理數。

反向：

\operatorname{round}_{F,\rho}: \mathbb R \to \mathsf{FiniteFloat}_F

則受限於有限格點。一般：

\operatorname{decode}_F \circ \operatorname{round}_{F,\rho} \neq \operatorname{id}_{\mathbb R}.

在可表示值的子集上才可能有：

\operatorname{decode}_F \circ \operatorname{round}_{F,\rho} = \operatorname{id}.

16.4 捨入模式是算子參數，不是背景噪音

同一個實數 $x$ 在不同 $\rho$ 下可能投影到不同浮點值：

\operatorname{round}_{F,\downarrow}(x), \qquad \operatorname{round}_{F,\uparrow}(x), \qquad \operatorname{round}_{F,\mathrm{nearest}}(x).

因此捨入不應只寫成：

\operatorname{round}_F,

而應至少寫成：

\operatorname{round}_{F,\rho}.

否則算子本體論把一個會改變結果的控制條件錯誤地隱藏了。

16.5 二進位與十進位不是誰更真

二進位與十進位格式對不同有理數有不同的精確子域：

\mathbb Q_2 \neq \mathbb Q_{10}.

其中：

\mathbb Q_{10} = \left\{\frac{m}{2^a5^b}\middle|m\in\mathbb Z,\;a,b\in\mathbb N\right\}.

十進位有限小數如 $0.1$ 在十進位格式中可精確，卻通常不在有限二進位格式中精確；反過來，分母含純 $2$ 冪的數在二進位格式中自然精確。

這是表示域結構差異，不是「一方是真數、另一方是假數」。

16.6 浮點等於與語義等於

必須分開：

f=g \quad\text{作為位元或格式值，}

\operatorname{decode}(f)=\operatorname{decode}(g) \quad\text{作為實數語義，}

f\equiv_{\mathrm{cmp}}g \quad\text{作為某個浮點比較結果。}

$+\!0$ 與 $-\!0$ 是第一、第二層不同而某些比較層相同的典型； $\mathsf{NaN}$ 則提醒我們某些比較不形成通常等價關係。

16.7 浮點測試對算子本體論的意義

浮點系統迫使框架同時回答：

原始表示是什麼？
解碼後的語義是什麼？
哪些操作是正確捨入？
哪些操作會進例外域？
哪些原始差異在何種任務下可商化？
誤差怎樣隨多步複合累積？

若框架無法回答這六點，就不能宣稱自己已可處理有限機器上的「算子跨域」。

十七、核心定理與命題

17.1 命題一：完成不是有限狀態遷移

令：

x_n=1-10^{-n}.

則：

\forall n\in\mathbb N,\;x_n<1,

但：

\sup_nx_n=1.

故任何把：

\mathsf{Comp}((x_n)_n)=1

解釋為存在有限 $N$ 使：

x_N=1

的模型都不正確。

意義。 完成算子的輸入型別必須是鏈、網、序列、濾子或其他圖表，而不是單一有限狀態。

17.2 命題二：十進位流—完成相干

令：

p_n=9^n, \qquad s_9=9^\omega.

則：

\operatorname{pref}_n(s_9)=p_n,

並且：

\operatorname{Val}(s_9) = \mathsf{Comp}_{\sup}\bigl((v_n(p_n))_n\bigr) =1.

證明。 $v_n(p_n)=1-10^{-n}$ ，而該單調鏈上確界為 $1$ ；無限級數求值同樣為 $1$ 。證畢。

意義。 餘遞歸展開與完成提升可在此案例中相干，但它們仍為不同算子。

17.3 命題三：捨入投影一般非單射

令 $F$ 為有限浮點格式， $\rho$ 為固定捨入模式。因：

|\mathbb R|>|\mathsf{Float}_F|,

所以：

\operatorname{round}_{F,\rho}:\mathbb R\to\mathsf{Float}_F

不可能為單射。

故存在：

x\neq y,

但：

\operatorname{round}_{F,\rho}(x) = \operatorname{round}_{F,\rho}(y).

意義。 浮點投影後的相等不能反推精確實數相等。

17.4 命題四：有限浮點解碼具有局部精確性

若 $f$ 為非例外有限格式值，則存在：

r_f\in\mathbb Q_b

使：

\operatorname{decode}_F(f)=r_f.

若把同一數值的多個原始格式表示依任務適當商化，則解碼可視為嵌入到 $\mathbb R$ 的一個有限子集。

意義。 浮點的問題通常不是「每個值都含糊」，而是運算與轉換相對於欲表達的精確目標可能產生投影誤差或例外。

17.5 定理五：精確橋接的複合

若：

\llbracket B_1x\rrbracket_Y = \overline B_1\llbracket x\rrbracket_X

與：

\llbracket B_2y\rrbracket_Z = \overline B_2\llbracket y\rrbracket_Y,

則：

\llbracket B_2(B_1x)\rrbracket_Z = (\overline B_2\circ\overline B_1) \llbracket x\rrbracket_X.

證明。 代入第二式中的 $y=B_1x$ ，再使用第一式。證畢。

意義。 有了每段相干證書，跨域鏈才可被組合；否則「很多步都差不多對」不構成整體正確性。

17.6 定理六：商下降準則

令：

Q:X\to X/{\sim}.

對：

B:X\to Y,

若存在：

\overline B:X/{\sim}\to Y

使：

\overline B\circ Q=B,

則必有：

x\sim x' \Rightarrow B(x)=B(x').

反之，若此保持條件成立，則 $\overline B([x])=B(x)$ 良定義。

意義。 任何打算先把表示商化、再讓算子作用的方案，都必須做這個檢查。

17.7 命題七：有限觀察不能一般地決定精確相等

令精確實數以任意精化名稱給出。對每個固定精度 $k$ ，都可存在不同實數 $x\neq y$ ，其前 $k$ 層近似相同或落在同一誤差包絡中。

因此：

\text{固定有限精度相同} \not\Rightarrow \text{精確實數相等}.

這也是為何：

\text{有限前綴皆不足以獨立輸出 }1

與：

0.999\ldots=1

可以同時成立。

17.8 命題八：例外域不可由普通等號吸收

若：

\mathsf{NaN}\notin\mathbb R,

則不存在保持普通實數算術全部性質的嵌入：

\mathsf{Float}\to\mathbb R.

任何把全部浮點資料直接視為實數的模型，必然遺失例外語義、比較語義或運算語義之一。

十八、六個測試案例

案例 A：有限全 $9$ 前綴

輸入：

p_n=9^n.

正確輸出：

v_n(p_n)=1-10^{-n}<1.

不可接受輸出：

v_n(p_n)=1.

除非已明示改用浮點捨入，而非精確有理求值。

案例 B：全 $9$ 無限流

輸入：

s_9=9^\omega.

正確鏈：

s_9 \xrightarrow{\operatorname{Val}} 1.

不可接受說法：

機器必須先把所有 $9$ 寫完，才能使流具有語義。

因為流的餘遞歸規格、其指稱語義與物理輸出痕跡是不同層。

案例 C：十進位字面值到 binary64

輸入：

\texttt{"0.1"}.

正確鏈：

\mathsf{Text} \xrightarrow{\operatorname{parse}_{10}} \frac1{10} \xrightarrow{\operatorname{round}_{\mathrm{binary64},\rho}} f.

語義上：

\operatorname{decode}(f) \neq \frac1{10}

通常成立。

不可接受說法：

binary64 中的 $f$ 就是十進位的 $0.1$ 。

案例 D：足夠接近 $1$ 的有限字面值

輸入：

1-10^{-n}.

當 $n$ 夠大時，對某格式與捨入模式可能：

\operatorname{round}_{F,\rho}(1-10^{-n}) = \operatorname{round}_{F,\rho}(1).

這只證明同一浮點格點，不證明原始精確有理數相等。

案例 E： $+\!0$ 與 $-\!0$

輸入：

+0, \qquad -0.

若任務是純實數值：

\operatorname{decode}(+0) = \operatorname{decode}(-0) =0.

若任務需保留符號、位元序、極限方向或特定浮點操作，則不應先商化。

案例 F： $\mathsf{NaN}$

輸入：

\mathsf{NaN}.

正確處理是進入例外／非數值分支，而不是任選一個實數 $x$ 使：

\mathsf{NaN}=x.

此案例防止「所有符號都必有一個單一實數本體」的過度簡化。

十九、常見失敗模式：跨域 GAP 真正在哪裡

19.1 把完成誤寫成最後一步

錯誤形式：

x_0\to x_1\to\cdots\to x_N=1.

對全 $9$ 前綴鏈，這不存在。

正確形式：

\mathsf{Comp}\bigl((x_n)_n\bigr)=1.

錯誤的來源是把圖表層算子偽裝成狀態層算子。

19.2 把無限流誤寫成已實體化的記憶體內容

錯誤形式：

9^\omega = \text{某段有限記憶體中的全部 }9.

正確形式是：

\text{有限規格} \xrightarrow{\mathsf{Unfold}} \text{無限行為語義}.

機器可以在有限時間內保存規格、按需產生有限前綴、或計算要求精度的近似；它不需要真的儲存無限資料。

19.3 把浮點相等誤寫成實數相等

錯誤形式：

\operatorname{round}_{F}(x) = \operatorname{round}_{F}(y) \Rightarrow x=y.

這違反命題三。捨入是多對一投影。

19.4 把實數等值誤寫成原始表示相等

錯誤形式：

\operatorname{Val}(p) = \operatorname{Val}(q) \Rightarrow p=q.

十進位雙重表示直接反駁此式。

19.5 把誤差小誤寫成誤差已被控制

錯誤形式：

\widetilde x\approx x.

若沒有指定：

d(\widetilde x,x)\le\varepsilon

或：

x\in\gamma(\widetilde I),

就不能把近似帶入後續定理。

19.6 把例外值當作數值邊界

$+\infty$ 有時能在擴張實數中被處理； $\mathsf{NaN}$ 則不是「非常大的數」也不是「未知但必為某個實數」。

錯誤把例外值塞進普通數值域會使：

\text{比較}, \quad \text{排序}, \quad \text{傳播}, \quad \text{錯誤處理}

全部失去明確語義。

19.7 把不同跨域箭頭全叫作投影

完成通常把近似圖表映到規範結果；捨入把精確語義映到有限格點；商化辨識表示；區間包絡保留可能集；解析改變編碼。

它們不應全被叫成：

P:X\to Y.

名字可以短，類型與證書不能短。

19.8 把範疇論圖畫成證明本身

可交換圖是對需要證明之相干的精確表述，不是自動成立的理由。每一個正方形都必須由定義、定理、誤差界或泛性質支持。

所以：

\text{畫出圖} \not\Rightarrow \text{圖可交換}.

這一點尤其重要於跨域論證：圖能暴露 GAP，但不能替代填補 GAP。

二十、跨域算子演算：從口頭轉換到可驗證鏈

20.1 一條橋接鏈的標準形式

任何跨域敘述可正規化為：

X_0 \xrightarrow{B_1} X_1 \xrightarrow{B_2} \cdots \xrightarrow{B_n} X_n,

並為每一段登錄：

(X_i,\llbracket-\rrbracket_i,B_i,\kappa_i,\mathcal C_i,\varepsilon_i,\mathsf{Exc}_i).

這使自然語言中的「變成」「映射」「顯化」「收斂」「投影」可以被拆成可檢查元件。

20.2 十進位的標準橋接鏈

可寫成：

\mathsf{Spec}_{9} \xrightarrow{\mathsf{Unfold}} \mathsf{Stream}_{10} \xrightarrow{\operatorname{Val}} \mathbb R,

以及：

\mathsf{FinStr}_{10}^{\mathbb N} \xrightarrow{v_\bullet} \operatorname{Dir}_\uparrow(\mathbb Q) \xrightarrow{\mathsf{Comp}_{\sup}} \mathbb R.

再以：

\mathsf{Rep}_{10} \xrightarrow{Q_{\operatorname{Val}}} \mathsf{DecReal}_{10} \cong \mathbb R

處理表示同一。

20.3 機器數值的標準橋接鏈

一個有限十進位 literal 進入二進位浮點可寫成：

\mathsf{Text} \xrightarrow{\mathsf{Lex}} \mathsf{FinDecimal} \xrightarrow{\operatorname{parse}_{\mathbb Q}} \mathbb Q \xrightarrow{\operatorname{round}_{F,\rho}} \mathsf{Float}_{F}.

為了驗證其相對於目標實數的意義，再加：

\mathsf{Float}_{F}^{\mathrm{finite}} \xrightarrow{\operatorname{decode}_F} \mathbb R.

整條鏈的真實語義不是「字串等於浮點」，而是：

\operatorname{decode}_F( \operatorname{round}_{F,\rho}( \operatorname{parse}_{\mathbb Q}(s)))

與原字面值語義之間的精確或近似關係。

20.4 升階、降階與橫移

本文把跨域箭頭依資訊方向分成三種。

方向	形式	例子
升階	近似／名稱／圖表到完成語義	Cauchy name 到實數
降階	精確語義到有限表示	實數到 float
橫移	同語義域的重編碼	二進位字串到 dyadic rational

商化不完全屬於三者之一；它改變的是可區分性：

X\to X/{\sim}.

20.5 可逆性光譜

對橋接 $B:X\to Y$ ，不要只問「能不能逆」，而應判斷：

是否有嚴格逆：

B^{-1}:Y\to X;

是否有左逆或右逆；
是否只在子域可逆；
是否只能選擇一個集合論截面；
是否存在連續截面；
是否可由區間或候選集合重構；
是否只能以機率或後驗分布重構。

浮點捨入通常在整個 $\mathbb R$ 上沒有逆；十進位求值可有集合論代表選擇，但不存在自然的全域連續正規形；區間包絡通常只能提供候選集合。

20.6 保持量表

每一橋接還需標記保留什麼：

性質	可能狀態
數值	精確保留／近似保留／不保留
順序	保留／僅單調／不保留
拓樸	連續／不連續／未定義
代數運算	同態／近似同態／不保留
進位歷史	保留／遺忘
資訊量	增加／降低／改編碼
可執行性	可計算／半可計算／不保證
例外行為	無／可傳播／可恢復

沒有這張保持量表，「跨域轉換」仍只是一句抽象敘述。

20.7 跨域橋接的最小證明格式

對每個 $B:X\to Y$ ，建議提供以下七項：

型別：

B:X\to Y;

語義：

\llbracket-\rrbracket_X, \quad \llbracket-\rrbracket_Y;

分類：

\kappa(B);

相干方程、誤差界或包含關係；
可逆性或不可逆性證明；
商下降條件；
例外與執行條件。

這就是本文所說的跨域轉換證書。

二十一、面向程式語言的最小中介表示

21.1 為何需要中介表示

若未來的 EML、視覺化程式語言或 AI 程式代理要安全地操作不同數值與符號域，僅靠型別名稱例如：

\texttt{float}, \quad \texttt{decimal}, \quad \texttt{real}

仍不夠。它們需要知道轉換是否精確、是否捨入、是否可逆、是否會產生例外，以及誤差能否累積。

21.2 橋接中介表示

可把一個橋接節點表示為：

\mathsf{BridgeNode} = \bigl( \mathsf{sourceType}, \mathsf{targetType}, \mathsf{kind}, \mathsf{semanticMap}, \mathsf{certificate}, \mathsf{loss}, \mathsf{exceptions}, \mathsf{cost} \bigr).

其中：

$\mathsf{kind}$ 為七類橋接之一；
$\mathsf{certificate}$ 可為等式、誤差界、區間包含或商下降證明；
$\mathsf{loss}$ 記錄不可逆資訊；
$\mathsf{exceptions}$ 記錄可能例外；
$\mathsf{cost}$ 記錄時間、空間、精度或查詢成本。

21.3 一個抽象程式片段

不把它當作特定語言語法，而把它讀為型別化意圖：

\begin{aligned} p&:\mathsf{FinDecimal},\\ r&=\operatorname{prefixEval}(p):\mathsf{Rational},\\ \gamma&:\mathsf{BoundedDirectedChain}(\mathsf{Rational}),\\ x&=\operatorname{complete}(\gamma):\mathsf{ExactReal},\\ f&=\operatorname{round}_{F,\rho}(x):\mathsf{Float}_{F},\\ I&=\operatorname{enclose}_k(x):\mathsf{Interval}. \end{aligned}

其中：

x, \quad f, \quad I

不是可任意互換的三種「數」。

21.4 靜態檢查可阻止的錯誤

一個具備橋接資料的編譯器或 AI 代理至少可以拒絕：

把 $\mathsf{NaN}$ 當作 $\mathsf{ExactReal}$ ；
未提供誤差界就以浮點值證明實數不等式；
對單一有限前綴呼叫完成算子；
將流直接塞入有限浮點格式；
在未驗證下降條件下先商化再套用表示算子；
將不同捨入模式視為同一算子；
將未終止的精確實數判等視為已完成決策。

21.5 執行期追蹤

跨域節點也可產生可視化追蹤：

\mathsf{Trace}(B,x) = (\text{來源載體},\text{目標載體},\text{證書},\text{誤差},\text{例外},\text{成本}).

這與 PHOSPHOR 式的複雜度觀測可以自然接合：不只觀察程式跑了幾步，也觀察它每一步跨了什麼語義域、失去多少資訊、是否仍有可追溯的正確性證書。

21.6 AI 代理的實務含義

對 AI 而言，跨域錯誤常不是演算法不會算，而是：

\text{符號域} \to \text{數值域} \to \text{近似域} \to \text{決策域}

中有未被標記的轉換。

若 AI 代理以橋接證書作為內部資料，它可以在回答或執行前主動提出：

此處由精確有理數降至 binary64，數值語義只保留至指定誤差；若後續需證明等號，應改用區間或精確實數。

這正是算子本體論從哲學語言進入可操作代理架構的一條路。

二十二、驗證階梯：從紙上相干到機器可檢查

22.1 第一階：純數學核心

可先在不涉及完整 IEEE 細節的模型中形式化：

有限全 $9$ 前綴：

v_n(9^n)=1-10^{-n};

單調有界鏈：

\sup_n(1-10^{-n})=1;

十進位流求值：

\operatorname{Val}(9^\omega)=1;

進位等價：

(0,9^\omega)\sim_{\operatorname{Val}}(1,0^\omega);

商下降準則；
精確橋接複合定理。

這一階可在 Lean、Coq、Agda 或其他證明助理中處理。

22.2 第二階：玩具浮點模型

在小基數、有限尾數、有限指數的玩具格式中定義：

\mathsf{ToyFloat}_{b,p,E}.

並證明：

有限值的精確解碼；
捨入的範圍與單調性；
捨入非單射；
$+\!0/-\!0$ 的原始與數值關係；
例外域與普通域分離；
有向捨入的區間包絡正確性。

先完成玩具模型，才能知道後續針對完整標準的形式化究竟增加了哪些真實複雜度。

22.3 第三階：標準規格映射

再把：

\mathsf{ToyFloat}_{b,p,E}

映射到 IEEE 754 實際格式族，增加：

normal 與 subnormal；
多種捨入模式；
例外旗標；
NaN payload；
字串轉換；
fused operations；
total order 與比較謂詞。

這一步不應只依賴測試輸出，而要保留規格條款到形式模型的可追溯映射。

22.4 第四階：實作與證明的精化

理想鏈為：

\text{抽象實數定義} \rightsquigarrow \text{精確名稱演算法} \rightsquigarrow \text{區間／浮點實作} \rightsquigarrow \text{機器碼}.

每次精化都應有：

\mathsf{Refine}_{i+1} \models \mathsf{Spec}_i.

這正是把「算子跨域」落實成可驗證軟體的方式，而不是只在最終輸出做幾個數值比對。

22.5 第五階：反例驅動測試庫

最低測試庫至少應含：

測試	要防止的錯誤
$0.999\ldots$	完成被誤寫為最後一步
$0.1$ 到 binary64	十進位 literal 被誤當精確二進位值
$+\!0/-\!0$	數值商化過早
$\mathsf{NaN}$	例外被塞入實數
溢位／下溢	有限格式被誤當無界域
directed rounding	誤差無方向
迭代計算	誤差複合被忽略
雙重十進位表示	指稱相等被誤當字串相等

這個測試庫可以成為未來跨域算子語言或 AI 代理的回歸測試核心。

二十三、研究邊界與可否證性

23.1 若橋接無法附證書

若一個宣稱的跨域算子既沒有：

\text{精確方程}, \quad \text{誤差界}, \quad \text{包含關係}, \quad \text{商下降證明}, \quad \text{或例外規格},

則它暫時只是候選映射，而不是已建立橋接。

23.2 若框架只能事後命名

若框架對任何結果都說：

這是某種完成、投影或 $\Omega$ 轉換，

但無法預先判定其輸入型別、保留量與失敗條件，則它不是通用演算，只是回顧性命名。

23.3 若不同領域不能共享證書

本文不要求所有領域同構；但至少要求可比較：

\mathsf{Exact}, \qquad \mathsf{Approx}(\varepsilon), \qquad \mathsf{Enclose}(\gamma), \qquad \mathsf{Quotient}(\sim), \qquad \mathsf{Exception}.

若連這些證書型別都無法跨域對照，則「通用算子本體論」的範圍必須收縮為某個特定學科內的局部理論。

23.4 若完成被誤用於不存在的界

不是每條鏈都有完成值。若：

x_n=n,

在普通實數域中沒有有限實數上確界；若：

x_n=(-1)^n,

它不是單調鏈，且不收斂。

所以：

\mathsf{Comp}

必須帶有適用條件，不能成為「無限過程都會自動給出終點」的萬用詞。

23.5 若投影被誤用為本體遺失

一個投影失去資訊，並不自動表示來源本體不存在或被毀滅。它只表示該表示算子不能由結果唯一重構來源。

因此：

\text{投影不可逆} \not\Rightarrow \text{來源不存在}.

這與本體—表象接口論的限制一致：來源、表示、觀察與重構必須分開。

23.6 若物理實現沒有可區辨內容

從：

\text{程式可表達精確實數名稱}

不能推出：

\text{自然界以該名稱語義運作}.

算子本體論若要對物理提出主張，仍需給出可觀察、可測量、可與競爭模型區分的預測。本文只建立數學與計算語義上的跨域協議。

二十四、結論： $0.999\ldots$ 是跨域語義的最小閘門

本文的出發點不是要再證明一次：

0.999\ldots=1.

而是要指出：若一個框架想讓「算子」「狀態變化」「跨域轉換」「完成」「投影」成為可通用使用的概念，它就必須先通過這個最小案例。

全 $9$ 案例同時要求：

\text{有限字} \to \text{有理前綴} \to \text{有向近似圖表} \to \text{實數完成},

也要求：

\text{有限規格} \to \text{無限流} \to \text{實數求值},

並要求：

\text{原始表示} \to \text{核群胚} \to \text{商同一}.

一旦進入計算機，還必須加入：

\text{精確實數} \to \text{浮點投影} \to \text{誤差／區間／例外處理}.

其中最重要的修正是：

\boxed{ \text{完成不是最後一步，} \quad \text{捨入不是實數等號，} \quad \text{流不是已執行痕跡。} }

因此，本文提出的完成—投影雙向語義不是附加功能，而是算子本體論從單域關係語言走向跨域演算的必要層。

其最簡潔的總圖為：

\boxed{ \begin{aligned} \mathsf{Finite\;Spec} &\xrightarrow{\mathsf{Unfold}} \mathsf{Infinite\;Behavior} \xrightarrow{\mathsf{Eval}} \mathsf{Exact\;Semantic}\\ &\xleftarrow{\mathsf{Complete}} \mathsf{Finite\;Approximation\;Diagram}\\ &\xrightarrow{\mathsf{Project}_{F,\rho}} \mathsf{Finite\;Machine\;Format}\\ &\xrightarrow{\mathsf{Decode}/\mathsf{Enclose}} \mathsf{Exact\;or\;Verified\;Semantic}. \end{aligned} }

每一箭頭都必須帶有型別、相干、誤差或包絡、商、例外與執行條件。只有這樣，算子本體論才不會把「近似、完成、轉碼、同一化、投影、狀態改變」全壓縮成一個看似深刻、實際卻未定義的「變成」。

附錄 A：十進位案例的完整橋接圖

A.1 有限前綴路徑

\begin{array}{ccc} p_n=9^n & \xrightarrow{\;v_n\;} & 1-10^{-n}\in\mathbb Q\\ \Big\downarrow{\text{形成鏈}} & & \Big\downarrow{\text{嵌入}}\\ (p_n)_n & \xrightarrow{\;\mathsf{Comp}\;} & 1\in\mathbb R \end{array}

關鍵不在左上到右下存在某個單點函數，而在底部的完成作用於整條鏈。

A.2 無限流路徑

\begin{array}{ccc} \mathsf{nine} & \xrightarrow{\;\mathsf{Unfold}\;} & 9^\omega\\ \Big\downarrow{} & & \Big\downarrow{\operatorname{Val}}\\ \mathsf{finite\;specification} & \xrightarrow{\;\text{denotation}\;} & 1\in\mathbb R \end{array}

A.3 表示商路徑

\begin{array}{ccc} (0,9^\omega) & \xrightarrow{\;Q\;} & [(0,9^\omega)]\\ \Big\downarrow{\operatorname{Val}} & & \Big\downarrow{\cong}\\ 1 & \xrightarrow{\;=\;} & 1 \end{array}

其中：

Q(0,9^\omega) = Q(1,0^\omega).

A.4 浮點投影路徑

\begin{array}{ccc} x\in\mathbb R & \xrightarrow{\;\operatorname{round}_{F,\rho}\;} & f\in\mathsf{Float}_{F}\\ \Big\downarrow{\operatorname{id}} & & \Big\downarrow{\operatorname{decode}_F}\\ x & \xrightarrow{\;\approx_{\varepsilon}\;} & \operatorname{decode}_F(f) \end{array}

這張圖一般不是嚴格可交換圖；它應由誤差界或區間包含取代。

附錄 B：最小跨域橋接偽程式

B.1 類型宣告

\begin{aligned} \mathsf{FinDecimal}&=\text{有限十進位字},\\ \mathsf{DecimalStream}&=\text{數位流},\\ \mathsf{ExactReal}&=\text{實數名稱},\\ \mathsf{Float}_F&=\text{格式 }F\text{ 的浮點值},\\ \mathsf{Interval}&=\text{實數區間},\\ \mathsf{MachineResult}_F&= \mathsf{FiniteFloat}_F+\mathsf{PosInf}+\mathsf{NegInf}+\mathsf{NaN}. \end{aligned}

B.2 算子宣告

\begin{aligned} \operatorname{prefixEval}&: \mathsf{FinDecimal}\to\mathsf{Rational},\\ \operatorname{unfold}&: \mathsf{Spec}\to\mathsf{DecimalStream},\\ \operatorname{streamEval}&: \mathsf{DecimalStream}\to\mathsf{ExactReal},\\ \operatorname{complete}&: \mathsf{BoundedDirectedChain}(\mathsf{Rational}) \to\mathsf{ExactReal},\\ \operatorname{round}_{F,\rho}&: \mathsf{ExactReal}\to\mathsf{MachineResult}_F,\\ \operatorname{enclose}_k&: \mathsf{ExactReal}\to\mathsf{Interval}. \end{aligned}

B.3 正確使用

\begin{aligned} \gamma&=(\operatorname{prefixEval}(9^n))_{n\in\mathbb N},\\ x&=\operatorname{complete}(\gamma),\\ I_k&=\operatorname{enclose}_k(x),\\ m&=\operatorname{round}_{F,\rho}(x). \end{aligned}

此處：

x=1,

但：

\operatorname{prefixEval}(9^n)<1

對每個有限 $n$ 仍成立。

附錄 C：跨域算子審核清單

C.1 載體

來源載體 $X$ 是字串、狀態、流、圖表、名稱、實數、區間還是機器格式？
目標載體 $Y$ 是什麼？
$X$ 與 $Y$ 是否都被明確定義？
是否把例外值、空值、未終止或外部效應放入和型別？

C.2 輸入形狀

算子作用於單一元素：

T:X\to Y,

還是作用於整條圖表：

\mathsf{Comp}:\operatorname{Diag}(X)\to\widehat X?

是否誤把序列、流或分布當成單一狀態？

C.3 語義

$\llbracket-\rrbracket_X$ 與 $\llbracket-\rrbracket_Y$ 是什麼？
算子保留的是數值、順序、拓樸、代數、歷史或任務結果中的哪些量？
是否有精確相干方程？
若不精確，是否給誤差界或包含關係？

C.4 資訊方向

這是編碼、展開、完成、商化、投影、包絡還是例外逃逸？
它增加、遺忘、重編碼還是保守包住資訊？
是否存在逆、部分逆、截面或重構集合？

C.5 商與同一性

原始相等、語義相等、商後相等分別是什麼？
何種差異會被商掉？
算子是否保持等價關係，因而可下降？
是否需要保留群胚路徑或僅需集合商？

C.6 數值與執行

是否指定目標格式與捨入模式？
是否處理 $+\!0/-\!0$ 、 $\mathsf{NaN}$ 、 $\pm\infty$ 、溢位與下溢？
誤差如何隨複合累積？
是否有區間或其他保守驗證方式？
抽象語義是否被錯誤地聲稱為已物理執行？

C.7 反例

有沒有一個輸入會使完成不存在？
有沒有一個輸入會進入例外域？
有沒有兩個不同精確值投影到同一有限表示？
有沒有兩個不同表示指稱同一語義值？
有沒有一個算子不能下降到所選商？

若上述任一項未回答，跨域敘述應保留為研究問題，而非標記為已完成轉換。

附錄 D：與既有論文的依賴與分工

D.1 《未執行的無限是否已經完成？》

該文分開：

\text{規則}, \quad \text{抽象軌跡}, \quad \text{物理執行}, \quad \text{極限}, \quad \text{指稱}.

本篇承接其「極限是外部作用於整條序列的算子」結論，並把它擴張到程式語言的精確實數名稱、浮點投影與執行證書。

D.2 《從歸納到餘歸納》

該文建立：

D^\ast \quad\text{與}\quad D^{\mathbb N}

的型別分離，並以初始代數、終餘代數與前綴樹連接有限字與無限流。

本篇把這個分離落入：

\mathsf{FinDecimal}, \quad \mathsf{DecimalStream}, \quad \mathsf{ExactReal}

等可計算橋接型別。

D.3 《不到達而完成》

該文證明：

\sup_n(1-10^{-n}) = \operatorname{lfp}(T_9) =1.

本篇進一步指出，此完成算子必須具有：

\operatorname{Diag}(X)\to\widehat X

的圖表型別，不能被誤用為一般狀態更新。

D.4 《表示不同，指稱同一》

該文建立進位核群胚、商型別與算子下降。

本篇把同一方法推到浮點格式： $+\!0/-\!0$ 、有限值與例外值都要求明示何時商化、何時保留原始表示。

D.5 《生成、展開、完成與同一化》

該總論提供：

\mathfrak O = (\Sigma,M,\mathfrak I,\mathsf{Comp},V,\mathcal G_V,Q,\mathsf{Exec}).

本篇的實質貢獻是補上：

\mathsf{Name}, \quad \mathsf{Lift}, \quad \mathsf{Project}, \quad \mathsf{Enclose}, \quad \mathsf{Err}, \quad \mathsf{Exc},

使其能處理有限機器與精確語義之間的雙向跨域問題。

D.6 《本體—表象接口論》

本體—表象接口論問的是來源結構如何經操作生成不同表象，並特別分析可逆性、選擇性、操作相對性與重構不確定性。

本篇把其中的接口概念收窄到一個更具體、可形式驗證的子問題：

在數值與程式語言中，跨載體的表示／完成／投影算子如何攜帶精確、誤差、包絡、商與例外證書？

它們相互支援，但不互相取代。

附錄 E：符號表

符號	含義
$D$	十進位數位集合 $\{0,\ldots,9\}$
$D^\ast$	有限十進位字
$D^{\mathbb N}$	無限十進位數位流
$p_n=9^n$	長度為 $n$ 的全 $9$ 前綴
$9^\omega$	全 $9$ 無限流
$v_n$	有限前綴的精確有理求值
$\gamma_9$	全 $9$ 前綴值所成的有向鏈
$\mathsf{Comp}$	對圖表、鏈或名稱的完成算子
$\operatorname{Val}$	十進位流或完整表示的實數求值
$Q$	商映射
$\sim_{\operatorname{Val}}$	求值核等價
$\mathsf{ExactReal}$	以名稱／oracle 實作的精確實數型別
$\mathsf{Float}_{b,p,E}$	浮點格式
$\operatorname{round}_{F,\rho}$	依格式與模式 $\rho$ 的捨入投影
$\operatorname{decode}_F$	有限浮點值的精確解碼
$\mathbb Q_b$	分母為 $b$ 冪的有理數子域
$\mathsf{Int}(\mathbb R)$	實數閉區間域
$\gamma$	區間或抽象元素的 concretization
$\alpha$	從具體集合到抽象域的 abstraction
$\mathfrak B$	跨域橋接算子規格
$\kappa$	橋接類型
$\varepsilon$	誤差界資料
$\mathsf{Exc}$	例外域與例外規格
$\mathsf{Lift}$	從近似／名稱到完成語義的提升
$\mathsf{Project}$	從精確語義到有限格式的投影
$\mathsf{Enclose}$	產生保守包絡的算子

參考文獻

IEEE. “IEEE Standard for Floating-Point Arithmetic.” IEEE Std 754-2019, 2019. DOI: 10.1109/IEEESTD.2019.8766229.
IEEE. “IEEE Standard for Interval Arithmetic.” IEEE Std 1788-2015, 2015.
Boehm, H.-J., Cartwright, R., Riggle, M., & O'Donnell, M. J. “Exact Real Arithmetic: A Case Study in Higher Order Programming.” Proceedings of the 1986 ACM Conference on LISP and Functional Programming, 1986, 162–173.
Boehm, H.-J. “The Constructive Reals as a Java Library.” Journal of Logic and Algebraic Programming, 64(1), 2005, 3–11.
Edalat, A. “A Domain-Theoretic Approach to Computability on the Real Line.” Theoretical Computer Science, 210(1), 1999, 73–98.
Abramsky, S., & Jung, A. “Domain Theory.” In Handbook of Logic in Computer Science, Vol. 3, Oxford University Press, 1994.
Escardó, M. H. “Introduction to Exact Numerical Computation.” ISSAC 2000 tutorial notes, 2000.
Goldberg, D. “What Every Computer Scientist Should Know About Floating-Point Arithmetic.” ACM Computing Surveys, 23(1), 1991, 5–48.
Boldo, S., & Melquiond, G. “Some Formal Tools for Computer Arithmetic: Flocq and Gappa.” 28th IEEE Symposium on Computer Arithmetic, 2021.
Rutten, J. J. M. M. “Universal Coalgebra: A Theory of Systems.” Theoretical Computer Science, 249, 2000, 3–80.
Scott, D. S. “Continuous Lattices.” In Toposes, Algebraic Geometry and Logic, Lecture Notes in Mathematics 274, Springer, 1972, 97–136.
Riehl, E. “Category Theory in Context.” Dover Publications, 2016.
The Univalent Foundations Program. “Homotopy Type Theory: Univalent Foundations of Mathematics.” Institute for Advanced Study, 2013.
Neo.K. 《未執行的無限是否已經完成？數字生成、極限算子與程序本體論》, 2026.
Neo.K. 《從歸納到餘歸納：十進位前綴樹、終餘代數與無限數位流》, 2026.
Neo.K. 《不到達而完成：有向上確界、Scott 拓樸與十進位收縮算子的最小固定點》, 2026.
Neo.K. 《表示不同，指稱同一：十進位進位群胚、商型別與多層等號》, 2026.
Neo.K. 《生成、展開、完成與同一化：從十進位邊界到算子本體論》, 2026.
Neo.K. 《本體—表象接口論：操作相對表示、投影家族與跨域結構對應》, 2026.

文件資訊

文件類型： 程式語言語義／數值計算／精確實數／算子本體論論文
版本： v1.0
日期： 2026-07-12
狀態： 可獨立閱讀之公開研究草稿
系列： 「十進位邊界與算子本體論」
系列位置： 核心總論的計算語義續篇
前置依賴： 有限—無限型別分離、完成理論、表示商化、程序—指稱分離
核心貢獻： 建立完成—投影雙向語義、跨域橋接證書、浮點／精確實數／區間語義之統一接口

有限機器與無限實數之間_浮點數精確實數與跨域算子的完成投影雙向語義

有限機器與無限實數之間：浮點數、精確實數與跨域算子的完成—投影雙向語義

摘要

一、問題的真正形式：不是一個等式，而是一個轉換協議

1.1 為何上一輪總論仍不夠

1.2 不能再寫「 0.999…0.999\ldots0.999… 變成 111 」

1.3 本文的中心主張

1.4 本文的邊界

二、七個載體：同一個符號實際跨過哪些域

2.1 有限十進位字

2.2 有限前綴的有理值

2.3 無限數位流

2.4 完整十進位表示

2.5 精確實數語義

2.6 有限浮點格式

2.7 區間與保守近似

2.8 七域總表

三、跨域不是一種箭頭：七類橋接算子

3.1 精確重編碼

3.2 餘遞歸展開

3.3 完成提升

3.4 商同一化

3.5 捨入投影

3.6 區間包絡

3.7 例外逃逸

四、完成與投影：兩個方向相反的跨域運動

4.1 有限近似到精確語義

4.2 精確語義到有限機器表示

4.3 兩個箭頭不是互逆

4.4 「有限中的無限」與「無限中的有限」

五、 0.999…0.999\ldots0.999… 的四條精確路徑

5.1 有限字到有理值

5.2 有理鏈到實數完成

5.3 有限規格到無限流再到實數

5.4 表示商到同一實數

5.5 四路相干條件

六、精確實數不是無限記憶體中的小數

6.1 Cauchy name

6.2 程式有限，語義可任意精化

6.3 相等判定的非對稱

6.4 精確實數算子的正確型別

七、浮點數不是失敗的實數，而是另一種操作域

7.1 有限浮點的精確解碼

7.2 二進位 0.10.10.1 的典型分離

7.3 有限 999 字面值被捨入成 111 的陷阱

7.4 + ⁣0+\!0+0 與 − ⁣0-\!0−0

7.5 NaN\mathsf{NaN}NaN 與無限大

八、區間語義：把誤差改寫為包含關係

8.1 點近似的不足

8.2 區間 concretization

8.3 有向捨入與可驗證包絡

8.4 抽象解釋形式

8.5 區間不是實數的低級替代

九、跨域橋接算子的正式規格

9.1 為何普通函數簽名不夠

9.2 橋接規格

9.3 六種正確性證書

9.4 橋接種類 κ\kappaκ

9.5 圖表輸入與狀態輸入

十、相干圖：跨域轉換何時真正成立

10.1 精確可交換圖

10.2 完成圖

10.3 近似可交換圖

10.4 包含可交換圖

10.5 商相干圖

10.6 例外圖

十一、橋接的複合：精確、誤差與包絡如何累積

11.1 精確橋接可複合

11.2 誤差橋接的複合

11.3 包絡橋接的複合

11.4 例外的複合

11.5 跨域鏈的信任預算

十二、程式語言中的 0.999…0.999\ldots0.999… ：解析、求值與執行必須分開

12.1 省略號不是一般程式字面值

12.2 有限十進位字面值

12.3 無限流字面值

12.4 近似請求式求值

12.5 整體語義與物理執行

12.6 編譯器與語義模型不可互相偷換

十三、同一實數系統中的轉換，到底改變了什麼

1.2 不能再寫「 $0.999\ldots$ 變成 $1$ 」

五、 $0.999\ldots$ 的四條精確路徑

7.2 二進位 $0.1$ 的典型分離

7.3 有限 $9$ 字面值被捨入成 $1$ 的陷阱

7.4 $+\!0$ 與 $-\!0$

7.5 $\mathsf{NaN}$ 與無限大

9.4 橋接種類 $\kappa$

十二、程式語言中的 $0.999\ldots$ ：解析、求值與執行必須分開

13.2 在 $\mathbb R$ 中沒有數值狀態跳躍

案例 A：有限全 $9$ 前綴

案例 B：全 $9$ 無限流

案例 D：足夠接近 $1$ 的有限字面值

案例 E： $+\!0$ 與 $-\!0$

案例 F： $\mathsf{NaN}$