Background
C++で書かれた以下の関数 f は(整数型のビット制約を無視すれば)全て同一の(数学的な意味での)関数
$$\Sigma\colon \mathbb{N}^{\ast} \to \mathbb{N},\quad a \mapsto \sum_{i\in\operatorname{index}\left(a\right)}a_{i}$$
を計算する:
#include<valarray>
int f(std::valarray<int> const& ar) {
int sum = 0;
for (const auto& x: ar) {
sum += x;
}
return sum;
}
#include<cstddef>
#include<valarray>
std::valarray<int> g(std::valarray<int> const& ar) {
std::size_t const N = ar.size();
std::size_t const M = (N + 1) / 2;
std::valarray<int> psum(M);
for(std::size_t i = 0; i < N / 2; ++i) {
psum[i] = ar[i*2] + ar[i*2 + 1];
}
if (N % 2 != 0) {
psum[M-1] = ar[N-1];
}
return psum;
}
int f(std::valarray<int> const& ar) {
std::valarray<int> psum(ar);
while(psum.size() > 1) {
psum = g(psum);
}
return psum.size() == 0 ? 0 : psum[0];
}
前者は素直な総和計算(左結合)を実装したものである.後者は「隣り合う2項を足して約半分の長さの配列を作る」という操作を繰り返すことで総和を計算している.
アルゴリズムまで変えなくとも,単に使用する変数名を変えたり,コメント行を追加したりすれば,同じ関数を計算するプログラムをいくらでも作れる.一般化して言えば次のようになる:
定理(インフォーマル). C++において,いかなる(数学的)関数についても,それを実現するプログラムが複数通り存在する.
そこで次のような問いが立ち上がってくる:
問題(インフォーマル). いかなる(数学的)関数についても,それを実現するプログラムがただ一通りに決まるような,変則的なプログラミング言語は存在するだろうか?
つまり,ある機能を実現するためのプログラムの「正解」がただ一つに決まってしまうような言語はあるか,という問題である.もしそのような言語があれば,どういう設計で機能を実現すれば綺麗だとか,コーディングスタイルをどうするかとか,識別子の名前をどうするかとか,そういったことに煩わされることがなくなる.
本記事ではこれに対する回答を与える.答えを先に言っておくと,そのようなプログラミング言語は存在する.ただし使い物にはならない.
ナンバリングとm-還元
前述の問題を数学的にformulateしなければ話が始まらない.そのためには計算可能部分関数のナンバリングと還元の理論を知る必要がある.
ナンバリング
定義(計算可能性クラス).
$$\mathcal{P}^{\left(n\right)} := \set{f \mid f\colon\mathbb{N}^{n}\rightharpoonup \mathbb{N}\text{ is computable}}.$$
ここで $A \rightharpoonup B$ は $A$ の部分集合から $B$ への関数(部分関数)を意味する.
定義(ナンバリング). クラス $\mathcal{A} \subseteq \mathcal{P}^{\left(n\right)}$ のナンバリング(numbering)とは,全射 $\varphi \colon \mathbb{N} \to \mathcal{A}$ のことをいう.自然数 $e$ を部分関数 $\varphi_{e} := \varphi\left(e\right)$ の $\varphi$–インデックスと呼ぶ.
例えば,C++のプログラムは究極的にはただの文字列であり,文字列はUTF-8などの文字エンコーディングによってバイナリ表現される.バイナリ表現の際に先頭と終端がself-containedに分かる形で表現1した後,これを自然数の2進表現として読めば,プログラムを自然数と同一視できる.この対応を $\operatorname{enc}(P) = e$ と書こう.そして
$$\varphi_{e} := \begin{cases} \text{$P$ の計算する $n$–変数部分関数}, & \operatorname{enc}^{-1}\left(e\right) = \set{P} \\ \varnothing, & \operatorname{enc}^{-1}\left(e\right) = \varnothing \end{cases}$$
と定義する2.この $\varphi \colon \mathbb{N} \to \mathcal{P}^{\left(n\right)}$ は $\mathcal{P}^{\left(n\right)}$ のナンバリングになる.さらにこのナンバリングは以下のような良い性質を持つ.
定義(計算可能ナンバリング). クラス $\mathcal{A}\subseteq \mathcal{P}^{\left(n\right)}$ のナンバリング $\varphi$ が計算可能であるとは,部分関数 $\operatorname{eval}\colon \mathbb{N} \times \mathbb{N}^{n} \rightharpoonup \mathbb{N}$, $\left(e, \vec{x}\right) \mapsto \varphi_{e} \left(\vec{x}\right)$ が計算可能であることをいう.
C++に対応するナンバリングは計算可能である.C++に限らず既存の(実際に計算機で動かせる)プログラミング言語の定めるナンバリングは全て計算可能である.
約束. 以下を同一視する:
- (Turing完全な)プログラミング言語 ↔ 計算可能ナンバリング
- プログラム ↔ インデックス(自然数)
Turing完全なプログラミング言語がナンバリングを定めることは(Turing完全の定義から)自明である.計算可能であることは,プログラムを計算機の中で実行できることと同じことである.コンパイル言語ならコンパイルしてから実行する一連の流れをひとつの計算機の中で行えるし,スクリプト言語ならランタイムにスクリプトを渡して実行する一連の流れをひとつの計算機の中で行える.プログラムとインデックスの対応は既に述べた通り.
ここでは自然数上の部分関数だけを考えているが,このことは理論の適用範囲を一切狭めない.例えば自然数以外のデータ構造はどれも自然数にエンコーディングできる.(プログラムを自然数にエンコーディングしたのと全く同じ方法による.)したがって木,リスト,文字列,多倍長浮動小数点数などを許容する場合にも全く同じ結果を適用できる.
ここでは純粋な(数学的)部分関数を考えている.つまり副作用(side effect)を考えないもののみを扱っている.しかしこれも理論の適用範囲を狭めない.なぜなら副作用を含む関数は「環境」を関数の入出力に含めることによって純粋な関数として表現可能だからである.Haskellのような圏論に動機づけられた言語は,この方法で環境・副作用を扱うことができる.
ただし「外部環境からの入力」は考慮していないことに注意.例えば熱雑音を利用した計算(x86系CPUにおける RDRAND 命令など)はこの枠組みでは扱えない.確率的Turing機械モデルなどを利用する必要がある.もちろんそこでも類似の理論を展開できる.
m-還元
定義(多対一還元). $\varphi,\psi$ を $\mathcal{A}\subseteq\mathcal{P}^{\left(n\right)}$ のナンバリングとする.$\varphi$ を $\psi$ に多対一還元可能(many-one reducible)またはm-還元可能(m-reducible)とは,計算可能関数 $h\colon \mathbb{N} \to \mathbb{N}$ が存在して $\varphi = \psi \circ h$ が成り立つことをいう.このことを $\varphi \leq_{m} \psi$ と表記する.
m-還元は $\varphi$–プログラム $e$ を $\psi$–プログラム $h\left(e\right)$ に変換するトランスパイラ $h$ の存在と見做せる.例えば,いかなるコンパイル言語も最終的には機械語に変換(コンパイル)されるのだから,コンパイル言語の定めるナンバリングは機械語の定めるナンバリングにm-還元可能というわけである.通常の実用プログラミング言語3はデコンパイルが原理的には常に可能なわけだから,その反対のことも言える.つまり既存のプログラミング言語は互いに互いをm-還元可能である.
ここで「多対一」というのは複数のプログラムが同じプログラムに変換されうるからである.例えば(コメントを最適化のヒントに使うようなコンパイラを除けば)コメントを増やそうと減らそうと,コンパイラは同じ機械語を吐き出す.実は後で述べるように,還元先の言語が良い性質を備えている場合,これを必ず一対一にできる.
アクセプタブルナンバリング
Turing完全な実用プログラミング言語(機械語を含む)は互いに互いをm-還元可能であると述べたが,実際にはそれより遥かに強いことが言える.
定義(アクセプタブルナンバリング). クラス $\mathcal{A} \subseteq \mathcal{P}^{\left(n\right)}$ のナンバリング $\varphi$ がアクセプタブル(acceptable)であるとは,以下の2つを満たすことをいう:
- $\varphi$ は計算可能である
- $\mathcal{A}$ の任意の計算可能ナンバリング $\psi$ に対して $\psi \leq_{m} \varphi$
つまり,どんなプログラミング言語であっても,そのプログラミング言語にトランスパイルできるような,懐の深い?プログラミング言語がアクセプタブルナンバリングである.実は,Turing完全な実用プログラミング言語はどれもアクセプタブルであることが知られている.
定理(Smn定理). $\varphi^{\left(n\right)}$ を $\mathcal{P}^{\left(n\right)}$ の計算可能ナンバリングとする.次は同値:
- $\varphi^{\left(n\right)}$ はアクセプタブルである
- 計算可能関数 $S^{m}_{n} \colon \mathbb{N}^{m} \to \mathbb{N}$ が存在して
- $\varphi^{\left(n\right)} \left(S^{m}_{n}\left(\vec{y}\right)\right) = \varphi^{\left(n+m\right)}\left({-},\vec{y}\right)$
つまり部分適用(partial evaluation)が可能なプログラミング言語であればアクセプタブルになるわけである.ラムダ計算において部分適用は言語そのものに内蔵されている.C++では std::bind がこれを実現する4.
部分適用が可能なときアクセプタブルになることは簡単に分かる.$\varphi^{\left(n\right)}$ を部分適用を持つプログラミング言語に対応するナンバリングとする.$\psi$ を $\mathcal{P}^{\left(n\right)}$ の任意の計算可能ナンバリングとする.仮定より,$\psi$ は $1+n$–変数部分関数と見做したときに計算可能であるから,その $\varphi^{\left(1+n\right)}$–インデックス $i$ を取ることができる.つまり
$$\varphi^{\left(n\right)}_{i} \left(e, \vec{x}\right) = \psi\left(e\right)\left(\vec{x}\right)$$
である.すると
$$h\left(e\right) := S^{1}_{n}\left(i,e\right)$$
は $\psi_{e}$ の $\varphi^{\left(n\right)}$–インデックスとなる.つまり $\psi$ は $\varphi^{\left(n\right)}$ にm-還元可能である.
パディング補題と同型定理
C++(を含む普通のプログラミング言語)においては,いかなる部分関数に対しても,それを実現するプログラムがいくらでも多く存在する.これを数学的に厳密な形で述べたものが次のパディング補題(Padding Lemma)である:
定理(パディング補題). $\varphi$ を $\mathcal{P}^{\left(n\right)}$ のアクセプタブルナンバリングとする.次を満たす計算可能関数 $\operatorname{pad}\colon \mathbb{N}\times\mathbb{N}\to\mathbb{N}$ が存在する:
- $\varphi_{\operatorname{pad}\left(e, x\right)} = \varphi_{e}$
- $\operatorname{pad}\left(e, x\right) \geq x$
具体的なプログラミング言語から導かれるアクセプタブルナンバリングでは,コメント行や値を変えない命令などを機械的に付け加えることで,$\varphi_{e}$ を変えずに $e$ をいくらでも大きくできる.よってパディング補題が成立する.実は特定のプログラミング言語に依存することなく抽象的な議論で証明することもできる.
証明. $\left( A, B\right)$ を計算的分離不能対,すなわち以下を満たすものとする:
- $A,B$ は計算的枚挙可能(computably enumerable,c.e.)な $\mathbb{N}$ の部分集合である
- $A\cap B = \varnothing$
- $A,B$ を分離($A \subseteq C \subseteq \mathbb{N}\setminus B$)する計算可能集合 $C$ は存在しない
計算可能部分関数 $\psi \colon \mathbb{N}^{2}\to\mathbb{N}$ を
$$
\psi_{\braket{i,j}}\left(x\right)=
\begin{cases}
j, & j\in A,\\
\varphi_{i}\left(x\right), & j\in B,\\
\text{undefined}, & \text{otherwise}
\end{cases}
$$
で定める.ここで $\braket{-,-}$ は $\mathbb{N}^{2} \to \mathbb{N}$ なる計算可能全単射である.$\psi$ は計算可能ナンバリングを成す.$\varphi$ はアクセプタブルだから,計算可能関数 $h$ であって $\psi = \varphi\circ h$ を満たすものが取れる.
次に $\mathbb{N}$ の部分集合列 $C_{0},C_{1},\ldots$ を次で定める:
$$
C_{i}=\set{h\left(\braket{i,j}\right)|j\in B}.
$$
$\psi$ の定義より,各 $i$ に対して $\psi_{\braket{i,k}}=\varphi_{i}$ を満たす $k\in A$ は存在すれば一意的であり,任意の $j\in A\setminus \set{k}$ に対して $\psi_{\braket{i,j}}\neq\varphi_{i}$ かつ $h\left(\braket{i,j}\right)\notin C_{i}$ が成り立つ.よって
$$
D_{i}=\set{j|h\left(\braket{i,j}\right)\in C_{i}}
$$
とおけば,$D_{i} \setminus \set{k}$ は $A,B$ を分離する.よって $D_{i} \setminus \set{k}$ は計算不能であり,そのためには $C_{i}$ も計算不能でなければならない.とくに $C_{i}$ は無限集合でなければならない.
$\Sigma^{0}_{1}$–単層化定理より,計算的枚挙可能集合
$$
E := \set{\left(e,x,i\right)|x\leq i \land i\in C_{e}}
$$
は計算可能選択関数 $p\colon \mathbb{N}^{2} \to \mathbb{N}$ を持つ.これは
- $p\left(e, x\right) \geq x$
- ある $j\in B$ に対し $p\left(e, x\right) = h\left(\braket{e,j}\right)$
を満たす.後者より
$$
\begin{aligned}
\varphi_{p\left(e, x\right)} &= \varphi_{h\left(\braket{e,j}\right)} \\
&= \psi_{\braket{e,j}} \\
&= \varphi_{e}
\end{aligned}
$$
が成り立つ.□
補題. $\varphi,\psi$ を $\mathcal{P}^{\left(n\right)}$ の計算可能ナンバリングとする.$\psi$ はアクセプタブルかつ $\varphi \leq_{m} \psi$ と仮定する.このとき,計算可能単射 $h\colon \mathbb{N} \to \mathbb{N}$ が存在して $\varphi = \psi \circ h$ が成り立つ.
証明. $g$ を $\varphi = \psi \circ g$ なる計算可能関数とする.これは単射とは限らない.また $\operatorname{pad}\colon\mathbb{N}\times\mathbb{N}\to\mathbb{N}$ をパディング補題における関数とする.計算可能関数 $h\colon \mathbb{N}\to\mathbb{N}$ を次のように原始再帰によって定義する:
$$
\begin{aligned}
h\left(0\right) & := g\left(0\right) \\
h\left(e+1\right) & := \operatorname{pad}\left(g\left(e+1\right), h\left(e\right)\right)
\end{aligned}
$$
定義より $h$ は $\varphi = \psi \circ h$ を満たす.また $h$ は狭義単調増加であるから単射である.□
ここから次が従う:
定理(Rogersの同型定理). $\varphi,\psi$ を $\mathcal{P}^{\left(n\right)}$ のアクセプタブルナンバリングとする.このとき計算可能全単射 $h\colon \mathbb{N} \to \mathbb{N}$ が存在して $\varphi = \psi \circ h$ (よって $\psi = \varphi \circ h^{-1}$)が成り立つ.
証明は異様に長いので省略する.基本戦略はCantor–Bernstein–Schröderの定理5の証明と類似の往復論法(back-and-forth argument)に基づく.$\varphi$ から $\psi$ への単射な還元と $\psi$ から $\varphi$ への単射な還元を取ってきて,それらを交互に合成した写像をうまく使って全単射な還元 $h$ を構築するわけである.ただしこの構成によって得られる全単射が計算可能となるような工夫が必要である.
この定理は「m-完全集合は互いに再帰同型である」というMyhillの定理のナンバリング版である.
Riceの定理と決定不能問題
定理(Rice). $\mathcal{A}$ を $\mathcal{P}^{\left(n\right)}$ の部分クラス,$\varphi$ を $\mathcal{P}^{\left(n\right)}$ のアクセプタブルナンバリングとする.もし $A:=\set{ e\in \mathbb{N} \mid \varphi_{e} \in \mathcal{A} }$ が計算可能ならば $\mathcal{A}=\varnothing$ または $\mathcal{A} = \mathcal{P}^{\left(n\right)}$ が成り立つ.
ここで,$\mathcal{A}$ は部分計算可能関数に関する何かしらの性質を表しており,$A$ はそのような性質を満たすプログラム全体の成す集合と見做せる.Riceの定理は,与えられたプログラムがそのような性質を満たすかどうかは,自明なケースを除いては機械的に判定できないということを述べている.
例えば,与えられた2つのプログラムが同一の部分関数を実現しているかどうかは,機械的に判定することができない.
系. $\varphi$ を $\mathcal{P}^{\left(n\right)}$ のアクセプタブルナンバリングとする.このとき2つの指標が同一の部分関数を表現しているかどうか $\varphi_{i} = \varphi_{j}$ は計算可能でない.
証明. さもなくば,$\mathcal{A} := \set{\varnothing}$ に対する $A$ が計算可能になってしまって,Riceの定理と矛盾する.□
Friedbergナンバリング
問題の定式化
定義(Friedbergナンバリング). 単射かつ計算可能なナンバリングをFriedbergナンバリングと呼ぶ.
我々の冒頭の問いは次のように定式化できる:
問題. $\mathcal{P}^{\left(n\right)}$ のFriedbergナンバリングは存在するか?
この問題の答えは「Yes」である.
定理(Friedberg 1958 6). $\mathcal{P}^{\left(n\right)}$ はFriedbergナンバリングを持つ.
それではどうやって構成すればいいだろうか?すぐ思いつく方法はナンバリングの重複を見つけて削除するというものである.つまり $\varphi$ を $\mathcal{P}^{\left(n\right)}$ のアクセプタブルナンバリングとする.ここから単射なナンバリング $\psi$ を
$$
\begin{aligned}
\psi\left(0\right) &:= \varphi \left(0\right) \\
\psi\left(e+1\right) & := \varphi\left(\mu i. \bigwedge_{j\leq e} \varphi\left(i\right) \neq \psi\left(j\right) \right)
\end{aligned}
$$
で定義するわけである.しかしこの方法はうまくいかない.というのも,右辺にて重複判定している部分があるが,Riceの定理の系によれば,これは計算不可能だからである.
Friedbergナンバリングの構成
Friedbergナンバリングは優先法(priority argument)という複雑な構成法によって得ることができる.特定の要件の族を満たすc.e.集合や計算可能部分集合(グラフを考えればc.e.集合と見做せる)を構成するには,下から近似するc.e.列を構成すればよい.構成の各ステージでは,所望の要件が満たされるように元を加えていくのだが,ある要件を満たそうとした結果として,別の要件が覆される(injured)場合がある.そこで,要件の間に優先度を設けて,より高い優先度の方が優先的に満たされるようにする.これをうまくやると,どの要件も高々有限回覆された後,満たされた状態で安定するようになる.これが優先法である.
ここではShen7によるゲーム理論的な証明を,Kummer8によるpriority-freeな証明と同じ流れに整理した,筆者9による証明を紹介する.
定義(強稠密性). $\mathcal{A}$ と $\mathcal{B}$ を $\mathcal{P}^{\left(1\right)}$ の部分クラスとする.$\mathcal{B}$ が $\mathcal{A}$ の中で強稠密(strongly dense)であるとは,$\mathcal{A}$ に属するどの部分関数の有限部分10も $\mathcal{B}$ の中に無限個の拡張を持つときをいう.
補題(Kummer 19898). $\mathcal{A}$ と $\mathcal{B}$ を $\mathcal{P}^{\left(1\right)}$ の部分クラスとする.以下を仮定する.
- $\mathcal{A} \cap \mathcal{B} = \varnothing$
- $\mathcal{A}$ は $\mathcal{B}$ の中で強稠密
- $\mathcal{A}$ は計算可能ナンバリングを持つ
- $\mathcal{B}$ はFriedbergナンバリングを持つ
このとき $\mathcal{A} \cup \mathcal{B}$ はFriedbergナンバリングを持つ.
先ず,次のような二人,無限,完全情報ゲームを考える:
- プレイヤー: Alice, Bob
-
プロトコル: ターン $s=0,1,2,\ldots$ において
- Aliceは有限部分関数 $A_{s}\colon \mathbb{N}^{2} \rightharpoonup \mathbb{N}$ を宣言する
- Bobは有限部分関数 $A_{s}\colon \mathbb{N}^{2} \rightharpoonup \mathbb{N}$ と有限集合 $K_{s}\subseteq \mathbb{N}$ を宣言する
- 付帯条件: $A_{s}$, $B_{s}$, $K_{s}$ はそれぞれ $\subseteq$–増大列でなければならない
-
勝利条件: 極限において以下の全ての要件が満たされた場合はBobの勝利とする.それ以外の場合はAliceの勝利とする
- 各 $i \in \mathbb{N}$ に対し $j \in \mathbb{N}\setminus K$ が存在して $A\left(i,{-}\right) = B\left(j,{-}\right)$
- $\mathbb{N}\setminus K \ni i \mapsto B\left(i,{-}\right)$ は単射である
つまり $B$ が $\mathbb{N}\setminus K$ から $\set{A\left(i, {-}\right) \mid i\in \mathbb{N}}$ への全単射になっていれば勝利である.とくに $K = \varnothing$ なら $B$ は単射なナンバリングである.
ここで $\mathbb{N}^{2} \rightharpoonup \mathbb{N}$ は $\omega \times \omega$ のセルに自然数が埋められた盤面と見做す.各ターン毎に,AliceはA–盤面の空いているセルに有限個の自然数を入れ,BobはB–盤面の空いているセルに有限個の自然数を入れる.さらにBobは各ターン毎にB–盤面の有限個の行を選んで勝敗判定から除外することができる.このターンを無限に続けた極限において,A–盤面にあるどの行に対しても,それと同じ内容の行がB–盤面に存在し,かつB–盤面のどの行もユニークであるとき,Bobの勝利とする(ここで除外された行は考慮しない).
このゲームについて次が成り立つ:
主張(Shen 20127). Bobは計算可能必勝戦略を持つ.
主張の証明. Bobは可算無限人のエージェントを用意し,それらに自然数で番号付けておく.
- エージェントはB–盤面の除外されていない行を排他的に予約することができる
- エージェントは番号の小さい順番に行動する
エージェント $i\in \mathbb{N}$ は以下の手順に従って行動する:
- ターン $s<i$ の間は待機する
- ターン $s\geq i$ では,以下の操作を行う:
- もし現在予約している行がないならば,予約可能な最初の行を予約する
- $k$ を自身が現在までに除外した行の個数とする
- A-盤面の $i$–行の最初の $k$–列目までの状態が,それより上のいずれかの行と一致している場合,その行を除外する
- どれとも一致していなかった場合は,A-盤面の $i$–行の現在の状態を,除外されていない予約した行にコピーする
この戦略は計算可能である.なぜなら,各ターンでエージェントは有限人のみ動作し,手順の各ステップは計算可能に実行できるからである.極限において以下が成立する:
- どのB–盤面の行も予約されているか除外されているかのいずれかである
- もしA–盤面の $i$–行が,先行する行と一致する場合,エージェント $i$ は行の除外を無限回実行する.したがって,極限において,エージェント $i$ によって予約されたままの行は存在しない
- もしA-盤面の $i$–行が,先行する行と一致しない場合,エージェント $i$ は行の除外を高々有限回だけ実行する.したがって,極限において,エージェント $i$ によって予約されたままの行が一意的に存在する
ここから極限においてBobの勝利条件が満たされることが分かる. □
補題の証明(I. 20159). Aliceが $\mathcal{A}$ の計算可能ナンバリング(の有限近似列)に従ってプレイする状況を考える.この場合にBobは行の除外を行わなくて良いことが分かる.何故なら,各エージェントは,行を除外する代わりに,除外したい行が極限において $\mathcal{B}$ に属す元となるようにセルを埋めれば良いからである.ただし $\mathcal{B}$ の各元は高々一回ずつだけ使うようにするため,自分及び他のエージェントがまだ選んでいない $\mathcal{B}$ の元を選ぶようにする.(これは $\mathcal{B}$ がFriedbergナンバリングを持つことと強稠密性から常に可能である.)この戦略に従ってプレイすると,$B$ はある $\mathcal{B}'\subseteq \mathcal{B}$ に対する $\mathcal{A} \cup \mathcal{B}'$ のFriedbergナンバリングとなる.ここで $\mathcal{B}'=\mathcal{B}$ を保証するためには,Bobはさらに追加で可算無限人のエージェントを用意する.エージェントはターン $i$ において,B–盤面の行をひとつ予約するとともに,$\mathcal{B}$ の未使用の元をひとつ(Friedbergナンバリングの順番で最初のものを)選び,極限においてその行がその元と一致するようにセルを埋めていけばよい.□
主定理の証明(Kummer 1989). $\mathcal{B} \subseteq \mathcal{P}^{\left(1\right)}$ を偶数個の入力に対してのみ値が定義された部分関数全体の成すクラスとする.そして $\mathcal{A} = \mathcal{P}^{\left(1\right)} \setminus \mathcal{B}$ とおく.このとき $\mathcal{A}$ は計算可能ナンバリングを持ち,$\mathcal{B}$ はFriedbergナンバリングを持つことが容易に分かる.さらに $\mathcal{B}$ は $\mathcal{A}$ の中で強稠密である.よってKummerの補題により $\mathcal{P}^{\left(1\right)}$ はFriedbergナンバリングを持つ.
まとめ
実用プログラミング言語ではコーディングには「自由度」がある.同一言語であっても同じ機能を実現するコードが無数に存在する(パディング補題).さらには「2つのコードが同じ機能を実現しているか?」という判定問題は計算不可能である(Riceの定理).一方,優先法という構成法を用いると,どんな機能にもそれぞれただ一通りのコードが対応するような,異常なプログラミング言語を構成できる.このプログラミング言語ではコーディングスタイルやプログラミングパラダイムの論争は生じない.さらには2つのコードの機能的同値性の機械的判定すら可能である.そのようなプログラミング言語の言語仕様はおよそ人間に扱える複雑さではなく,またその計算量は現実の計算機で実行できるような複雑さではない,という欠点を措けば.
-
例えば
0000 0000 0000 0001と0000 0001はどちらも自然数としては1に対応する.つまり,単純にバイナリを自然数の二進表現と見做すだけだと,この対応は単射にならないので,自然数から元のバイナリを復元できない.この問題は次のようなエンコーディングを用いて回避できる.
バイナリ列 $\sigma := b_{1}b_{2}\cdots b_{N}$ を任意に取る.長さ $N$ の二進表現を $l_{1}l_{2}\cdots l_{M}$ とする.次の長さ $2 \left\lceil \log_{2}\left( N + 1 \right) \right\rceil + 2 + N$ のバイナリ列を考える:$$l_{1}l_{1}l_{2}l_{2}\cdots l_{n}l_{n} 01 \sigma.$$
これを元々のバイナリ表現の代わりに用いればよい. ↩ -
正確には,何らかの識別子(
__PARTIAL_FUNCTIONなど)を予約しておいて,$e$ に対応する文字列 $P$ が「当該識別子が $n$ 個のunsigned intを受け取ってunsigned intを返す関数であるようなC++プログラム」である場合のみ,一つ目の条件分岐にマッチさせる. ↩ -
Turing完全な言語.計算能力の著しく制限された言語は除く.例えば,単純型付きラムダ計算は強正規性を持つことから,部分的にのみ定義された関数は記述できず,したがってTuring完全ではない.それゆえ無限ループするような実行可能バイナリを当該言語にデコンパイルすることはできない. ↩
-
Cantorは,集合 $A$ の濃度が集合 $B$ の濃度以下 $\left|A\right| \leq \left| B \right|$ であるということを,単射 $A\to B$ が存在することと定めた.一方,濃度が等しい $\left|A\right| = \left| B \right|$ ということを,全単射 $A \cong B$ が存在することと定めた.CBSの定理は $\left|A\right| \leq \left| B \right| \leq \left| A \right|$ (双方向の単射の存在)から $\left|A\right| = \left| B \right|$ (全単射の存在)を導く定理である. ↩
-
Friedberg, Richard M. “Three Theorems on Recursive Enumeration. I. Decomposition. II. Maximal Set. III. Enumeration Without Duplication.” The Journal of Symbolic Logic, Vol. 23, No. 3 (1958): 309–316. https://doi.org/10.2307/2964290 ↩
-
Shen, A. (2012). Game Arguments in Computability Theory and Algorithmic Information Theory. In: Cooper, S.B., Dawar, A., Löwe, B. (eds) How the World Computes. CiE 2012. Lecture Notes in Computer Science, vol 7318. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-30870-3_66 ↩ ↩2
-
Kummer, M. (1989). Numberings of R1∪F. In: Börger, E., Büning, H.K., Richter, M.M. (eds) CSL '88. CSL 1988. Lecture Notes in Computer Science, vol 385. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0026301 ↩ ↩2
-
Imamura, T. (2015). Game arguments in some existence theorems of Friedberg numberings, arXiv preprint. https://doi.org/10.48550/arXiv.1508.04387 ↩ ↩2
-
関数 $f\colon A\to B$ をグラフ $G_{f}:=\set{\left(x, f\left(x\right)\right) \mid x\in A}$ と同一視する.そのうえで $G_{g}$ が $G_{f}$ の有限部分集合になっているようなものを考える. ↩