パラレルワールドをチラ見する②

ちゃんと理解していないまま、マルコフの構成的解析学をやる*1。

本当に理解していません。

1. チャーチのテーゼとマルコフの原理
2. 内容を見る
- 2-1. 排中律
- 2-2. 関数の連続性
3. まとめ

1. チャーチのテーゼとマルコフの原理

マルコフ流の解析学では、計算可能な実数をすごく重視します。

いつものとおり、実数をコーシー列 $a_n$ で定めるのですが、計算可能な数列 $b_n$ によって、

$(1) \quad \forall n, i, j [b_n \lt i, j \to |a_i - a_j| \lt 2^{-n}$ ]

という性質が成り立つときに、実数になると想定します。したがって、実数 $a$ を $\pm 2^{-N}$ の精度で計算しようとすると、数列 $a_n$ を第 $b_N$ 項くらいまで計算すればよい（それができるものが実数である）ということになります。

これは、チャーチのテーゼの一変種です*2。

マルコフ流の解析学では、チャーチのテーゼのほかに、マルコフの原理と呼ばれる公理を採用しています。

マルコフの原理もMarkov's principle - Wikipediaを見る限り、変種がいろいろあるのですが、

if it is impossible that an algorithm does not terminate, then for some input it does terminate.

と、

For each real number x, if it is contradictory that x is equal to 0, then there exists y ∈ Q such that 0 < y < |x|, often expressed by saying that x is apart from, or constructively unequal to, 0.

を使うことにしました*3。

2. 内容を見る

2-1. 排中律

マルコフ流の解析学では、一部の排中律を否定できるようです。

具体的には、

$(2) \quad \forall a [\forall n (a_n = 0) \lor \neg \forall n (a_n = 0)$ ]

を否定します。ということで、ひとまずこの式を仮定しておきます。

ここで、ある数列 $a_n$ に対して、次のような数列 $\gamma_{m, n}$ を考える。

・ $a_m$ が、nステップ以内で停止するとき、停止するステップを $l$ として、

$\gamma_{m, n} = 2^{-l}$

・そうじゃないとき、

$\gamma_{m, n} = 0$

このとき、停止するステップを $L$ とするとき、

・ $n \lt L$ では、 $n \lt i, j$ で $|\gamma_{m, i} - \gamma_{m, j}| \leq 2^{-L}$

・ $n \geq L$ では、 $n \lt i, j$ で $|\gamma_{m, i} - \gamma_{m, j}| = 0$

となるため、いずれにせよ $\lt 2^{-n}$ となります。なので、 $b_n = n$ としておけば、(1)を突破することができることになります。

さらに、特定の $m$ について、

・ $a$ が停止しないならば、 $\forall n (\gamma_{m, n} = 0)$

・ $a$ が $L$ ステップで停止するならば、 $\forall n (n \geq L \to \gamma_{m, n} = 2^{-L})$

で、各 $n$ について、 $\lambda_m = \gamma_{m, n}$ とすると、 $\lambda$ は実数となります。

・ $a_m$ が停止しないとき、そのときに限り

$\lambda_m = 0$

となります。

(2)式を場合分けで考えてみます。

(i) $\forall m (\lambda_m = 0)$ のとき

これは、 $a_m$ が停止しないということができる、ということです。

しかし、 $a_m$ が停止しないことを示すようなアルゴリズムは一般に存在しません。したがって、これはあり得ないということになります。

(ii) $\neg \forall m (\lambda_m = 0)$ のとき

これは、「 $a_m$ が停止しないと仮定したときに矛盾が生じる」という主張です。なので、マルコフの原理の一類型から、「 $a_m$ は停止する」ということができます。

しかし、 $a_m$ が停止することを示すようなアルゴリズムは一般に存在しません。したがって、これはあり得ないということになります。

(i)と(ii)により、いずれの選択肢もあり得ないということになるため、(2)は否定されます。

つまり、この種の排中律は成り立たないということです*4。

2-2. 関数の連続性

Kushner(1999)のp.278では、

A constructive function by Markov is an algorithm $f$ whose arguments and values are c.r.n.-s and such that for every two equal c.r.n.-s $x_1$ and $x_2$ the values $f(x_1)$ and $f(x_2)$ are equal c.r.n.-s