Sプログラム計算可能性定義1.3

Sプログラム計算可能性
定義1.3
(1) 関数 f （Σ* 上の（部分）関数）に対し，次の条件を満たす
Sプログラム A を，f を計算するSプログラムという。
（ただし，Dom(f) は f の定義域）
すべての x ∈ Σ* に対し，
x ∈ Dom(f) ⇒ Aに x を与えて実行すると f(x) を出力して停止する
x ∉ Dom(f) ⇒ Aに x を与えて実行すると，正常終了しない
なお，実行が halt 文で終了することを，正常終了と考える
(2) 関数 f に対し，それを計算するSプログラムが存在するとき，
f をSプログラム計算可能という
$ Sプログラムの実行環境は未定義
%
& 変数の数は有限であれば良い（メインメモリ無限大）
表記法1.1
SプログラムAに対し
A(x)： A に x を与えて実行したときの出力
述語
Σ* のすべての元に対して，1(真) か 0(偽) を返す全域関数
万能Sプログラム
次に定義される関数 comp を計算するSプログラム
comp(p, x) =
A(x),
p が，あるSプログラム A のコードのとき,
0,
p がSプログラムのコードになっていないとき,
定理1.2
関数 comp を計算する万能Sプログラム univ が存在する
証明の概略
p と x が与えられたとき，univ はおおまかにいって，
次の手順で comp を計算する
(1) p が標準形Sプログラムの2進数コードになっているかを調べ，
もし p が正しいコードでなければ，即座に 0 を出力して終了
(2) p があるSプログラムAのコードだった場合には，
A の x に対する実行をシミュレートし，halt文で終了した場合には
同じ出力を出して計算を終了する．
ステップ(1) はやさしい
定理1.2 証明の概略つづき
ステップ(2)
変数 pc : A の pc
v : A の変数のリスト (v1,...,vL)
動作 A のプログラムに従い，pcとvを更新する
pc = 0 となったとき，v の第一成分を出力して終了
prog univ (input p, x);
if ¬is-prog?(p) then halt(0) end-if
K ← get(p,1); L ← get(p,2); ss ← get(p,3);
v ← (x, ε,...,ε);
A が停止しないとき，
pc ← 1;
while pc ≠ 0 do
A の pc が 0 にならない
s ← get(ss, pc); 文sを実行（pcの変更も含む）
end-while
⇒ univ は停止しない
halt(get(v,1))
end-prog
L − 1
t-comp
A が正常終了しない場合，comp( !A" , x) は未定義
comp は部分関数
!A" は A の2進コード
↓ 全域化
t-comp(p, x) =
$ A(x),
%
& 0,
p が，ある A のコードで
しかも A(x) が正常終了するとき
その他のとき．
定理1.3
t-comp を計算するSプログラムは存在しない．
つまり，t-comp はSプログラム計算不可能
定理1.3証明
背理法：t-comp を計算するSプログラムの存在を仮定
次のような関数 h を考える
! 1, t-comp(x, x) = 0 のとき
h(x) = "
# 0, t-comp(x, x) ≠ 0 のとき
h(x) の定義より，∀x, h(x) ≠ t-comp(x, x)
t-comp を計算するSプログラム
⇒ hを計算するSプログラム Ah
ph = &Ah' とおくと，
h(x) = comp(ph, x) = t-comp(ph, x) ← h(x) は全域的
ここで，x = ph と，とると，h(ph) = t-comp(ph, ph)
矛
盾
定理1.3 証明（対角線論法）
Σ*の元を，次の順に並べ，w1, w2, ... とする．
長さの短い順，長さが同じなら２進数読みで小さい順
つまり，w1 = 0, w2 = 1, w3 = 00, w4 = 01, ...
t-comp(wi, wj) の表
d(wi) の表
w1 w2 w3 . . . wi
w1
0
0
0
0
w2
0
0
0
0
w3
.
..
wi
0
0
0
0
1
10 11
1010
対角成分
変更
0→1
0以外→0
w1 w2 w3 . . . wi
w1
w2
w3
w3
1
1
1
0
" 1, t-comp(wi, wi) = 0 のとき，
d(wi) = #
$ 0, t-comp(wi, wi) ≠ 0 のとき．
定理2.7 証明（対角線論法）つづき
w1 w2 w3 . . . wi
w1 w2 w3 . . . wi
w1
0
0
0
0
w1
w2
0
0
0
0
w2
w3
..
.
wi
0
0
0
0
w3
1
10 11
1010
1
1
1
w3
0
t-comp を計算するSプログラム
⇒ dを計算するSプログラム Ad
wd = "Ad# とする
表の作り方より，t-comp(wd, wd) ≠ d(wd)
一方，wd は d を計算するSプログラムのコードなので，
t-comp(wd, wd) = d(wd)
矛
盾
定理1.4
次の述語は計算不可能
! 1, p が，あるSプログラム A のコードで，
halt?(p, x) = "
しかも，A(x) が正常終了するとき，
# 0, その他のとき．
halt? が計算可能なら，halt? を計算するSプログラムと
comp を計算するSプログラムunivを用いて，
t-comp を計算するSプログラムが作れる
定理1.3に反する
prog t-comp (input p, x);
if ¬halt?(p,x) then halt(0)
else halt(univ(p,x)) end-if
end-prog

Download Report