エレファント・コンピューティング調査報告

極限に関する順序を論理プログラミングの手法を使って指定することを目指すブロクです。

中間報告(10)

「ラムダ計算と無限ラムダ多項式」では呼び出しの深さが有限のクロージャーを含む式を表すための「有限ラムダ多項式」を定義しましたが、これは「一般マグマの多項式」と同様のものでした。呼び出しの深さが有限なのでクロージャーを除去することはできると思われるのですが、式にクロージャーを含むようにしたほうが良いのでこれも考えていきたいと思います。これは「有限ラムダ代数」という名前に変更したいと思います。

「たらい回し関数」はクロージャーの変数を「変更できない変数」にする方法のために調査していたのですが、これはできそうにないので中断しています。「アッカーマン関数」の項の中で書いた関数の分類は使えるかもしれません。

フラクタル」もこの目的に使えるかもしれないので調査しています。このブログでは有限時間で終了する論理プログラミングと無限の時間動作する論理プログラミングの関係をフラクタルの考え方で表すことはできないかと考えていましたが、中断しています。クロージャーを表すために使えるかどうかも考えてみたいと思っています。

またMathematics and Computingで書いたフラクタルのプログラムをJavaScriptで書き直しているので、その件もこのブログに書こうと思っています。

フラクタル(1)

このブログでは有限時間で終了する論理プログラミングと無限の時間動作する論理プログラミングの関係をフラクタルの考え方で表すことはできないかと以前考えていましたが、その件は今は中断しています。今後はクロージャーではどうなるか考えてみたいと思っています。

Mathematics and Computingフラクタルの図形を描画できるようになっていたのですが、JavaActiveXで書いてあるので今は動作しないようです。これは今後書き換えていきたいと思います。

Vectorのサイトに上記のサイトのプログラムに「ソースコード」を作成するエディタを追加したものが登録してあります。(WindowsFractal Diagram Editorの詳細情報 : Vector ソフトを探す!JavaFractal Diagram Editor(Javaアプリケーション版)の詳細情報 : Vector ソフトを探す!)

フラクタル: 混沌と秩序のあいだに生まれる美しい図形 アルケミスト双書』や『アートで魅せる数学の世界』に書かれている「Lシステム」のような形で描画できるシステムを作成してみましたが、それだとあまり複雑なことはできそうにない感じです。

そこでMathematics and Computingのシステムを発展させてC#のコードのように書けるようにしたいと思ったのですが、まだうまくできていません。

まずMathematics and Computingを書き換えてみたいと思います。

アッカーマン関数(3)

関数の再帰的定義

ここではある形の関数の再帰的定義について考えます。

 g: X \to X に対して  g^+: \mathbb{N} \times X \to \mathbb{N} \times X g^+(n, x) = (n+1, f(x)) と定義します。

 \mathcal{S}(g^+, (n, x)) = \{ S \mid S \subseteq \mathbb{N} \times X, (n, x) \in S, g^+(S) \subseteq S \} \overline{g^+}(n, x) = \bigcap \mathcal{S}(g^+, (n, x)) とおきます。

 \mathcal{S}_0 = \mathcal{S}(g^+, (0, a)) R = \overline{g^+}(0, a) = \bigcap \mathcal{S}_0 とおくと  R
 \begin{cases}
(0, a) \in R \\
(n, x) \in R \implies (n+1, g(x)) \in R
\end{cases}
を満たす最小の集合となります。

 S \subseteq \mathbb{N} \times X に対して  \pi_1(S) = \{ n \in \mathbb{N} \mid (n, x) \in S \ \text{を満たす} \ x \in X \ \text{が存在する}\} と定義します。

 R_1 = \pi_1(R) とおくと
 \begin{cases}
0 \in R_1 \\
n \in R_1 \implies n+1 \in R_1
\end{cases}
が成り立つので、自然数の性質より  R_1 = \mathbb{N} となります。

計算可能性の議論にはこれだけでも良いとは思うのですが
 f(n) = x \iff (n, x) \in R
