# 抽象計算模型

有限狀態計算模型以狀態集、初始狀態集、步驟關係與停止狀態集描述可能執行。

mko-computational-model · definition · v0.10.0



## 數學敘述

本條目的有限抽象模型為 (S,Init,Step,Halt)，其中 Init,Halt⊆S、Step⊆S×S。執行從 Init 中狀態開始並沿 Step 前進；無後繼的 stuck 狀態不因而自動屬於 Halt。





## 代表公式（精確 TeX）

R\subseteq S





## 成立條件


- S 是明示有限狀態集，Step 是有向關係，可具 nondeterminism。
- 到達 Halt 後本模型視為停止，不再沿其外出邊；若資料含外出邊仍在分析前截斷。





## 符號作用域


- R — 步驟關係
- S — 狀態集合





## 直觀、定義與常見誤解

可達性從全部初始狀態出發，沿 Step 的零步或多步閉包計算。

合法 trace 必須首狀態在 Init、相鄰狀態成 Step；一旦進入 Halt 就結束，不能在同一執行繼續。

有限深度沒有看到循環不代表所有執行終止；reachable 非停止 cycle 或 reachable stuck 非停止狀態都是終止性風險。

把無外出邊自動叫做 halt，或以有限 execution prefix 斷言所有執行終止。





## 已採用的推導導讀

[抽象計算模型：在七狀態模型中截斷停止邊、計算可達集並區分停止、卡住與不終止](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-computational-model-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識


- [集合](https://ocme.evemisslab.com/zh-Hant/mko/mko-set/) — 狀態、初始與停止條件用集合表示。
- [二元關係與集合投影](https://ocme.evemisslab.com/zh-Hant/mko/mko-relation/) — 步驟語義是狀態間有向關係。
- [自然數](https://ocme.evemisslab.com/zh-Hant/mko/mko-natural-number/) — 有限 trace 長度與步數由自然數索引。





## 驗證界線

有限狀態圖可以完整枚舉可達結構；不外推未指定的 Turing 完備性或實際程式行為。

not_formalized

這不表示內容錯誤；只表示尚未登錄可重播的計算或形式證據。





## 下一個義務

建立 deterministic／nondeterministic、stuck、maximal execution 與有效編碼的分層模型。





## 同源結構化資料

本頁與互動版共用同一個物件與既有語言 edition；未新增證明或人工審定。

[原始 MKO JSON](https://ocme.evemisslab.com/data/mko/computational-model.json) · [純文字 Markdown](https://ocme.evemisslab.com/zh-Hant/mko/mko-computational-model/index.md)