語義—形式—工程非同構論

跨層轉譯中的不變量保存、結構誤差與實作偏移

Semantic–Formal–Engineering Non-Isomorphism
Invariant Preservation, Structural Error, and Implementation Drift Across Translational Layers

作者：Neo.K（許筌崴）／EveMissLab
協作整理：OpenAI GPT-5.6 Thinking
日期：2026-07-23
性質：概念論文／方法論提案
狀態：初稿 v0.1

摘要

一個原始概念被提出之後，通常必須經過數學形式化、演算法設計、程式實作與實際執行，才能成為可驗證的技術或科學成果。然而，這些層級並不是同一對象的透明複製。原始語義包含尚未完全封閉的可能展開；形式化則必須選擇座標、尺度、邊界與假設；演算法進一步決定操作次序與資料存取方式；程式實作又受資料結構、語言、函式庫與硬體限制；實際執行則受到浮點誤差、排程、記憶體、編譯器與環境條件影響。

本文提出「語義—形式—工程非同構論」，主張原始語義、形式模型、演算法、實作與執行之間通常不存在完全同構關係。跨層轉譯不是無損映射，而是選擇性保存、主動壓縮、假設注入與結構重構。某一層中的局部錯誤，也不一定只造成小幅數值偏差；它可能改變下一層的狀態空間、可達路徑、複雜度類別與可觀察行為。

本文建立五層轉譯鏈、六類等價關係、五項基本公理、跨層保真矩陣、結構誤差模型及反向診斷程序。本文並將需求工程、形式方法、編譯驗證、科學模型、科學計算與軟體工程中的相關研究整合為一個統一框架。其目的不是否定形式化或工程實作，而是使研究者能更精確地回答：哪些性質被保存、哪些資訊被壓縮、哪些假設是後來加入、失敗究竟發生在哪一層，以及工程失敗何時能夠反證原始概念。

關鍵詞： 語義形式化、非同構、形式方法、演算法、計算工程、不變量、結構誤差、語義保存、實作偏移、跨層轉譯

一、問題的提出

科學、數學與工程常以一條看似自然的路徑推進：

\text{概念} \rightarrow \text{公式} \rightarrow \text{演算法} \rightarrow \text{程式} \rightarrow \text{結果}

在日常敘述中，這條鏈容易被理解為同一內容逐步被寫得更精確。於是人們常默認：

概念被公式完整表達；
公式被演算法忠實實現；
演算法被程式直接翻譯；
程式執行等於理論運作；
實驗失敗等於理論失敗；
形式證明成立等於現實主張成立。

但實際研究中，這些推論經常失效。

一個自然語言需求可能在形式規格中遺失語境；一條正確公式可能被放在錯誤的指稱位置；兩個輸出相同的演算法可能具有完全不同的時間與空間成本；同一份程式在不同硬體上可能產生不同的數值結果；一個實作錯誤可能被誤判為概念反例；反過來，一個概念也可能長期被「只是工程還沒做好」保護，而逃避真正的反證。

因此，核心問題不是：

概念、公式與程式是否有關？

而是：

它們以何種方式相關？哪些性質被保存？哪些性質被重構？哪些錯誤會被放大？哪些失敗能向上回溯？

本文將這個問題抽象為一條五層轉譯鏈。

二、五層轉譯鏈

令：

$\mathcal S$ ：原始語義生成空間；
$\mathcal F$ ：形式模型空間；
$\mathcal A$ ：演算法空間；
$\mathcal I$ ：實作空間；
$\mathcal E_h$ ：環境 $h$ 下的實際執行空間。

則整體過程為：

\mathcal S \xrightarrow{\Phi} \mathcal F \xrightarrow{\Gamma} \mathcal A \xrightarrow{\Lambda} \mathcal I \xrightarrow{\Xi_h} \mathcal E_h

其中：

$\Phi$ ：形式化映射；
$\Gamma$ ：演算法化映射；
$\Lambda$ ：工程實作映射；
$\Xi_h$ ：環境化執行映射。

