含epsilon的star閉包與完整長度切片

目標與範圍

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去重。

逐步主鏈

R=\operatorname{concat}(\operatorname{star}(\operatorname{union}(\varepsilon,a)),b)

\text{union binary, concat binary, star unary; }a,b\in\Sigma

L(\varepsilon)=\{\varepsilon\},\quad L(a)=\{a\}

K=L(\operatorname{union}(\varepsilon,a))=\{\varepsilon,a\}

S_0=\{\varepsilon\},\quad S_{j+1}=S_j\cup\{uv:u\in S_j,v\in K,|uv|\le3\}

S_1=\{\varepsilon,a\}

S_1=\{\varepsilon,a\}

S_2=\{\varepsilon,a,aa\},\quad S_3=\{\varepsilon,a,aa,aaa\},\quad S_4=S_3

L(R)=K^*\{b\}

L(R)\cap\Sigma^{\le3}=\{b,ab,aab\}

K^*=\{a^m:m\in\mathbb N_0\}

L(R)=\{a^mb:m\in\mathbb N_0\}

w=aaab,\quad |w|=4

w=a^3b\in L(R),\quad w\notin\{b,ab,aab\}

\operatorname{concat}(b,\operatorname{star}(a))

b\{a^m:m\ge0\}\ne\{a^mb:m\ge0\}\quad(ab\text{ witnesses})

局部子步與引理

本稿無局部子步。

逐步反向審查

• 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、反控制與修訂記錄）