によって関数  f: \mathbb{N} \to X を定義するには、任意の  n \in \mathbb{N} と任意の  x, y \in X に対して  (n, x) \in R かつ  (n, y) \in R ならば  x = y が成り立つ必要があります。以下でこれを示します。

 \{(0, a)\} \cup \overline{g^+}(g^+(0, a)) \in \mathcal{S}_0 となるので  R \subseteq \{(0, a)\} \cup \overline{g^+}(g^+(0, a)) となります。

 (0, x) \in R とすると  (0, x) \notin \overline{g^+}(g^+(0, a)) なので  (0, x) \in \{(0, a)\} となります。よって  x = a となります。

よって  n = 0 のときには成り立ちます。

次に  n のときには成り立つと仮定します。 (n, b) \in R とします。

 R_n = \{(k, x) \in R \mid k \le n\} c = g(b) とおくと  (n+1, c) \in R となります。

 R_n \cup \{(n+1, c)\} \cup \overline{g^+}(g^+(n+1, c)) \in \mathcal{S}_0 となるので  R \subseteq R_n \cup \{(n+1, c)\} \cup \overline{g^+}(g^+(n+1, c)) となります。

 (n+1, x) \in R とすると  (n+1, x) \notin R_n \cup \overline{g^+}(g^+(n+1, c)) なので  (n+1, x) \in \{(n+1, c)\} となります。よって  x = c となって  n+1 のときにも成り立ちます。

よって帰納法により任意の  n \in \mathbb{N} と任意の  x, y \in X に対して  (n, x) \in R かつ  (n, y) \in R ならば  x = y が成り立ちます。よって
 f(n) = x \iff (n, x) \in R
によって関数  f: \mathbb{N} \to X を定義することができます。

アッカーマン関数(2)

ハイパー演算子

計算論 計算可能性とラムダ計算 (コンピュータサイエンス大学講座)』の「問 1.3.17 (4)」が簡単にはできそうにないので、まず『コンピュータと数学 (現代基礎数学)』の第5章を見ていきます。第5章では「ハイパー演算子」(wikipedia:ハイパー演算子と同様ですが記法は異なります)から関数族の階層を定義しています。この階層は「グジェゴルチク階層」(wikipedia:グジェゴルチク階層、『数学基礎論の応用』*1参照)と同様のものと考えられます(定義は異なります)。この階層から「問 1.3.17 (4)」が得られると考えられます。

定義 5.2.1 自然数  j に対して  h_j: \mathbb{N} \to \mathbb{N}
 \begin{cases}
h_0(x) = \mathrm{suc}(x) \\
h_{j+1}(x) = h_j^*(x, x) = h_j^x(x) \\
\end{cases}
と定義します。ここで
 \mathrm{suc}(x) = x + 1
  h_j^*(n, x) = h_j^n(x) = \underbrace{h_j(h_j(\cdots(h_j(}_{n 回}x))\cdots))
を表しています。

補題 5.2.2 任意の自然数  j, k, x に対して

  1.  0 < x のとき  h_j^k(x) < h_j^{k+1}(x)
  2.  h_j^k(x) < h_j^{k}(x+1)
  3.  0 < x のとき  h_j^k(x) \le h_{j+1}^{k}(x)
  4.  h_j^{kx}(x) \le h_{j+1}^{k}(x)

が成り立ちます。以下でこれを示します。

(1)  0 < x のとき  h_j^k(x) < h_j^{k+1}(x)

 0 < x のとき  x < h_j(x)」 (*)ならば主張が成り立ちます。

 j = 0 のとき  h_0(x) = \mathrm{suc}(x) > x なので成り立っています。

 j のときに成り立つ(すなわち  x < h_j(x))と仮定すると  x < h_j(x) < h_j^2(x) < h_j^3(x) < \cdots となるので
 x < h_j(x) < h_j^2(x) < \cdots < h_j^x(x) = h_{j+1}(x)
となります。 0 < x なので  x < h_{j+1}(x) となって  j + 1 のときにも成り立ちます。

よって帰納法により(*)が成り立ちます。

(2)  h_j^k(x) < h_j^{k}(x+1)

 h_0^k(x) = \mathrm{suc}^k(x) = x + k < (x + 1) + k = \mathrm{suc}^{k}(x+1) = h_0^{k}(x+1)
となるので  j = 0 のとき成り立ちます。

 h_j^k(x) < h_j^{k}(x+1) と仮定すると
 h_{j+1}(x) = h_j^x(x) < h_j^{x}(x+1) < h_j^{x+1}(x+1) = h_{j+1}(x+1)