本文的核心主張是：

\boxed{ \mathcal S \not\cong \mathcal F \not\cong \mathcal A \not\cong \mathcal I \not\cong \mathcal E_h }

這裡的「非同構」不是指它們毫無對應關係，而是指通常不存在同時滿足以下條件的雙向映射：

一一對應；
完全可逆；
保存全部結構；
保存全部語義；
保存全部資源性質；
保存全部可觀察行為。

大多數實際轉譯只保存其中部分。

三、第一層：原始語義生成空間

3.1 概念不是一句話

原始概念通常不是一句自然語言命題，也不是一個固定定義。它更接近一個尚可繼續展開的語義生成狀態。

定義：

\mathcal S = (I,G,C,V,U)

其中：

$I$ ：核心意圖；
$G$ ：可繼續展開的語義方向；
$C$ ：概念約束；
$V$ ：希望保存的價值與不變量；
$U$ ：尚未決定的部分。

例如「只處理相關資訊」可能同時包含：

空間上的局部性；
語義上的局部性；
因果上的局部性；
時間上的局部性；
風險上的局部性；
資源上的局部性。

原始概念不必立刻決定「相關」應由距離、機率、相似度、因果圖或規則表示。

因此，原始概念具有未封閉性：

|\operatorname{Possible}(\mathcal S)|>1

也就是說，一個概念通常對應多個可能的形式模型。

3.2 語義展開態根

本文將這種尚未完全封閉、但已具有穩定生成方向的核心稱為：

語義展開態根（semantic generative root）

令其為：

\mathcal R_S = (I,\mathcal G,\mathcal B)

其中：

$I$ 是不應遺失的核心意圖；
$\mathcal G$ 是可允許的展開方向；
$\mathcal B$ 是不可跨越的概念邊界。

語義展開態根不是任意模糊。它仍具有約束，但這些約束未必已被壓縮成單一數學物件。

四、第二層：形式化不是複製，而是選擇

4.1 形式化映射

形式化可表示為：

\mathcal F = \Phi(\mathcal S;\theta_\Phi)

其中 $\theta_\Phi$ 代表形式化者加入的選擇，例如：

座標系；
變數；
度量；
邊界條件；
目標函數；
離散化；
機率假設；
連續性假設；
可微性假設；
對稱性假設。

因此，形式模型不是單純的：

\Phi(\mathcal S)

而是：

\boxed{ \text{原始語義} + \text{形式化選擇} }

4.2 有損壓縮

形式化通常會把多個語義狀態壓縮為同一個形式狀態：

s_1\neq s_2, \qquad \Phi(s_1)=\Phi(s_2)

這表示 $\Phi$ 可能不是單射。

同時，形式模型中也可能存在原始語義沒有明確要求的狀態：

\exists f\in\mathcal F, \quad f\notin\Phi(\mathcal S)

這表示形式空間也可能比原始概念切片更大。

因此形式化同時具有兩種作用：

語義壓縮：刪除或合併部分原始差異；
形式新增：加入尺度、邊界、排序與可計算假設。

4.3 公式正確不等於指稱正確

考慮公式：

N(d)=k^d

它可以正確描述固定分支數為 $k$ 的樹在深度 $d$ 的節點數。

但若將它直接解讀為整個系統的執行時間：

T_{\mathrm{system}}=k^d

則問題未必出在代數，而是出在指稱。

完整系統成本可能是：

T_{\mathrm{system}} = T_{\mathrm{route}} + T_{\mathrm{construct}} + T_{\mathrm{compute}} + T_{\mathrm{communicate}} + T_{\mathrm{verify}} + T_{\mathrm{memory}}

因此可以區分四種公式正確性：

\mathbf C_F = ( c_{\mathrm{syntax}}, c_{\mathrm{reference}}, c_{\mathrm{scope}}, c_{\mathrm{system}} )

分別表示：

句法與推導正確；
變數指稱正確；
使用範圍正確；
系統成本與條件完整。

