正規言語とPumping Lemma

Pumping Lemma 自体は、Agda でだいぶ昔に証明したんですけどね、

　　0{n}1{n}

つまり、n 個の0とn個の1ってのは、正規言語じゃない、正規表現で書けないってのがなんか難しくって。

カッコの対応なので stack 使えば良いだけだが。授業中に書き始めて、これは難しいとなった記憶がある。

その残骸が残ってたわけですが、それは書き方が悪いな。生成器と検査器を書くんだが、

　　それが並行するように書くんだよ

片方再帰で片方ループとかだめだろ。ってわけでうっかり書き始めて一応書けたんだが複雑すぎる。

0と1の個数が同じってのが x ++ y ++ z と x ++ y ++ y ++ z とで両方成立するからとかやってる。

でも、書き終わったあとに簡単なのを思いつくのはよくある。

　　だから、検査を通るなら、unique に生成器と同じ

ってのを示せば、いろいろ証明しないで、x ++ y ++ z と x ++ y ++ y ++ z とを生成器と一緒に走らせればいいじゃん。

でも、そこそこ面倒で本質的には変わらないらしい。uniquenessを使うのは圏論っぽくっていいかな。

pumpling lemma は Berstein と似てるところもある。この辺の復習は面白い。