# CFG的完整production與推導witness [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-context-free-grammar/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-context-free-grammar-01 · ocme-new142-reader-adoption-20261021 ## 目標與範圍 grammar S→aSb或ε具有aaabbb與ε的有限推導witness。 grammar合法性與指定word membership分開，不宣稱regularity或CFG-PDA等價。 ## 已知條件與符號 - calc - G1 — N={S}，Σ={a,b}，start S；完整production P={S→aSb,S→ε}；ε為空rhs。 - N,\Sigma — nonterminal與terminal集合 - P — 完整production集合 ## 規則與來源 - calc · prerequisite — 假設有限集合、有限字串與索引、逐步函數更新及自然數歸納；ε表示長度0字串。 - mko_definition · cited — rhs為terminal/nonterminal finite strings並明示epsilon convention。derivation是finite production sequence；language只含start導出的terminal-only words。空語言不等於含epsilon。witness證membership，但bounded search failure不證nonmembership，亦不自動推unambiguous、regular或PDA equivalence。 · mko-context-free-grammar ## 逐步主鏈 S01 · implies操作前 N=\{S\},\quad\Sigma=\{a,b\} 操作後 N\cap\Sigma=\varnothing,\quad S\in N 條件：無 規則：calc · 依賴：G1 葉節點依據：calc 兩alphabet有限、元素互異且不交，start確為nonterminal。 S02 · implies操作前 P=\{S\to aSb,\ S\to\varepsilon\} 操作後 \text{each lhs is one nonterminal; every rhs symbol is legal} 條件：無 規則：calc · 依賴：G1, S01 葉節點依據：calc 兩條lhs皆單一S；aSb只用合法symbols，ε是長度0而非新字元。 S03 · implies操作前 S 操作後 aSb 條件：無 規則：calc · 依賴：G1, S02 葉節點依據：calc 對start套S→aSb，第一步保留一個S。 S04 · implies操作前 aSb 操作後 aaSbb 條件：無 規則：calc · 依賴：G1, S02, S03 葉節點依據：calc 只替換中間S，以外的a、b保持順序。 S05 · implies操作前 aaSbb 操作後 aaaSbbb 條件：無 規則：calc · 依賴：G1, S02, S04 葉節點依據：calc 再用同一production產生第三對a、b。 S06 · implies操作前 aaaSbbb 操作後 aaabbb 條件：無 規則：calc · 依賴：G1, S02, S05 葉節點依據：calc 使用S→ε刪去唯一S，不消除或重排terminal。 S07 · implies操作前 S\Rightarrow aSb\Rightarrow aaSbb\Rightarrow aaaSbbb\Rightarrow aaabbb 操作後 aaabbb\in L(G) 條件：無 規則：mko_definition · 依賴：G1, S03, S04, S05, S06 葉節點依據：mko_definition 四步有限合法production序列結束於純terminal字，認證membership。 S08 · implies操作前 S\Rightarrow\varepsilon 操作後 \varepsilon\in L(G),\quad L(G)\ne\varnothing 條件：無 規則：calc · 依賴：G1, S02, S07 葉節點依據：calc 直接空production亦給有限witness；含空字的language不是空language。 S09 · implies操作前 \text{search depth }2 操作後 aaabbb\text{ not found by depth 2, but has the depth-4 witness above} 條件：無 規則：calc · 依賴：G1, S03, S04, S05, S06, S07 葉節點依據：calc 深度不足的搜尋未命中不證非membership，這裡已有確切反例。 ## 局部子步與引理 本稿無局部子步。 ## 逐步反向審查 - S09 · premise_audit · G1, S03, S04, S05, S06, S07 — 只有本grammar的完整witness足以接受，不借CFG-PDA等價。 - S08 · premise_audit · G1, S02, S07 — ε是集合的一個元素，∅則沒有元素。 - S07 · premise_audit · G1, S03, S04, S05, S06 — 此witness只證這個word，未自動證grammar無歧義。 - S06 · premise_audit · G1, S02, S05 — ε替換長度0，因此不輸出字母epsilon。 - S05 · premise_audit · G1, S02, S04 — 每步lhs是實際存在的單一S，沒有跳步換整個word。 - S04 · premise_audit · G1, S02, S03 — 不能同時把前面的terminal a改成S。 - S03 · premise_audit · G1, S02 — 此時仍有nonterminal，尚非terminal-only結束。 - S02 · premise_audit · G1, S01 — grammar資格不等於任意word都可導出。 - S01 · premise_audit · G1 — S不是terminal，含S的中途字不是language member。 ## 錯誤控制與反例 終點純terminal中途含S的sentential form不算接受word。 production位置每步只替換合法lhs出現處，保持其他symbols順序。 - aaSbb已是language中的terminal word。 → reject — 它仍含nonterminal S。 - 因可導出ε，language是空集。 → reject — ε本身已是一個元素，且aaabbb亦在內。 - depth2未命中aaabbb證拒絕。 → reject — 上面depth4完整推導認證membership。 ## 結論與限制 grammar S→aSb或ε具有aaabbb與ε的有限推導witness。 ## 驗證及來源綁定 0 個本稿宣告算術檢查；只支持所列算式。 - source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f - adopted source SHA-256: a8dca2b816c0c085ecbc6756e9970e00e0953a31ba8d0a4e35d497a9265aa220 - original source SHA-256: a8dca2b816c0c085ecbc6756e9970e00e0953a31ba8d0a4e35d497a9265aa220 - Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-context-free-grammar-01.json)