一條公式可能是：

\mathbf C_F=(1,0,0,0)

也就是「數學沒算錯，但用錯了位置」。

五、第三層：從形式模型到演算法

5.1 關係不等於操作

形式模型描述：

y=f(x)

演算法則必須決定：

如何找到輸入；
以何種順序處理；
是否保存中間狀態；
是否枚舉全集；
是否使用索引；
是否近似；
是否平行；
何時停止。

因此：

\mathcal A = \Gamma(\mathcal F;\theta_\Gamma)

其中 $\theta_\Gamma$ 包含操作策略。

同一個數學函數可能由多個演算法實現：

A_1(x)=A_2(x)=f(x)

但：

A_1\not\equiv_{\mathrm{op}}A_2

因為它們的操作次序、中間狀態與成本不同。

5.2 函數等價與資源非等價

例如兩個演算法都計算：

y_i = \sum_{j\in N(i)} a_{ij}v_j

演算法甲可能：

枚舉所有 $(i,j)$ ；
判斷 $j\in N(i)$ ；
丟棄不需要的項。

成本：

O(n^2)

演算法乙可能：

直接讀取鄰接表；
只枚舉有效邊；
只計算存在的關係。

成本：

O(|E|)

因此：

A_1\equiv_{\mathrm{function}}A_2

但：

A_1\not\equiv_{\mathrm{resource}}A_2

這說明：

\boxed{ \text{輸出相同} \not\Rightarrow \text{演算法相同} \not\Rightarrow \text{工程價值相同} }

六、第四層：演算法到實作

6.1 實作會加入新的結構

令：

\mathcal I = \Lambda(\mathcal A;\theta_\Lambda)

其中 $\theta_\Lambda$ 包含：

程式語言；
資料結構；
型別系統；
函式庫；
記憶體布局；
並行模型；
精度；
編譯器；
例外處理；
API 邊界。

演算法描述「要做什麼」，實作必須決定「如何被機器承載」。

6.2 資料結構不是中性容器

同一張圖可以用：

鄰接矩陣；
鄰接表；
CSR；
COO；
壓縮區塊；
雜湊索引；
trie；
分散式切片。

表示。

它們可能在抽象結構上等價：

G_{\mathrm{matrix}} \equiv G_{\mathrm{CSR}}

但在工程上具有不同性質：

記憶體成本；
建構時間；
查詢速度；
更新速度；
並行方式；
GPU 利用率；
通訊需求。

因此：

\boxed{ \text{資料結構是演算法語義的一部分。} }

6.3 隱性密集化

一個理論上稀疏的演算法，可能因為程式實作建立完整中間張量而重新變成密集計算。

形式上：

T_{\mathrm{theory}}=O(|E|)

但若實作建立：

M\in\mathbb R^{n\times n}

則實際成本可能重新成為：

T_{\mathrm{implementation}}=O(n^2)

這種現象稱為：

隱性密集化（implicit densification）

它是形式—工程非等價的一個典型案例。

七、第五層：程式到實際執行

7.1 執行是物理事件

實際結果不只由程式碼決定。

令：

e = \Xi_h( I, L, C, P, R, D )

其中：

$I$ ：實作；
$L$ ：函式庫版本；
$C$ ：編譯器與最佳化；
$P$ ：平行排程；
$R$ ：隨機性；
$D$ ：資料與環境；
$h$ ：硬體。

因此：

\Xi_{h_1}(I)\neq\Xi_{h_2}(I)

可能源於：

浮點次序；
非確定性 kernel；
記憶體分塊；
指令集差異；
並行 reduction；
編譯器重新排序；
快取與通訊瓶頸；
裝置精度不同。

7.2 理論複雜度與實際性能

即使兩個演算法同屬：

O(n\log n)

實際 wall-clock 仍可能差距巨大，因為：

T_{\mathrm{wall}} = T_{\mathrm{compute}} + T_{\mathrm{memory}} + T_{\mathrm{communication}} + T_{\mathrm{synchronization}} + T_{\mathrm{launch}}

