概要と対象読者

本単元は、形式言語と計算モデルを定式化し、有限オートマトン、文脈自由言語、Turing 機械、型なしラムダ計算を比較する。決定不能性、時間・空間計算量、P・NP、NP 完全性、計算量の階層定理を扱い、確率的計算、対話型証明、回路計算量、量子計算モデルへ進む。

量化を含む論証と離散的な構成を読み書きすることができ、計算可能性と計算資源の限界を定義と証明に基づいて学びたい数学専門課程の読者を対象とする。

到達像

必修の記事を学んだ読者は、次の事柄を実行することができる。

  • 有限オートマトン、正規表現、文脈自由文法、pushdown automaton、Turing 機械を定義し、それぞれの表現力に関する同値定理を証明することができる。
  • Myhill–Nerode の定理、正規言語と文脈自由言語のポンピング補題を証明し、与えられた言語が正規でないこと、または文脈自由でないことを証明することができる。
  • Rice の定理を証明し、認識可能言語の非自明な意味的性質が決定不能であることを示すことができる。
  • 決定可能性、認識可能性、停止問題、計算可能帰着を区別し、対角線論法と帰着によって決定不能性を証明することができる。
  • 原始再帰関数、部分ミュー再帰関数、型なしラムダ計算を定義し、Turing 計算可能性との同値性を証明することができる。
  • 時間計算量と空間計算量、P、NP、co-NP、多項式時間帰着を定義し、Cook–Levin の定理を計算履歴の符号化から証明することができる。
  • 対数空間クラス L、多項式空間クラス PSPACE、非決定性空間計算量クラスを定義し、時間と空間の包含関係、階層定理、および Savitch の定理を証明することができる。

展望の記事を選んで学んだ読者は、確率的計算、対話型証明、回路計算、量子計算について、計算モデルと資源制約を比較することができる。

区分

必修は、有限オートマトンと文脈自由言語から Turing 機械、計算可能関数、型なしラムダ計算へ進む。停止問題と帰着、Rice の定理、時間・空間計算量、P・NP、co-NP、Cook–Levin の定理、階層定理と Savitch の定理を扱う。13記事すべてを単元の修了に必要な内容とする。

展望は、確率的計算量、対話型証明、回路計算量、量子計算モデルを扱う。必修ではなく、関心に応じて選んで読むことができる。

前提知識

必修区分は、離散数学とアルゴリズムの必修と集合と論理の発展を前提とする。帰納的定義、離散構造、量化を含む命題、必要条件と十分条件、背理法を用いる。

記事ごとの前提は、使用する箇所に合わせて次のように定める。

学習の順序と理由

必修の13記事では、有限オートマトンから正規言語と文脈自由言語へ進み、その後に Turing 機械を導入する。Turing 機械を定義した後で、停止問題、帰着、計算可能関数を扱う。この順序により、機械、言語、関数という三つの見方を区別しながら計算可能性を比較することができる。

型なしラムダ計算は、構文と簡約を独立に定義した後、Turing 機械との相互模倣を証明する。続いて時間と空間を資源として測り、対数空間クラス L と多項式空間クラス PSPACE を定義してから、P、NP、多項式時間帰着、NP 完全性へ進む。Cook–Levin の定理では、SAT、Boolean 論理式、連言標準形を記事内で定義するため、後続の数理論理を前提としない。

必修の最後に計算量階層定理を置く。時間計算量と空間計算量の記事が定める資源上界の構成可能性と、空間を制限した配置の個数の評価をそのまま用いて、決定性時間階層定理と決定性空間階層定理を証明する。同じ記事で非決定性空間計算量クラスを定義し、非決定性の空間上界を二乗の決定性空間上界へ移すことができることを Savitch の定理として証明する。資源上限を真に増やしたときに、より多くの言語を決定することができるという結論は、P と NP の関係が未解決であることとは独立に証明することができるため、必修に含める。

展望の4記事は必修ではない。時間計算量と空間計算量を出発点として、確率的計算、対話型証明、回路計算量、量子計算モデルへ進む。後続単元が展望の記事を用いる場合は、必要な記事だけを選んで読む。

各記事の内容

