問題タブ [language-theory]

言語 a^nb^2n が 100 => n <= 0 のように有限である場合に限り、どのようにして正規である可能性がありますか?

n=>0 のとき ( a^nb^n ) のような形式の言語は規則的ではないことを私は知っています。これは、a と b の数を追跡するために一時メモリが必要であり、すべての有限言語が規則的であることを知っています。正規ですが、同様の形式の有限言語を正規にする理由がわかりませんか? どのように証明できますか？手がかりが必要です。同等の正規表現を取得できることに加えて、より詳細な説明が必要です..

ありがとう

私は Coq に少し慣れていないので、Coq 内の通常の文法を形式化しようとしています。次のような誘導型があるとします。

(a* b*)文法の派生規則を表します。後で使用するためにそれらを抽出したいとしましょう。これを実行してリストのリストに保存する方法はありますか? たとえば、私は私を返す手続きが欲しい[[S [inr a; inl S];S [inr b;inl S];[]]. 他のアイデアをいただければ幸いです。

前もって感謝します。