漸近複雜度只描述部分增長趨勢，不描述：

常數項；
硬體適配；
核心利用率；
記憶體頻寬；
通訊拓撲；
kernel 啟動成本。

因此：

\boxed{ \text{漸近等價} \not\Rightarrow \text{實際性能等價} }

八、六類等價關係

「等價」不能作為單一詞使用。本文至少區分六類。

8.1 意圖等價

兩個表達是否承載相同核心目的：

x\equiv_I y

8.2 語義等價

兩個表達是否在指定語境中指向相同意義：

x\equiv_S y

8.3 函數等價

對所有合法輸入輸出相同：

f\equiv_F g \iff \forall x,\ f(x)=g(x)

8.4 操作等價

是否具有相同操作步驟、狀態轉移與可觀察歷史：

A\equiv_O B

8.5 資源等價

時間、空間、通訊與能耗是否近似相同：

A\equiv_R B

8.6 實證等價

在指定環境與測量容差下是否呈現相同結果：

I_1\equiv_E I_2

因此可能出現：

A\equiv_F B \quad\text{但}\quad A\not\equiv_O B \quad\text{且}\quad A\not\equiv_R B

這不是矛盾，而是不同等價層次。

九、語義—形式—工程非同構的五項公理

公理一：層級異質性

不同層級的基本對象、操作及正確性條件不同。

\operatorname{Type}(\mathcal S) \neq \operatorname{Type}(\mathcal F) \neq \operatorname{Type}(\mathcal A) \neq \operatorname{Type}(\mathcal I) \neq \operatorname{Type}(\mathcal E_h)

因此不能用單一正確性條件覆蓋所有層級。

公理二：轉譯選擇性

任何有限轉譯只能保存前一層的部分性質，除非另有證明。

\exists K: K(x)\neq K(\Phi(x))

公理三：假設注入

每次轉譯都會加入前一層沒有完全規定的新選擇。

M_{i+1} = T_i(M_i;\theta_i)

其中 $\theta_i$ 不可被忽略。

公理四：結構誤差非線性

跨層錯誤可能改變狀態空間、路由及複雜度類別，因此不能只視為加性數值誤差。

\Delta_{\mathrm{structure}} \not\approx \sum_i\epsilon_i

公理五：正確性向量化

正確性不是單一布林值，而是多維向量。

\mathbf C = ( C_{\mathrm{intent}}, C_{\mathrm{semantic}}, C_{\mathrm{formal}}, C_{\mathrm{behavioral}}, C_{\mathrm{resource}}, C_{\mathrm{empirical}} )

某個系統可以在輸出上正確，但在資源、順序、血緣或安全性上不正確。

十、結構誤差與誤差放大

10.1 數值誤差

一般數值誤差可近似為：

\epsilon_{\mathrm{total}} = \epsilon_1+\epsilon_2+\cdots+\epsilon_n

10.2 結構誤差

若某個錯誤改變：

節點集合；
邊集合；
分支條件；
狀態空間；
遞歸深度；
終止條件；
資料布局；

則它改變的不只是數值，而是後續運算圖。

令：

x_{t+1}=F_t(x_t)

錯誤版本為：

\tilde{x}_{t+1} = \tilde{F}_t(\tilde{x}_t)

若：

F_t\neq\tilde{F}_t

則問題不再只是：

\tilde{x}_t=x_t+\epsilon_t

而可能是：

\operatorname{Reach}(F) \neq \operatorname{Reach}(\tilde{F})

也就是可達狀態集合已改變。

10.3 複雜度相變

一個局部條件錯誤也可能改變複雜度類別。

例如：

|N(i)|\leq k

若被錯誤實作為：

N(i)=\{1,\ldots,n\}

則：

O(nk) \rightarrow O(n^2)

這不是常數項變差，而是複雜度相變。

本文將其稱為：

跨層結構敏感性（cross-layer structural sensitivity）

十一、不變量保存