次の一覧は学習順に並んでいる。第1項から第13項までが必修であり、第14項から第17項までが任意の展望である。「公開中」は、読者ページで本文を読むことができる記事を表す。

  1. 有限オートマトン（公開中）形式言語、決定性有限オートマトン、非決定性有限オートマトン、空語遷移を定義する。部分集合構成と空語遷移の除去によって、三つの計算モデルが同じ言語を認識することを証明する。積構成によって、DFA の受理言語が共通部分と差について閉じていることを証明する。前提は帰納法と再帰的な定義である。
  2. 正規言語（公開中）正規表現と正規言語を定義し、両方向の構成を分けて Kleene の定理を証明する。Nerode 同値関係を定義し、言語が正規であることと指数が有限であることの同値性を Myhill–Nerode の定理として証明する。正規言語のポンピング補題も証明し、a の並びの後に同数の b が続く言語が正規でないことを証明する。前提は有限オートマトンである。
  3. 文脈自由言語（公開中）文脈自由文法、導出、導出木、pushdown automaton を定義し、両方向の構成を分けて表現力の一致を証明する。右線形文法の構成によって正規言語が文脈自由言語であることを示す。導出木の高さと成果（yield）の長さの関係からポンピング補題を証明し、a, b, c をこの順に同数ずつ並べた語からなる言語が文脈自由でないことを証明する。前提は有限オートマトンと帰納法と再帰的な定義である。
  4. Turing 機械（公開中） Turing 機械、配置、計算、受理、停止を形式化する。多テープ決定性機械と非決定性機械を単テープ決定性機械で模倣し、認識可能言語と決定可能言語のクラスが変わらないことを証明する。列挙器が列挙する言語と Turing 機械が認識する言語の一致は、機械間の模倣とは別の対応として証明する。有限オートマトンを必須の前提とし、アルゴリズムの正当性と計算量を補助的に参照する。
  5. 決定可能性と停止問題（公開中）決定可能な言語、認識可能な言語、余認識可能な言語を区別し、認識可能性と余認識可能性を同時に満たすことが決定可能性と同値であることを証明する。対角線論法によって停止問題の決定不能性を証明する。前提はTuring 機械である。
  6. 計算可能帰着（公開中） many-one 帰着を計算可能関数によって定義し、決定可能性と認識可能性が帰着に沿ってどちらの向きへ保存されるかを証明する。停止問題から具体的な問題へ帰着を構成して、決定不能性を導く。認識可能言語の非自明な意味的性質が決定不能であることを Rice の定理として証明し、個別の決定不能性がその特別な場合であることを示す。前提は決定可能性と停止問題である。
  7. 計算可能関数（公開中）初期関数、合成、原始再帰によって原始再帰関数を定義し、最小化を加えて部分ミュー再帰関数を定義する。部分ミュー再帰関数と部分 Turing 計算可能関数が一致することを証明し、原始再帰関数が全域 Turing 計算可能関数の真部分クラスであることを明示する。数学的な同値定理と Church–Turing の提唱を区別する。前提はTuring 機械と帰納法と再帰的な定義である。
  8. 型なしラムダ計算（公開中）型なしラムダ項、自由変数、束縛変数、アルファ変換、変数捕獲を避ける代入、ベータ簡約、正規形を定義する。Church–Rosser の定理を証明し、正規形が存在する場合の一意性と、簡約列が停止しない項の存在を区別する。前提は帰納法と再帰的な定義である。
  9. ラムダ計算と Turing 機械の同値性（公開中）ラムダ項による自然数と計算の符号化を定め、型なしラムダ計算で Turing 機械の計算を模倣する。逆向きの模倣も構成し、ラムダ計算可能性と Turing 計算可能性が一致することを証明する。前提は型なしラムダ計算、Turing 機械、計算可能関数である。
  10. 時間計算量と空間計算量（公開中）決定性 Turing 機械の時間計算量と空間計算量を入力長の関数として定義し、漸近的な上界によって計算量クラスを定める。時間・空間構成可能性と、計算モデルの変更に対する多項式時間の不変性を証明する。対数空間クラス L と多項式空間クラス PSPACE を定義し、時間と空間の基本的な包含関係を証明する。前提はTuring 機械である。
  11. P と NP（公開中） NP、多項式時間 many-one 帰着、補言語のクラス co-NP を定義する。P は前記事の定義を用いる。非決定性 Turing 機械による定義と、多項式長の証明書を決定性 Turing 機械が多項式時間で検証するという定義が同値であることを証明する。前提は時間計算量と空間計算量と計算可能帰着である。
  12. NP 完全性と Cook–Levin の定理（公開中）充足可能性問題 SAT、Boolean 論理式、連言標準形を本記事で定義し、SAT が NP に属することを示す。非決定性 Turing 機械の計算履歴を連言標準形の論理式へ符号化し、Cook–Levin の定理を証明する。前提はP と NPである。
  13. 計算量階層定理（公開中）時間・空間構成可能な上界を仮定し、対角線論法によって決定性時間階層定理と決定性空間階層定理を証明する。資源上限を真に増やしたときに、より多くの言語を決定することができるという結論の条件を明示する。非決定性空間計算量クラスを定義し、Savitch の定理を証明する。時間計算量と空間計算量を必須の前提とし、決定可能性と停止問題の対角線論法を必要に応じて補助的に参照する。
  14. 確率的計算量（公開中、展望）確率的 Turing 機械と受理確率を定義し、RP、coRP、ZPP、BPP を片側誤りと両側誤りによって区別する。独立な反復による誤り確率の減少を証明し、乱択アルゴリズムと計算量クラスを区別する。時間計算量と空間計算量を必須の前提とし、有限等確率空間の導入と復習のために確率の定義と「同様に確からしい」を必要に応じて補助的に参照する。
  15. 対話型証明（公開中、展望）計算能力に制限を課さない prover と確率的多項式時間の verifier の相互作用を定義し、完全性と健全性を確率の量化を含めて定める。代表的なプロトコルについて、正しい入力と誤った入力の受理確率を解析する。確率的 Turing 機械と受理確率の導入として、確率的計算量を必要に応じて補助的に参照する。
  16. 回路計算量（公開中、展望） Boolean 回路、回路族、一様性、サイズ、深さを定義する。多項式サイズの回路族と一様な多項式時間計算の関係を示し、回路下界を証明するために区別しなければならない条件を整理する。前提は時間計算量と空間計算量である。
  17. 量子計算モデル（公開中、展望）量子ビット、テンソル積、ユニタリ回路、測定、BQP を定義する。量子回路における状態の変化と測定結果の確率を計算し、決定性計算および確率的計算との違いを比較する。前提は回路計算量、実・複素内積空間、確率空間と確率モデルである。

