有限個の状態と遷移が定義された機械のようなもの

「ある出力をする入力」は無限個ある

キモ: 有限のフォーマリズムであるオートマトンが、無限の数学的集合を表現できる

オートマトンの「ある出力をする入力」の包含関係は、頑張れば証明できる

でも、証明せずに有限の計算機パワーで包含関係を確認してみたい

「ある出力をする入力」は無限個あるから全部確認するのは当然無理

それを有限回の計算で頑張る方法

材料1. 空判定: ある出力をする入力が存在するかどうか (ある出力をする入力の集合が空かどうか)

オートマトンの遷移のグラフを辿っていって、「ある出力」に辿り着くかどうかで有限回の検証が可能

材料2. オートマトンの同期積: 合成関数的な

材料3. 言語反転: 補集合的な

無限の集合Aが無限の集合Bに含まれている <=> notBとAの同期積が空である

だから、同期積が空かどうか判定すれば包含の判定ができる

有限回数でできる空判定で、無限個数の集合の包含関係を確認できるというのがポイント

有限のオートマトンの限界

記憶能力がない

このせいで、実現できない入力-出力関係がある

つまり、「ある出力をする入力の集合」「全入力」とは無限の次元が異なる?

オートマトンに記憶能力を持たせたのがチューリングマシン? (違うかも)