既然完全等價通常不可能，研究目標應改為明確指定需要保存的不變量。

令：

\mathcal K = \{K_1,K_2,\ldots,K_m\}

對轉譯 $T_i$ ，要求：

K_j(x) = K_j(T_i(x))

或在近似情形下：

d_j \left( K_j(x), K_j(T_i(x)) \right) \leq\varepsilon_j

常見不變量包括：

核心意圖；
因果方向；
輸入輸出關係；
順序；
安全性；
完備性；
單調性；
層級關係；
可追蹤性；
複雜度上界；
誤差界；
資源限制。

因此「語義保存」不應只是一句口號，而應拆成：

\mathbf K = ( K_{\mathrm{intent}}, K_{\mathrm{behavior}}, K_{\mathrm{order}}, K_{\mathrm{resource}}, K_{\mathrm{lineage}}, K_{\mathrm{error}} )

十二、跨層保真矩陣

定義：

P_{ij} = \operatorname{Preserve} ( T_i, K_j )

其中 $T_i$ 是某一層轉譯， $K_j$ 是某項不變量。

可建立如下矩陣：

轉譯	核心意圖	函數輸出	順序	複雜度	血緣	可逆性
語義→形式	部分	未定	部分	未定	低	低
形式→演算法	高	高	視設計	不保證	中	低
演算法→實作	高	高	視並行	可能改變	高	中
實作→執行	近似	近似	可能非確定	環境依賴	可記錄	低

矩陣中的值可以是：

布林值；
$[0,1]$ 分數；
誤差上界；
證明狀態；
實驗信心水準。

例如：

P_{ij}\in \{ \text{proved}, \text{tested}, \text{assumed}, \text{unknown}, \text{violated} \}

這可防止研究論文只寫「已正確實作」，卻沒有說明正確的是哪一種性質。

十三、反向診斷：失敗發生在哪一層

13.1 反例不可直接向上傳遞

以下推論一般不成立：

\text{實作失敗} \Rightarrow \text{演算法失敗}

\text{演算法失敗} \Rightarrow \text{形式模型失敗}

\text{形式模型失敗} \Rightarrow \text{原始概念失敗}

更準確地說：

\boxed{ \text{實作反例} \neq \text{演算法反例} \neq \text{形式反例} \neq \text{概念反例} }

13.2 但原始概念不能永久免疫

反過來，也不能將所有失敗都歸因於「只是實作問題」。

應使用以下診斷程序：

確認失敗的可觀察現象；
找出違反了哪個不變量；
定位最早發生違反的轉譯；
檢查是否為形式化選擇、演算法、資料結構或環境問題；
嘗試至少一種替代轉譯；
若多種合理轉譯均反覆失敗，再回頭質疑原始概念。

可寫為：

L^* = \min \left\{ i: K_j(M_i)\neq K_j(M_{i+1}) \right\}

$L^*$ 是最早發生保真破壞的層級。

十四、現有研究如何觸及此問題

14.1 需求工程

需求工程長期處理自然語言需求、利益相關者意圖與正式規格之間的距離。Nuseibeh 與 Easterbrook 指出，需求並不是一次取得、固定不變的輸入，而是在理解、協商、建模與環境變化中演化的對象。

這對應本文的：

\mathcal S \xrightarrow{\Phi} \mathcal F

其核心問題是語義選擇與規格化。

14.2 形式精化與編譯驗證

形式方法與 verified compilation 關注規格、原始程式與目標程式之間的語義保存。CompCert 類工作證明編譯器在指定語義下保存程式行為，正顯示「編譯不是透明搬運，而需要明確證明保存條件」。

這對應：

\mathcal F \xrightarrow{\Gamma} \mathcal A \xrightarrow{\Lambda} \mathcal I

14.3 並發正確性

Herlihy 與 Wing 的 linearizability 表明，並發物件的正確性不能只由最終回傳值判斷，還必須考慮可觀察操作歷史與抽象順序。

這說明：

\equiv_F \neq \equiv_O

