pumping lemma

Automaton の最初の方で出てくる定理ですね。正規(最近は正則って言うらしい)言語でない言語があるのを証明するのに使います。

かっこの対応をとるのは正規言語じゃないっていう定理なだけだが、補題の方が応用が効くので便利なことが多い。Agda では

trace-xyz : Trace fa (x ++ y ++ z) q
trace-xyyz : Trace fa (x ++ y ++ y ++ z) q

とか書くらしい。途中の状態が重なればそうなる。Trace は automaton fa が受理するのを表すデータ構造、あるいは、そういう性質。

証明自体は簡単なんですが、その簡単な証明を Agda で書くのは別問題。

なんで、年末年始にそんなことしたのはかは割と謎なんですが、授業で使うには複雑すぎる。まぁ、いろんな証明の例題の一つか。

複雑なのは証明の方なので、命題だけをみせて、証明は概略だけとかかな。いや、

　　神は detail に宿る

でしょ。いろいろ Agda の技術がみれて面白かったです。自分で書いていくというよりは降ってくる、あるいは、Agda を使って発掘してく感じ。

count 使う方が簡単ならしい。