# 語義—形式—工程非同構論 ## 跨層轉譯中的不變量保存、結構誤差與實作偏移 **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 } $$ 這裡的「非同構」不是指它們毫無對應關係，而是指通常不存在同時滿足以下條件的雙向映射： 1. 一一對應； 2. 完全可逆； 3. 保存全部結構； 4. 保存全部語義； 5. 保存全部資源性質； 6. 保存全部可觀察行為。 大多數實際轉譯只保存其中部分。 --- # 三、第一層：原始語義生成空間 ## 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) $$ 這表示形式空間也可能比原始概念切片更大。 因此形式化同時具有兩種作用： 1. **語義壓縮**：刪除或合併部分原始差異； 2. **形式新增**：加入尺度、邊界、排序與可計算假設。 ## 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 $$ 演算法甲可能： 1. 枚舉所有 $(i,j)$ ； 2. 判斷 $j\in N(i)$ ； 3. 丟棄不需要的項。 成本： $$ O(n^2) $$ 演算法乙可能： 1. 直接讀取鄰接表； 2. 只枚舉有效邊； 3. 只計算存在的關係。 成本： $$ 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 但原始概念不能永久免疫 反過來，也不能將所有失敗都歸因於「只是實作問題」。 應使用以下診斷程序： 1. 確認失敗的可觀察現象； 2. 找出違反了哪個不變量； 3. 定位最早發生違反的轉譯； 4. 檢查是否為形式化選擇、演算法、資料結構或環境問題； 5. 嘗試至少一種替代轉譯； 6. 若多種合理轉譯均反覆失敗，再回頭質疑原始概念。 可寫為： $$ 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 不可提前宣稱 在未證明前，不應直接聲稱： - 形式模型完整等價於原始概念； - 程式就是理論本身； - 輸出相同代表運算過程相同； - 理論複雜度直接等於實際速度； - 單一實作失敗推翻原始概念； - 單一實作成功證明原始概念全部正確； - 可重現結果等於外部世界真理。 --- # 十八、限制 本文是一個整合性方法論，不是所有層級的完整形式理論。 目前限制包括： 1. 「語義生成空間」仍需要更嚴格的形式語義； 2. 不變量選擇本身仍可能具有主觀性； 3. 跨層保真分數如何量化尚未統一； 4. 某些層級可能不是線性鏈，而是循環與共同演化； 5. 機器學習系統可能從執行結果反向修改形式模型； 6. 社會制度中的語義與價值未必能被單一度量描述； 7. 完全驗證整條鏈在大型系統中可能成本過高。 因此，更一般的模型可能是有向圖： $$ \mathcal G_T = (V_T,E_T) $$ 而不是單一線性鏈。本文先使用線性鏈，是為了建立最小可理解框架。 --- # 十九、後續研究方向 ## 19.1 跨層保真度量 建立： $$ F_i(K_j)\in[0,1] $$ 衡量每個轉譯對特定不變量的保存程度。 ## 19.2 結構誤差分類學 區分： - 指稱錯誤； - 狀態空間錯誤； - 路由錯誤； - 終止錯誤； - 資料結構錯誤； - 複雜度錯誤； - 環境錯誤。 ## 19.3 機器可讀轉譯證書 建立跨層證書格式： ```yaml 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{它們是連續轉譯、逐層約束、局部保真、假設遞增且通常不可完全逆轉的不同存在層。} } $$ 真正可靠的研究，不應只問「是否正確」，而應問： 1. 哪一層正確； 2. 保存了哪些性質； 3. 遺失了哪些語義； 4. 新增了哪些假設； 5. 錯誤是否改變了結構； 6. 失敗能否向上反證； 7. 結果能否被重播與驗證。 最終，本理論將「一步錯、一步對，天差地遠」轉化為一個可研究的正式命題： $$ \boxed{ \text{跨層轉譯中的局部選擇，可能改變下一層的世界生成規則。} } $$ --- # 參考文獻 1. Nuseibeh, B., & Easterbrook, S. (2000). Requirements Engineering: A Roadmap. *Proceedings of the Conference on the Future of Software Engineering*. DOI: 10.1145/336512.336523. 2. 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. 3. 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. 4. Leroy, X. (2009). Formal Verification of a Realistic Compiler. *Communications of the ACM*, 52(7), 107–115. DOI: 10.1145/1538788.1538814. 5. Frigg, R., & Hartmann, S. (2006). Scientific Models. In *The Philosophy of Science: An Encyclopedia*. 6. Portides, D. (2007). The Relation Between Idealisation and Approximation in Scientific Model Construction. *Science & Education*. 7. 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. 8. 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{原始概念需要重新審查} $$