14.4 科學模型與理想化

科學模型研究指出，模型不是理論或世界的透明複製，而是透過理想化、近似與表示策略建立的中介物。模型會刪除某些性質，也會加入新的操作結構。

這對應：

\mathcal S \not\cong \mathcal F

14.5 科學計算與可重現性

科學計算研究強調，數學模型成為軟體後，測試、版本、資料、依賴與執行環境都會影響科學可靠性。

這對應：

\mathcal I \xrightarrow{\Xi_h} \mathcal E_h

14.6 本文的整合位置

現有研究多半專注於其中一段。本文的目標不是取代這些領域，而是提出一個跨領域統一框架：

\boxed{ \text{語義生成} \rightarrow \text{形式化} \rightarrow \text{演算法化} \rightarrow \text{工程化} \rightarrow \text{環境化執行} }

並以不變量保存與結構誤差作為共同語言。

十五、方法論應用

15.1 數學理論

一個數學猜想可能在自然語義中包含多種直覺，但正式定義只固定其中一種。研究者必須區分：

猜想原意；
正式命題；
證明所使用的附加假設；
計算驗證所覆蓋的有限範圍。

15.2 人工智慧

模型架構論文常從「只關注重要資訊」直接跳到某個稀疏公式，再跳到效能結論。應分別檢查：

重要性的形式定義；
路由器成本；
稀疏資料結構；
kernel 是否真正稀疏；
模型品質是否保存；
實際硬體吞吐。

15.3 科學模擬

物理方程式正確，不表示數值離散、邊界條件與程式實作也正確。應分開：

理論方程；
離散模型；
數值方法；
程式；
硬體誤差；
實驗對照。

15.4 公共政策

政策理念、法條、行政程序、資訊系統與實際執法，也構成類似鏈條：

\text{價值目標} \rightarrow \text{法律文本} \rightarrow \text{行政規則} \rightarrow \text{系統實作} \rightarrow \text{人民經驗}

法律文字符合政策理念，不表示資訊系統與現場執行也會保存同一價值。

15.5 組織管理

組織願景轉為 KPI 時，也會產生形式化壓縮。若 KPI 只保留可測量部分，組織可能最佳化指標而偏離原始目的。

這可表示為：

\operatorname{Optimize}(\Phi(\mathcal S)) \not\Rightarrow \operatorname{Optimize}(\mathcal S)

十六、研究工作流程

本文建議任何跨層研究至少建立以下五份文件。

16.1 語義根文件

記錄：

原始意圖；
尚未決定部分；
禁止被誤解的邊界；
允許的替代形式化。

16.2 形式化決策表

記錄：

採用的變數；
座標；
度量；
假設；
遺失的語義；
新增的形式結構。

16.3 演算法保存表

記錄：

保存的函數關係；
操作順序；
終止性；
複雜度；
近似誤差；
資料存取方式。

16.4 實作偏移表

記錄：

資料結構；
函式庫；
精度；
並行方式；
與理論演算法的差異；
隱性密集化風險。

16.5 執行證書

記錄：

程式版本；
輸入雜湊；
環境；
硬體；
隨機種子；
依賴版本；
輸出摘要；
誤差容限。

十七、可驗證主張與不可提前宣稱事項

17.1 可驗證主張

一項跨層研究可以聲稱：

某不變量在指定映射下被證明保存；
某兩個演算法函數等價；
某實作在測試集合中與參考模型一致；
某環境下的誤差小於指定上界；
某資料結構在指定規模內保持稀疏；
某轉譯失去特定語義資訊。

17.2 不可提前宣稱

在未證明前，不應直接聲稱：

形式模型完整等價於原始概念；
程式就是理論本身；
輸出相同代表運算過程相同；
理論複雜度直接等於實際速度；
單一實作失敗推翻原始概念；
單一實作成功證明原始概念全部正確；
可重現結果等於外部世界真理。

十八、限制

本文是一個整合性方法論，不是所有層級的完整形式理論。

目前限制包括：

