『計算理論の基礎 原著第2版』の読書ノート。
方針 実はしばらく前に少し読んだのだが、その時は正規言語の途中までやって放置してしまった。今回改めて読み進めるにあたっての方針として、以下を挙げる。
演習問題はできる限り自力で解く 定理と証明は書き写す 進捗 2021/11/06: 開始 第0章 / 序論 オートマトン、計算可能性、複雑さのついての教科書 計算機の本質的な能力とその限界は何か？ 計算問題には優しい問題と難しい問題がある ソーティング問題 … 優しい スケジューリング問題 … 難しい 何が、問題の難しさ・やさしさを決めているのだろうか？ いまだに明確な答えが得られていない 計算の困難さに基づいて問題を分類するうまい方法の発見 計算が難しいことの証拠を示すことができる 計算が困難な問題の対処 難しさの根源がどこにあるか 難しい部分の変更によって解決 完全な解を諦めることで解決 初期の暗号 問題は難しいものより簡単な方が望ましい 暗号は難しいほうが望ましい 計算可能性の理論 計算機の理論的モデル オートマトン理論 計算の数学的モデル 第1章 / 正規言語 計算のモデル（computational model） 有限オートマトン（finite automaton） Markov連鎖（Markov chain） 有限オートマトンに確率的要素を許す パターンの認識を試みる際に有益 音声処理、光学的文字認識、価格変動のモデル化・予測 有限オートマトンの状態遷移図 開始状態（start state）、受理状態（accept state）、遷移（transition） 入力を処理し、その出力は受理（accept）または拒否（reject）のいずれか一方 有限オートマトンの正式な定義 有限オートマトンは以下の5個のもののリスト 状態の集合 入力アルファベット 動作規則 開始状態 受理状態 動作規則 … $\delta$ で表される遷移関数を用いる オートマトンが状態 $x$ にあって $1$ を読み出したときに状態 $y$ へ移る = $\delta(x, 1) = y$ 定義1.
『情報科学における論理』の演習問題に対する解答です．間違い・誤植など多分に含まれていると思います．ご了承ください．
第一章 命題論理 問 1.1 次の 1), 2) のそれぞれは正しいか．正しいときにはその証明を，正しくないときには反例を与えよ．
$A \supset B$および$A$がともに充足可能ならば，$B$も充足可能である．
$A \supset B$がトートロジーで$A$が充足可能ならば，$B$も充足可能である．
解答 $A \supset B$が充足可能なら，ある付値$v$に対し，$(v(A) = f \lor v(B) = t) = t$となる．よって，問題は次のように言い換えられる．「ある付値$v_1, v_2, v_3$に対し，$(v_1(A) = f \lor v_1(B) = t) \land (v_2(A) = t) \supset v_3(B) = t$が成り立つ」．しかし，例えば$v_1(A) = f$かつ$v_2(A) = t$である場合を考えると，$B$が充足不可能であっても，$(v_1(A) = f \lor v_1(B) = t) \land (v_2(A) = t)=t$が成り立つことがわかる．したがって，反例が見つかったので，1 は正しくない．
問題は次と同値である．「[すべての付値$v$に対し，$(v(A) = f \lor v(B) = t) = t$が成り立ち]，かつ，[ある付値$v$に対し，$v(A) = t$が成り立つ]ならば，ある付値$v$に対し，$v(B) = t$が成り立つ」．ここで，「すべての付値$v$に対し，$(v(A) = f \lor v(B) = t) = t$が成り立つ」なら，すべての$v$について，$v(A) = f$か$v(B) = t$のどちらかが常に成り立っている必要がある（両方成り立たないということはない）．そして，「ある付値$v$に対し，$v(A) = t$が成り立つ」なら，少なくとも一つの$v$について$v(A) = t$である必要がある．この 2 つは両方成り立っている必要があるから，「すべての$v$について，$v(A) = f$か$v(B) = t$のどちらかが常に成り立っている」かつ，「少なくとも一つの$v$について$v(A) = t$である」．よって，少なくとも一つの$v$について$v(A) = f$が成り立たなくなるため，「すべての$v$について，$v(A) = f$か$v(B) = t$のどちらかが常に成り立っている」には，ある$v$について$v(B)=t$が成り立っている必要がある．したがって，$B$は充足可能であるため，2 は正しい．
この記事では、主に型推論の実装方法について書いていきます。 理論的な側面は必要最低限に留めますので、詳しく知りたい方は参考文献を参照してください。
型推論とは何か 型推論とは何かについて軽く説明しておきましょう。
型推論とは、プログラムの変数や引数などの型を、明示的な指定がなくても自動的に推論し、決定する機構のことです。 たとえば、以下のような OCaml プログラムを考えてみましょう。
let f x y = x + y;; このプログラムはxとyを引数として、それらの和を返しています。OCaml の REPL で実行してみると、この関数は引数として整数を 2 つ持ち、整数を返す関数として定義されます。 xとyには何も型を指定していないのに、整数であると決定されるわけです。
val f : int -> int -> int = <fun> このように、型推論は型を周辺状況や文脈などから決定してくれます。
上記の例では、+演算子が左辺と右辺に整数をとり、整数を返す、という情報から関数の型を推論しています。このような単純な型推論は比較的簡単に実装できるでしょう。
今度は少し複雑な例を考えてみましょう。
let a x y z = if x == 2 then y else z(x - 1) この関数は以下の型を持ちます。
val a : int -> 'a -> (int -> 'a) -> 'a = <fun> 整数、任意の型x、引数として整数を持ち、任意の型xを返す関数、これらを引数として、任意の型xを返す関数、という型を持っています。
それぞれの引数について、なぜその型を持つのかについて説明します。
xは整数型を持っています。これは、x == 2の部分から推論されています。==演算子は左辺と右辺に同じ型をとるので、右辺の2と同じ型を持っていなくてはなりません。このことから、xは整数型を持つことがわかります。