となります。よって任意の  x, y に対して  x < y ならば  h_{j+1}(x) < h_{j+1}(y) が成り立ちます。

 h_{j+1}^n(x) < h_{j+1}^n(y) と仮定すると  h_{j+1}^{n+1}(x) < h_{j+1}^{n+1}(y) が成り立つので任意の  n に対して  h_{j+1}^n(x) < h_{j+1}^n(y) となります。よって  h_{j+1}^k(x) < h_{j+1}^{k}(x+1) となって  j + 1 のときも成り立ちます。

よって帰納法により主張が成り立ちます。

(3)  0 < x のとき  h_j^k(x) \le h_{j+1}^{k}(x)

(1)より  x < h_j(x) < h_j^2(x) < \cdots < h_j^x(x) = h_{j+1}(x)
であり  k = 0 のときは成り立ちます。

 0 < h_j^k(x) \le h_{j+1}^{k}(x) と仮定すると  k = 0 の結果と(2)から
 h_j^{k+1}(x) = h_j(h_j^k(x)) \le h_j(h_{j+1}^{k}(x)) \le h_{j+1}(h_{j+1}^{k}(x)) = h_{j+1}^{k+1}(x)
となって  k + 1 のときも成り立ちます。

よって帰納法により主張が成り立ちます。

(4)  h_j^{kx}(x) \le h_{j+1}^{k}(x)

 k = 0 のときは明らかに成り立ちます。

 x \le y \le z のとき(2)と(1)から
 h_j^{x}(y) \le h_j^{x}(z) \le h_{j}^z(z) = h_{j+1}(z)
が成り立ちます。

 h_j^{kx}(x) \le h_{j+1}^{k}(x) と仮定します。
 h_j^{(k+1)x}(x) = h_j^{x}(h_j^{kx}(x)) \le h_{j+1}(h_{j+1}^{k}(x)) = h_{j+1}^{k+1}(x)
となって  k + 1 のときも成り立ち、帰納法により主張が成り立ちます。

アッカーマン関数(1)

アッカーマン関数についても調査します。

アッカーマン関数は以下のように非負整数  x y に対して帰納的に定義された関数です(wikipedia:アッカーマン関数計算論 計算可能性とラムダ計算 (コンピュータサイエンス大学講座) 参照)。
\begin{cases}
f(0, y) & = & y + 1 & (a1) \\
f(x + 1, 0) & = & f(x, 1) & (a2) \\
f(x + 1, y + 1) & = & f(x, f(x + 1, y)) & (a3) \\
\end{cases}

  •  f(x, y) \widehat{f}(x)(y)
  •  \widehat{f}(x_1) ( \widehat{f}(x_2) ( \cdots \widehat{f}(x_n) (y) \cdots )) をかっこを省略して  \widehat{f}(x_1) \widehat{f}(x_2) \cdots \widehat{f}(x_n) (y)
  •  \underbrace {\widehat{f}(x) \cdots \widehat{f}(x)} _{n \ 個} (y) \widehat{f}(x)^n(y)