「語義生成空間」仍需要更嚴格的形式語義；
不變量選擇本身仍可能具有主觀性；
跨層保真分數如何量化尚未統一；
某些層級可能不是線性鏈，而是循環與共同演化；
機器學習系統可能從執行結果反向修改形式模型；
社會制度中的語義與價值未必能被單一度量描述；
完全驗證整條鏈在大型系統中可能成本過高。

因此，更一般的模型可能是有向圖：

\mathcal G_T = (V_T,E_T)

而不是單一線性鏈。本文先使用線性鏈，是為了建立最小可理解框架。

十九、後續研究方向

19.1 跨層保真度量

建立：

F_i(K_j)\in[0,1]

衡量每個轉譯對特定不變量的保存程度。

19.2 結構誤差分類學

區分：

指稱錯誤；
狀態空間錯誤；
路由錯誤；
終止錯誤；
資料結構錯誤；
複雜度錯誤；
環境錯誤。

19.3 機器可讀轉譯證書

建立跨層證書格式：

source_layer: semantic
target_layer: formal
preserved_invariants:
  - intent
  - causal_direction
lost_information:
  - ambiguity
introduced_assumptions:
  - differentiability
  - scalar_utility
verification:
  status: partial

19.4 AI 輔助形式化

大型模型可協助列出：

原始概念中的隱含語義；
形式化中新增的假設；
不同演算法的資源差異；
程式與公式的偏移；
實驗失敗的層級位置。

但 AI 本身也位於轉譯鏈中，不能被視為透明轉換器。

二十、結論

本文提出：

\boxed{ \mathcal S \xrightarrow{\Phi} \mathcal F \xrightarrow{\Gamma} \mathcal A \xrightarrow{\Lambda} \mathcal I \xrightarrow{\Xi_h} \mathcal E_h }

並主張這些層級之間通常不完全同構。

原始概念是一個可繼續展開的語義生成空間；形式模型是對它的有限切片與假設化；演算法是對形式關係的操作化；程式是對演算法的資料結構與機器化承載；執行則是程式在特定物理與軟體環境中的一次事件。

因此：

\boxed{ \text{概念不是公式，公式不是演算法，演算法不是程式，程式也不是實際執行。} }

但它們也不是彼此斷裂。

更準確的關係是：

\boxed{ \text{它們是連續轉譯、逐層約束、局部保真、假設遞增且通常不可完全逆轉的不同存在層。} }

真正可靠的研究，不應只問「是否正確」，而應問：

哪一層正確；
保存了哪些性質；
遺失了哪些語義；
新增了哪些假設；
錯誤是否改變了結構；
失敗能否向上反證；
結果能否被重播與驗證。

最終，本理論將「一步錯、一步對，天差地遠」轉化為一個可研究的正式命題：

\boxed{ \text{跨層轉譯中的局部選擇，可能改變下一層的世界生成規則。} }

參考文獻

Nuseibeh, B., & Easterbrook, S. (2000). Requirements Engineering: A Roadmap. Proceedings of the Conference on the Future of Software Engineering. DOI: 10.1145/336512.336523.
Herlihy, M. P., & Wing, J. M. (1990). Linearizability: A Correctness Condition for Concurrent Objects. ACM Transactions on Programming Languages and Systems, 12(3), 463–492. DOI: 10.1145/78969.78972.
Wilson, G., Aruliah, D. A., Brown, C. T., et al. (2014). Best Practices for Scientific Computing. PLOS Biology, 12(1), e1001745. DOI: 10.1371/journal.pbio.1001745.
Leroy, X. (2009). Formal Verification of a Realistic Compiler. Communications of the ACM, 52(7), 107–115. DOI: 10.1145/1538788.1538814.
Frigg, R., & Hartmann, S. (2006). Scientific Models. In The Philosophy of Science: An Encyclopedia.
Portides, D. (2007). The Relation Between Idealisation and Approximation in Scientific Model Construction. Science & Education.
Avižienis, A., Laprie, J.-C., Randell, B., & Landwehr, C. (2004). Basic Concepts and Taxonomy of Dependable and Secure Computing. IEEE Transactions on Dependable and Secure Computing, 1(1), 11–33. DOI: 10.1109/TDSC.2004.2.
Mittal, S. (2016). A Survey of Techniques for Approximate Computing. ACM Computing Surveys, 48(4). DOI: 10.1145/2893356.

