渡辺治著

Pascalとか余裕で知ってるっしょ？の感じでPascal用語が出てくる🤬

帰納的関数論を現代プログラミング風言語を用いてアプローチする本

個人的には逆にわかりにくい

ストレートに帰納的関数論を読んだほうがマシな気もする

いずれにせよ、何らかの帰納的関数論の本と併読するかそちらを先に読み終えるかなどしたほうが良いような気もする

この本特有の用語がやたら出てくるのはあまり好きではない

1章 問題とアルゴリズム

この本特有の用語

f(a_1,a_2,\cdots,a_n)=\bot: 関数の適用結果が未定義であることを示す

計算とは、の2理論

手に負えない問題

そもそも計算の構成の仕方がわからない、マジで無理

未解決問題など

その問題を解くプログラム自体が存在しない

総当りすれば解けるとは思うが、それは現実的な時間ではない

入力のサイズに対して解の候補数が指数関数的に増加する

多項式時間内で解くプログラムが存在しない

p.9

本書内で扱う用語や記号の定義など

Pascal風コードの非直感的な箇所

right(x) は、Haskellでいう tail

tail(x) は、Haskellでいう last

left(x) は、Haskellでいう init

2章 計算可能性入門

この本特有の記号のメモ

\Sigma: \{0,1\}

\Sigma^*: \Sigma上の文字列型

[n]:nの2進数表記。 [ ではなく下が開いているもの

\overline{n}: nの1進数表記

われわれのコード化法: データを\Sigma^*で表現すること

xのコード: 元のデータxを\Sigma^*で表現したもの

標準形プログラム

以下で構成されるプログラム

データは文字列の 0,1 のみ

演算は文字列型の基本演算

制御構造は if 、 while のみ

isProgram

各a\in\Sigma^*に対し

isProgram(a) とは、「 a は1入力の文法的に正しい標準形プログラムのコードである」ことを表す

コンパイラにおける構文解析のイメージ

eval

各a,x\in\Sigma^*に対し

eval(a,x) とは、

isProgram(a) なら f_a(x)

それ以外ならエラー

f_a(x) は、「「コード a が表すプログラム」が計算する関数」

コード a は高級言語でプログラムを書いている感じ

f_a は↑を実際に処理系が解釈したもの

[a] と同じ意味

それが x を入力に実際に実行されている感じ

インタプリタのようなもの

構文解析を通過した場合は f_a(x) が計算される

Halt

各a,x\in\Sigma^*に対し

\mathrm{Halt}(a,x)とは、

isProgram(a) かつ、

入力 x に対し [a] が停止すること

Haltは計算不可能

結局、parser, eval付きの処理系が停止するかどうかの話をイメージすればいいのね

tally

2進数を引数に取り、その長さの1の列を返す

ex. tally 100 = 1111

帰納的関数論の研究分野の4つの大別

hugeの定義合ってる？

huge 1 x = 2^x ってま？

対角線論法を使って計算不可能性を示す

対角線論法を用いた証明

計算可能な1引数の関数全体の集合をF_1とする

計算の基本要素を考えれば、任意のプログラムのコードは 0 、 1 の並びで全て表現できる

形式的に言うなら、「\Sigma=\{0,1\}があるときに、任意のプログラムのコードは\Sigma^*の元になる」

例えば 100011 とか 1 とかがプログラムのコードとして解釈可能

なのでこれらのプログラムを(2進数的に見て)小さいものから並べて、a_1,a_2,\cdots,a_k,\cdotsと並べることができる

この順番に従うことでF_1の元である関数をf_{a_1},\cdots,f_{a_k},\cdotsと並べることができる

f_{a_1}ってなに #??

これを以下の様にテーブルにする

関数f_{a_i}に入力a_1,\cdots,a_k,\cdotsを与えたときの出力を表している

例えばf_{a_1}(a_3)=00

出力は例

Zero, Total

3章 計算可能性の分析

この本特有の用語

集合Lの難しさ: 集合Lに対する決定問題の難しさ

認識プログラム: \Sigma^*型の値を1つ引数に取り、1または0を返すプログラム

受理: 認識プログラムAに対し、A(x)=1

拒否: 認識プログラムAに対し、A(x)=0

認識: 認識プログラムAが、集合Lを認識するとは、

任意のLの要素xに対して、A(x)=1を満たすこと

特徴述語

x\in Lを表す論理式R_L(x)のことを、Lの特徴述語という

決定問題のことを認識問題と呼んでいる

任意の「関数の計算問題」を「同等の難しさをもつ集合」に変換できる

述語は関数の一般化

述語は集合を扱う

「関数の計算問題」を「集合の決定問題」(「述語の計算問題」)に一般化できる

Lを認識する認識プログラムがある

= Lは帰納的

= Lの特徴述語は計算可能

半認識

一般的な用語ではない

\forall x\in \Sigma^*に対して、

x\in LならA(x)=1

x\notin LならA(x)は停止しない

普通の認識との差はどこ #??

半帰納的

一般的な用語ではない

集合Lを半認識するプログラムが存在するとき、Lのことを半帰納的という

半帰納的なら帰納的

p.65の3.6から