と書くことにするとアッカーマン関数の定義は
\begin{cases}
\widehat{f}(0)(y) & = & y + 1 & (a1') \\
\widehat{f}(x + 1)(0) & = & \widehat{f}(x)(1) & (a2') \\
\widehat{f}(x + 1)(y + 1) & = & \widehat{f}(x) \widehat{f}(x + 1)(y) & (a3') \\
\end{cases}
となります。
\begin{eqnarray*}
f(x, y) & = & \widehat{f}(x)(y) \\
& \underset{(a3')}{=} & \widehat{f}(x-1) \widehat{f}(x) (y-1) \\
& \underset{(a3')}{=} & \widehat{f}(x-1)^2 \widehat{f}(x) (y-2) \\
& \vdots & \\
& \underset{(a3')}{=} & \widehat{f}(x-1)^y \widehat{f}(x) (0) \\
& \underset{(a2')}{=} & \widehat{f}(x-1)^y \widehat{f}(x-1) (1) \\
& = & \widehat{f}(x-1)^{y+1} (1) \\
\end{eqnarray*}
が成り立ちます。(a4')

アッカーマン関数は原始帰納的関数ではない帰納的関数であるということの証明が計算論 計算可能性とラムダ計算 (コンピュータサイエンス大学講座)の問題にあるのでそれを見ていきます。

まず  f(1, y) f(2, y) f(3, y) f(4, y) がどうなるか調べます。

 f(1, y)

 \widehat{f}(0)(y) = y + 1 n 回繰り返すと
 \widehat{f}(0)^n (y) = y + \underbrace {1+\cdots +1} _{n \ 個} = y + n
となります。よって
 \widehat{f}(1)(y) = \widehat{f}(0)^{y+1} (1) = 1 + (y + 1) = y + 2

 f(2, y)

 \widehat{f}(1)(y) = y + 2 n 回繰り返すと
 \widehat{f}(1)^n (y) = y + \underbrace {2+\cdots +2} _{n \ 個} = y + 2n
となります。よって
 \widehat{f}(2)(y) = \widehat{f}(1)^{y+1} (1) = 1 + 2(y + 1) = 2y + 3

 f(3, y)

 \widehat{f}(2)(y) + 3 = 2(y + 3) となるので、これを  n 回繰り返すと
 \widehat{f}(2)^n(y) = (y + 3) \cdot \underbrace {2 \cdot \cdots \cdot 2} _{n \ 個} - 3 = 2^n(y + 3) - 3
となります。よって
 \widehat{f}(3)(y) = \widehat{f}(2)^{y+1} (1) = 2^{y+1}(1 + 3) - 3 = 2^{y+3} - 3

 f(4, y)

 a^b a \wedge b と書くと、 \widehat{f}(3)(y) + 3 = 2^{y + 3} = 2 \wedge (y + 3) となります。これを  n 回繰り返すと
 \widehat{f}(3)^n(y) =  \underbrace {2 \wedge ( \cdots \wedge (2} _{n \ 個} \wedge (y + 3)) \cdots ) - 3
このかっこは省略することにします。
 \widehat{f}(3)^n(y) =  \underbrace {2 \wedge \cdots \wedge 2} _{n \ 個} \wedge (y + 3) - 3
 \underbrace {a \wedge \cdots \wedge a} _{b \ 個}  a \barwedge b と書くことにすると
 \widehat{f}(4)(y) = \widehat{f}(3)^{y+1} (1) = \underbrace {2 \wedge \cdots \wedge 2} _{y+1 \ 個} \wedge (1 + 3) - 3 = 2 \barwedge (y+3) - 3

問 1.3.17 について考えます。

(1)  x + y + 1 \le f(x, y)

 x = 0 のとき

 f(0, y) \underset{(a1)}{=} y + 1 = x + y + 1

 x - 1 のとき成り立つ(1-1)として  x \ (\ge 1) のとき

 y = 0 のとき

 f(x, 0) \underset{(a2)}{=} f(x-1, 1) \underset{(1-1)}{\ge} (x-1) + 1 + 1 = x + y + 1

 y - 1 のとき成り立つ(1-2)として  y \ (\ge 1) のとき

 \begin{eqnarray*}
f(x, y) & \underset{(a3)}{=} & f(x-1, f(x, y-1)) \\
 & \underset{(1-1)}{\ge} & (x-1) + f(x, y-1) + 1 \\
 & \underset{(1-2)}{\ge} & (x-1) + (x + (y-1) + 1) + 1 \\
 & = & 2x + y \ge x + y + 1
\end{eqnarray*}

(2)  f(x, y) < f(x, y+1) \le f(x + 1, y)

(2-1)  f(x, y) < f(x, y+1)

 x = 0 のとき

 f(0, y) \underset{(a1)}{=} y + 1 < y + 2 \underset{(a1)}{=} f(0, y + 1)

 x \ \ge 1 のとき

 \begin{eqnarray*}
f(x, y+1) & \underset{(a3)}{=} & f(x-1, f(x, y)) \\
 & \underset{(1)}{\ge} & (x-1) + f(x, y) + 1 \\
 & = & x + f(x, y) > f(x, y)
\end{eqnarray*}

(2-2)  f(x, y+1) \le f(x + 1, y)

 x = 0 のとき

 f(x, y+1) = f(0, y+1) \underset{(a1)}{=} y + 2 = f(1, y) = f(x+1, y)

 y = 0 のとき

 f(x, y+1) = f(x, 1) \underset{(a2)}{=} f(x+1, 0) = f(x+1, y)

 x, y \ge 1 のとき

 f(x+1, y-1) \underset{(1)}{\ge} (x+1) + (y-1) + 1 = x + y + 1
よって
 f(x+1, y) \underset{(a3)}{=} f(x, f(x+1, y-1)) \underset{(2-1)}{>} f(x, y+1)

(3) 任意の  a, b \ge 0 に対して  f(a, f(b, y)) < f(c, y) ( \forall y \in \mathbb{N})を満たす  c \ge 0 がある

 b = 0 のとき

 f(a, f(0, y)) \underset{(a1)}{=} f(a, y + 1) \underset{(2-2)}{\le} f(a + 1, y) \underset{(2)}{<} f(a + 2, y)

 b のとき成り立つ(3-1)と仮定して  b + 1 のとき

 y = 0 のとき

 f(a, f(b+1, 0)) \underset{(a2)}{=} f(a, f(b, 1)) \underset{(3-1)}{<} f(c, 1) \underset{(a2)}{=} f(c+1, 0)
を満たす  c が存在します。

 y のとき成り立つ(3-2)と仮定して  y + 1 のとき

 f(a, f(b+1, y+1)) \underset{(a3)}{=} f(a, f(b, f(b+1, y))) \underset{(3-1)}{<} f(c, f(b+1, y)) \underset{(3-2)}{<} f(c', y)
を満たす  c, c' が存在します。

たらい回し関数(6)

while の繰り返しが2回以下であることを考えると、以下のように書き直すことができます。これを見ると a2 と c2 は計算する必要がありません。

        public static string Test()
        {
            int count = 0;
            int depth = 0;
            float tarai(float x, float y, float z, int d)
            {
                count++;
                d++;
                depth = d > depth ? d : depth;
                if (x <= y)
                {
                    return y;
                }
                else
                {
                    float a = tarai(x - 1, y, z, d);
                    float b = tarai(y - 1, z, x, d);
                    float c = tarai(z - 1, x, y, d);
                    (x, y, z) = (a, b, c);
                    count++;
                    d++;
                    depth = d > depth ? d : depth;
                    if (x <= y)
                    {
                        return y;
                    }
                    else
                    {
                        float a2 = tarai(x - 1, y, z, d);
                        float b2 = tarai(y - 1, z, x, d);
                        float c2 = tarai(z - 1, x, y, d);
                        (x, y, z) = (a2, b2, c2);
                        count++;
                        d++;
                        depth = d > depth ? d : depth;
                        return y;
                    }
                }
            }
            return $"{tarai(12, 6, 0, 0)}, count = {count}, depth = {depth}";
        }

たらい回し関数(5)

たらい回し関数についてはクロージャーの説明には使えそうにないので変数を使わないように書き直す意味はあまりないとは思いますが、やってみます。

たらい回し関数をできるだけ変数を使わないように書き直します。このために前回「呼び出しの深さ」について考えました。「呼び出しの深さ」別に tarai_0、tarai_1、tarai_2 のように関数を作っていきます。以下では「呼び出しの深さ」2 でかなり複雑になるので以下の関数では 2 までしかありません.が、これが無限に続くと考えると擬似的に無限の場合を表しています。

C# ではあまりうまく書くことができないのでわかりにくいですし、「呼び出しの深さ」2 までしかないので「幅」0 の場合しか計算できません(これはあまり意味がありません)。これが続いていくことを想像できるようコードを掲載します。

        public static string Test()
        {
            float tarai_0(float x, float y, float z)
            {
                return (x <= y ?
                        y :
                        0);
            }
            float tarai_1(float x, float y, float z)
            {
                return (x <= y ?
                        y :
                        ((x - 1 <= y ?
                            y :
                            0) <= (y - 1 <= z ?
                            z :
                            0) ?
                            (y - 1 <= z ?
                                z :
                                0) :
                            0));
            }
            float tarai_2(float x, float y, float z)
            {
                return (x <= y ?
                        y :
                        ((x - 1 <= y ?
                            y :
                            ((x - 1 - 1 <= y ?
                                y :
                                0) <= (y - 1 <= z ?
                                z :
                                0) ?
                                (y - 1 <= z ?
                                    z :
                                    0) :
                                0)) <= (y - 1 <= z ?
                            z :
                            ((y - 1 - 1 <= z ?
                                z :
                                0) <= (z - 1 <= x ?
                                x :
                                0) ?
                                (z - 1 <= x ?
                                    x :
                                    0) :
                                0)) ?
                            (y - 1 <= z ?
                                z :
                                ((y - 1 - 1 <= z ?
                                    z :
                                    0) <= (z - 1 <= x ?
                                    x :
                                    0) ?
                                    (z - 1 <= x ?
                                        x :
                                        0) :
                                    0)) :
                            (((x - 1 <= y ?
                                y :
                                ((x - 1 - 1 <= y ?
                                    y :
                                    0) <= (y - 1 <= z ?
                                    z :
                                    0) ?
                                    (y - 1 <= z ?
                                        z :
                                        0) :
                                    0)) - 1 <= (y - 1 <= z ?
                                z :
                                ((y - 1 - 1 <= z ?
                                    z :
                                    0) <= (z - 1 <= x ?
                                    x :
                                    0) ?
                                    (z - 1 <= x ?
                                        x :
                                        0) :
                                    0)) ?
                                (y - 1 <= z ?
                                    z :
                                    ((y - 1 - 1 <= z ?
                                        z :
                                        0) <= (z - 1 <= x ?
                                        x :
                                        0) ?
                                        (z - 1 <= x ?
                                            x :
                                            0) :
                                        0)) :
                                0) <= ((y - 1 <= z ?
                                z :
                                ((y - 1 - 1 <= z ?
                                    z :
                                    0) <= (z - 1 <= x ?
                                    x :
                                    0) ?
                                    (z - 1 <= x ?
                                        x :
                                        0) :
                                    0)) - 1 <= (z - 1 <= x ?
                                x :
                                ((z - 1 - 1 <= x ?
                                    x :
                                    0) <= (x - 1 <= y ?
                                    y :
                                    0) ?
                                    (x - 1 <= y ?
                                        y :
                                        0) :
                                    0)) ?
                                (z - 1 <= x ?
                                    x :
                                    ((z - 1 - 1 <= x ?
                                        x :
                                        0) <= (x - 1 <= y ?
                                        y :
                                        0) ?
                                        (x - 1 <= y ?
                                            y :
                                            0) :
                                        0)) :
                                0) ?
                                ((y - 1 <= z ?
                                    z :
                                    ((y - 1 - 1 <= z ?
                                        z :
                                        0) <= (z - 1 <= x ?
                                        x :
                                        0) ?
                                        (z - 1 <= x ?
                                            x :
                                            0) :
                                        0)) - 1 <= (z - 1 <= x ?
                                    x :
                                    ((z - 1 - 1 <= x ?
                                        x :
                                        0) <= (x - 1 <= y ?
                                        y :
                                        0) ?
                                        (x - 1 <= y ?
                                            y :
                                            0) :
                                        0)) ?
                                    (z - 1 <= x ?
                                        x :
                                        ((z - 1 - 1 <= x ?
                                            x :
                                            0) <= (x - 1 <= y ?
                                            y :
                                            0) ?
                                            (x - 1 <= y ?
                                                y :
                                                0) :
                                            0)) :
                                    0) :
                                0)));
            }
            int diff(float x, float y)
            {
                if (x <= y)
                {
                    return 0;
                }
                else
                {
                    return (int)Math.Ceiling(x - y);
                }
            }
            int dist(float x, float y, float z)
            {
                float m = Math.Min(Math.Min(x, y), z);
                return diff(x, m) + diff(y, m) + diff(z, m);
            }
            float tarai(float x, float y, float z)
            {
                switch (dist(x, y, z) * 3 + 1)
                {
                    case 0:
                        return tarai_0(x, y, z);
                    case 1:
                        return tarai_1(x, y, z);
                    case 2:
                        return tarai_2(x, y, z);
                }
                return -1;
            }
            return tarai(0, 0, 0).ToString();
        }

このように x、y、z 以外の変数を使わないように書き直すことができました。