# 含epsilon的star閉包與完整長度切片 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-regular-expression/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-regular-expression-01 · ocme-new142-reader-adoption-20261021 ## 目標與範圍 typed AST遞迴語義、完整bounded枚舉與membership責任。 Σ={a,b}；只把長度≤3的清單標成切片。 ## 已知條件與符號 - work - G1 — Σ={a,b}。R=concat(star(union(epsilon,symbol(a))),symbol(b))；empty-language記作∅，epsilon語言為{ε}。 - K — star的子語言 - S_j — bounded closure迭代 ## 規則與來源 - mko_definition · cited — typed AST只允許empty-language、epsilon、alphabet symbol、union、ordered concatenation與star；每個symbol須屬明示alphabet。語義遞迴定義language，star的bounded enumeration以fixed-point closure處理epsilon cycle並extensional dedup。word membership必須完整決定，不因某個不足的bound沒列出就判false。Union canonicalize permutation/idempotence，concatenation保留次序。empty language與{epsilon}、regex與shell wildcard分開；長度≤N語言相同不證全語言等價。 · mko-regular-expression - work · prerequisite — core regex遞迴語義：empty無word，epsilon含空word，union為聯集，concat為ordered word乘積，star為全部有限次concat；bounded closure以set去重。 ## 逐步主鏈 S01 · implies操作前 R=\operatorname{concat}(\operatorname{star}(\operatorname{union}(\varepsilon,a)),b) 操作後 \text{union binary, concat binary, star unary; }a,b\in\Sigma 條件：無 規則：work · 依賴：G1, work 葉節點依據：work 完整驗AST節點型別、arity與alphabet資格。 S02 · implies操作前 L(\varepsilon)=\{\varepsilon\},\quad L(a)=\{a\} 操作後 K=L(\operatorname{union}(\varepsilon,a))=\{\varepsilon,a\} 條件：無 規則：work · 依賴：G1, S01, work 葉節點依據：work union合併語言元素並去重。 S03 · implies操作前 S_0=\{\varepsilon\},\quad S_{j+1}=S_j\cup\{uv:u\in S_j,v\in K,|uv|\le3\} 操作後 S_1=\{\varepsilon,a\} 條件：無 規則：work · 依賴：G1, S02, work 葉節點依據：work bounded star用set固定點closure，乘epsilon不新增元素。 S04 · implies操作前 S_1=\{\varepsilon,a\} 操作後 S_2=\{\varepsilon,a,aa\},\quad S_3=\{\varepsilon,a,aa,aaa\},\quad S_4=S_3 條件：無 規則：work · 依賴：G1, S03, work 葉節點依據：work 完整固定點在第四輪穩定，所有長度≤3的a串都列出。 S05 · implies操作前 L(R)=K^*\{b\} 操作後 L(R)\cap\Sigma^{\le3}=\{b,ab,aab\} 條件：無 規則：work · 依賴：G1, S04, work 葉節點依據：work ordered concat在右附b，僅保留總長度≤3。 S06 · implies操作前 K^*=\{a^m:m\in\mathbb N_0\} 操作後 L(R)=\{a^mb:m\in\mathbb N_0\} 條件：無 規則：work · 依賴：G1, S05, work 葉節點依據：work 任意K因子不是epsilon就是a，故concat只計a個數；反向可用m個a因子。 S07 · implies操作前 w=aaab,\quad |w|=4 操作後 w=a^3b\in L(R),\quad w\notin\{b,ab,aab\} 條件：無 規則：work · 依賴：G1, S06, work 葉節點依據：work 完整membership由語義判true，長度3清單缺席不能判false。 S08 · implies操作前 \operatorname{concat}(b,\operatorname{star}(a)) 操作後 b\{a^m:m\ge0\}\ne\{a^mb:m\ge0\}\quad(ab\text{ witnesses}) 條件：無 規則：work · 依賴：G1, S07, work 葉節點依據：work concat不可交換：ab在R但不在ba*。 ## 局部子步與引理 本稿無局部子步。 ## 逐步反向審查 - S08 · premise_audit · G1, S07, work — union可按排列及idempotence canonicalize，但concat須保序。 - S07 · premise_audit · G1, S06, work — 若用bounded membership，至少用完整長度4 slice。 - S06 · premise_audit · G1, S05, work — 這是雙向全m語義證明，不由bounded清單推無限語言。 - S05 · premise_audit · G1, S04, work — aaab長度4，不在此slice但可在完整language。 - S04 · premise_audit · G1, S03, work — 其他symbol不在K，故不會產生b或混合串。 - S03 · premise_audit · G1, S02, work — 去重使epsilon cycle不產生無限重複。 - S02 · premise_audit · G1, S01, work — empty-language與{epsilon}不同，前者沒有元素。 - S01 · premise_audit · G1, work — star作用在子語言，不是shell任意字串wildcard。 ## 錯誤控制與反例 epsilon去重closure用集合，epsilon乘積不新增副本。 slice標記每個bounded結果標長度上限，不推完整等價。 - ∅與{ε}相同。 → reject — 後者有一元素空word，前者無元素。 - aaab沒在長度3清單故非member。 → reject — aaab=a³b，符合完整語義且長度4超出slice。 - concat可交換左右。 → reject — ab在a*b但不在ba*。 ## 結論與限制 完整語言為{a^m b:m≥0}；長度≤3切片為{b,ab,aab}，aaab仍是member。 ## 驗證及來源綁定 2 個本稿宣告算術檢查；只支持所列算式。 - source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f - adopted source SHA-256: 477a3a7c717c0ddf0f6208cbbf27ebde9d4743b8722ed272a842db0e6b108780 - original source SHA-256: 477a3a7c717c0ddf0f6208cbbf27ebde9d4743b8722ed272a842db0e6b108780 - Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-regular-expression-01.json)