計算可能性とチューリングマシン
「計算とは何か」を抽象機械で定式化し、判定問題の解法と難しさを論じる分野。論理と代数的手法(有限体上のグレブナー基底)に橋を架ける。
チューリングマシン
アラン・チューリングが計算可能性のために考案した抽象機械 (1936)。両方向無限のテープ・ヘッダ・制御器からなり、形式的には
で与えられる。状態遷移図で動作を表現でき、あらゆる「計算」を TM の動作に還元できる(万能性)。
神託機械
特定の決定問題を 1 ステップで答えるブラックボックス(オラクル)を付けた TM が神託機械。停止性問題を解くオラクルを仮定することもでき、多項式階層の議論に繋がる。無作為に一貫した値を返すランダムオラクルは理想的な一方向関数として暗号の安全性証明(ランダムオラクル仮定)で使われる。
充足可能性ソルバ
- SAT:ブール式の充足可能性問題。現代のソルバは DPLL を基礎にする。
- SMT(Satisfiability Modulo Theories):値がブールでなくなった拡張。SAT が命題論理、SMT が一階述語論理に対応。Microsoft z3 が有名(Julia バインディングあり)。充足判定を二分探索すれば最適化問題が解ける。
代数的・組合せ的手法
- グレブナー基底(Buchberger アルゴリズム):多値論理を多項式で表して判断推理を解いたり、有限体 上の算術回路の形式検証(等価性判定)に使われる。逆トポロジカル順序での基底導出でバグを含む回路でも検証を完了できる、という論文がある。
- Schwartz–Zippel の補題:誤った多項式はランダム評価点で高確率に異なる値を返す(恒等性検査の基礎)。
- Chordal Graph(弦グラフ、木の同型判定)、マトロイド、有限体上の行列簡約の計算量など組合せ最適化の話題。
関連: mathematical-logic / abstract-algebra / np-complexity-classes / _moc-cs
オートマトンと形式言語
計算モデルを表現力の階層で整理する計算理論の基礎。受理する文字列の集合をそのオートマトンの言語と呼ぶ。
有限オートマトン (FA)
状態遷移図で表される最も単純なモデル。DFA (状態・入力アルファベット・開始状態・受理状態・遷移関数)。遷移先が一意なら DFA、そうでなければ NFAだが、NFA は必ず DFA に変換でき表現力は同じ。受理できる言語が正規表現。限界として は受理できない。
プッシュダウンオートマトン (PDA)
有限オートマトンにスタックを付けて履歴を記憶できるようにしたもの。 を受理でき、FA より表現力が高い。PDA で受理できる言語が**文脈自由文法 (CFG)**(生成規則で定義、いわゆる構文解析の対象)。限界として は受理できない。
チューリングマシンと決定不能性
- 万能チューリングマシン: 別の TM の記述をテープ入力として受け取り、その動作をエミュレートする TM。
- 停止性問題: 任意の TM が停止するか判定する TM は作れない(決定不能)。ゲーデルの不完全性定理(証明も反証もできない命題の存在)や連続体仮説とも関連する。
関連
- 構文解析は言語処理系、計算モデルとしてはλ計算と等価。
- _moc-lang-compilers