附錄 A：最小跨層診斷表

問題	檢查內容
原始概念是什麼？	核心意圖、允許展開、禁止誤讀
公式加入了什麼？	座標、尺度、邊界、假設
公式漏掉了什麼？	語境、歧義、替代路徑
演算法如何求值？	操作順序、索引、停止、近似
程式如何承載？	資料結構、中間張量、並行
實際執行依賴什麼？	硬體、函式庫、精度、排程
哪些不變量被保存？	意圖、輸出、順序、資源、血緣
失敗最早出現在哪？	語義、形式、演算法、實作、環境

附錄 B：核心命題濃縮

命題一

\text{形式正確} \not\Rightarrow \text{指稱正確}

命題二

\text{函數等價} \not\Rightarrow \text{操作等價}

命題三

\text{操作等價} \not\Rightarrow \text{資源等價}

命題四

\text{程式一致} \not\Rightarrow \text{執行一致}

命題五

\text{實作失敗} \not\Rightarrow \text{概念失敗}

命題六

\text{多次合理轉譯均失敗} \Rightarrow \text{原始概念需要重新審查}

語義—形式—工程非同構論_跨層轉譯中的不變量保存與結構誤差_v0.1

語義—形式—工程非同構論

跨層轉譯中的不變量保存、結構誤差與實作偏移

摘要

一、問題的提出

二、五層轉譯鏈

三、第一層：原始語義生成空間

3.1 概念不是一句話

3.2 語義展開態根

四、第二層：形式化不是複製，而是選擇

4.1 形式化映射

4.2 有損壓縮

4.3 公式正確不等於指稱正確

五、第三層：從形式模型到演算法

5.1 關係不等於操作

5.2 函數等價與資源非等價

六、第四層：演算法到實作

6.1 實作會加入新的結構

6.2 資料結構不是中性容器

6.3 隱性密集化

七、第五層：程式到實際執行

7.1 執行是物理事件

7.2 理論複雜度與實際性能

八、六類等價關係

8.1 意圖等價

8.2 語義等價

8.3 函數等價

8.4 操作等價

8.5 資源等價

8.6 實證等價

九、語義—形式—工程非同構的五項公理

公理一：層級異質性

公理二：轉譯選擇性

公理三：假設注入

公理四：結構誤差非線性

公理五：正確性向量化

十、結構誤差與誤差放大

10.1 數值誤差

10.2 結構誤差

10.3 複雜度相變

十一、不變量保存

十二、跨層保真矩陣

十三、反向診斷：失敗發生在哪一層

13.1 反例不可直接向上傳遞

13.2 但原始概念不能永久免疫

十四、現有研究如何觸及此問題

14.1 需求工程

14.2 形式精化與編譯驗證

14.3 並發正確性

14.4 科學模型與理想化

14.5 科學計算與可重現性

14.6 本文的整合位置

十五、方法論應用

15.1 數學理論

15.2 人工智慧

15.3 科學模擬

15.4 公共政策

15.5 組織管理

十六、研究工作流程

16.1 語義根文件

16.2 形式化決策表

16.3 演算法保存表

16.4 實作偏移表

16.5 執行證書

十七、可驗證主張與不可提前宣稱事項

17.1 可驗證主張

17.2 不可提前宣稱

十八、限制

十九、後續研究方向

19.1 跨層保真度量

19.2 結構誤差分類學

19.3 機器可讀轉譯證書

19.4 AI 輔助形式化

二十、結論

參考文獻

附錄 A：最小跨層診斷表

附錄 B：核心命題濃縮

命題一

命題二

命題三