証明責任と評価

必修の記事は、定義だけを列挙せず、表現力の同値、表現力の限界、決定不能性、計算モデル間の同値、計算量クラスの特徴づけ、Cook–Levin の定理、階層定理と Savitch の定理までの証明を本単元で完結させる。展望の記事も、記事の守備範囲で主要定理を述べる場合は、その仮定と証明を示す。対話型証明と量子計算モデルでは、定義と計算例を中心に、モデル間の比較を行う。

評価では、定義の再現だけでなく、オートマトンや模倣機械の構成、帰着の向きの判定、計算履歴の符号化、計算量の上界の証明を求める。展望では、確率の量化、回路の一様性、量子測定の確率を明示して比較することを求める。

記事の執筆に先立ち、各記事が用いる必須の前提が公開済みで、必要な定理を完全に証明しているかを確認する。参照先が概説に留まる場合は、本論の根拠に用いず、先に参照先を完全化するか、当該記事内で必要な限定形を証明する。

本単元が扱う範囲と扱わない範囲

  • Robinson 算術 Q、Peano 算術 PA、構文の算術化、算術における表現可能性、対角線補題、不完全性定理、Church の定理、単純型付きラムダ計算、限定した Curry–Howard 対応は扱わない。これらは数理論理が扱う。
  • 自然演繹の正規化、シークエント計算のカット除去、単純型付きラムダ計算の強正規化、証明論的順序数は扱わない。これらは証明論が扱う。
  • 初等部分構造、量化子消去、型、飽和性、圏別性、安定性理論、有限モデル理論、記述計算量は扱わない。これらはモデル理論が扱う。

前後の単元との関係

離散数学とアルゴリズムと集合と論理は、本単元で用いる離散的構成と量化を含む論証を供給する。後続の数理論理は、本単元の計算可能関数、計算可能帰着、型なしラムダ計算を、それぞれ構文の算術化と表現可能性、Church の定理、単純型付きラムダ計算の前提として用いる。モデル理論は、本単元の P と NP および Cook–Levin の定理を、有限モデル理論と記述計算量の接点で参照する。