エレファント・ビジュアライザー調査記録

ビジュアルプログラミングで数式の変形を表すことを考えていくブロクです。

ラムダ計算と無限ラムダ多項式(17)

たらい回し関数の例

フィボナッチ数列の例ではクロージャーを変数を使わずに書く例としては単純すぎてわかりにくかったので、たらい回し関数が使えるかどうか調べてみます。まずたらい回し関数自体について調べてみます。たらい回し関数は以下のように定義された関数です(wikipedia:竹内関数参照)。
 \mathrm{tarai}(x,y,z)= \\
\begin{cases}
y & (x \leq y \ のとき) \\
\mathrm{tarai}(\mathrm{tarai}(x-1,y,z), \mathrm{tarai}(y-1,z,x), \mathrm{tarai}(z-1,x,y)) & (x > y \ のとき) \\
\end{cases}

 \mathrm{tarai}(x,y,z)=
\begin{cases}
y & (x \leq y\  のとき) \\
z & (x > y \ かつ \ y \leq z \ のとき) \\
x & (x > y \ かつ \ y > z \ のとき) \\
\end{cases}
が成り立ちます。まずこれが成り立つことを示します。 \mathrm{tarai}(x,y,z) t(x, y, z) と書きます。

ハッカーの遺言状──竹内郁雄の徒然苔第18回:問題児も悪くない | サイボウズ式によると整数でなくても成り立つということなので、そのような形で示します。うまくパターン化できるかと思ったのですができなかったので長くなっています。

 x \leq y のとき

定義より  x \leq y のとき  t(x,y,z)=y が成り立ちます。

 x > y かつ  y \leq z のとき

 c_n = t(x-n, y, z) d_n = t(z-1,x-n,y) とおきます。 y-1 < y \leq z となるので定義より   t(y-1,z,x-n) = z となります。よって
 c_n = t(x-n, y, z) \\
= t(t(x-(n+1),y,z), t(y-1,z,x-n), t(z-1,x-n,y)) \\
= t(c_{n+1}, z, d_n)
が成り立ちます。

 n = \min\{n \mid x-n \leq y\} \ (n \ge 1) とおくと
 c_n = t(x-n, y, z) = y
 c_{n-1} = t(c_n, z, d_{n-1}) = t(y, z, d_{n-1}) = z
が成り立ちます。

帰納法により  c_{i} = z \ (i = 0, 1, \cdots , n-1) を示します。 i = n-1 の場合は上に書いた通りです。 i=k のときに成り立つと仮定すると
 c_{k-1} = t(c_{k}, z, d_{k-1}) = t(z, z, d_{k-1}) = z
となって  i=k-1 のときにも成り立ちます。よって  c_{i} = z \ (i = 0, 1, \cdots , n-1) が成り立ちます。

よって  t(x,y,z) = c_{0} = z が成り立ちます。

 x > y かつ   y > z のとき

 a_{m} = t(x-m, y, z)
 b_{m} = \begin{cases}
z & (y-1 \le z \ のとき) \\
x-m & (y-1 > z \ のとき)
\end{cases}
とおきます。

 x-m > y かつ   y > z のとき
 a_{m} = t(x-m, y, z) \\
= t(t(x-(m+1), y, z), t(y-1, z, x-m), t(z-1, x-m, y)) \\
= t(a_{m+1}, b_{m}, x-m)
となります。

 m = \min\{m \mid x-m \leq y\} \ (m \ge 1) とおくと  x-(m-1) > y かつ  x-m \le y かつ   y > z となります。
 a_{m} = t(x-m, y, z) = y
 a_{m-1} = t(a_{m}, b_{m-1}, x-(m-1)) = t(y, b_{m-1}, x-(m-1))
が成り立ちます。ここで
 b_{m-1} = \begin{cases}
z & < & y &(y-1 \le z \ のとき) & (1) \\
x-(m-1) & > & y & (y-1 > z \ のとき) & (2)
\end{cases}
なので (2) のときは  a_{m-1} = x-(m-1) となります。(1) のときは
 a_{m-1} = t(y, z, x-(m-1)) = x-(m-1)
となります。

帰納法により  a_{i} = x-i \ (i = 0, 1, \cdots , m-1) を示します。 i = m-1 の場合は上に書いた通りです。 i=k のときに成り立つと仮定すると
 a_{k-1} = t(a_{k}, b_{k-1}, x-(k-1)) = t(x-k, b_{k-1}, x-(k-1))
 b_{k-1} = \begin{cases}
z & < & x-k &(y-1 \le z \ のとき) & (1) \\
x-(k-1) & > & x-k & (y-1 > z \ のとき) & (2)
\end{cases}
となるので (2) のときは  a_{k-1} = x-(k-1) となります。(1) のときは
 a_{k-1} = t(x-k, z, x-(k-1)) = x-(k-1)
となります。よって  a_{i} = x-i \ (i = 0, 1, \cdots , m-1) が成り立ちます。

よって  t(x, y, z) = a_{0} = x が成り立ちます。

ラムダ計算と無限ラムダ多項式(16)

フィボナッチ数列の例(4)

クラスを使ったものを考えます。

        private class FibClass
        {
            private int x = 0;
            private int y = 1;
            public int Next()
            {
                int z = x + y;
                x = y;
                y = z;
                return z;
            }
        }

このクラスを使ったものは以下のようになります。

            IEnumerable<int> fib()
            {
                FibClass fibobj = new FibClass();
                yield return 0;
                yield return 1;
                for (; ; )
                {
                    yield return fibobj.Next();
                }
            }

このクラスを変更しないようにしたものを考えます。

        private class FibClassImmutable
        {
            private readonly int x = 0;
            private readonly int y = 1;
            public FibClassImmutable()
            {
                x = 0;
                y = 1;
            }
            public FibClassImmutable(int x, int y)
            {
                this.x = x;
                this.y = y;
            }
            public FibClassImmutable Next()
            {
                return new FibClassImmutable(y, x + y);
            }
            public int Current
            {
                get
                {
                    return y;
                }
            }
        }

このクラスを使うと以下のようになります。

            IEnumerable<int> fib()
            {
                FibClassImmutable fibobj = new FibClassImmutable(0, 1);
                yield return 0;
                yield return 1;
                for (; ; )
                {
                    fibobj = fibobj.Next();
                    yield return fibobj.Current;
                }
            }

for を展開して変数を変更しないようにすると以下のようになります。

            IEnumerable<int> fib()
            {
                FibClassImmutable fibobj_0 = new FibClassImmutable(0, 1);
                yield return 0;
                yield return 1;
                FibClassImmutable fibobj_1 = fibobj_0.Next();
                yield return fibobj_1.Current;
                FibClassImmutable fibobj_2 = fibobj_1.Next();
                yield return fibobj_2.Current;
                FibClassImmutable fibobj_3 = fibobj_2.Next();
                yield return fibobj_3.Current;
                FibClassImmutable fibobj_4 = fibobj_3.Next();
                yield return fibobj_4.Current;
                FibClassImmutable fibobj_5 = fibobj_4.Next();
                yield return fibobj_5.Current;
                FibClassImmutable fibobj_6 = fibobj_5.Next();
                yield return fibobj_6.Current;
                FibClassImmutable fibobj_7 = fibobj_6.Next();
                yield return fibobj_7.Current;
                FibClassImmutable fibobj_8 = fibobj_7.Next();
                yield return fibobj_8.Current;
            }

フィボナッチ数列の例(5)

再帰的定義の関数を考えます。

            IEnumerable<int> fib()
            {
                int fib(int n)
                {
                    if (n == 0)
                    {
                        return 0;
                    }
                    else if (n == 1)
                    {
                        return 1;
                    }
                    else
                    {
                        return fib(n - 1) + fib(n - 2);
                    }
                }
                for (int i = 0; ; i++)
                {
                    yield return fib(i);
                }
            }

この関数は変数を変更しないので、for を展開すれば変数を変更しないようにすることができます。さらに再帰的定義を展開して再帰的定義を含まない形に書き直します。

            IEnumerable<int> fib()
            {
                int fib_0(int n)
                {
                    if (n == 0)
                    {
                        return 0;
                    }
                    else if (n == 1)
                    {
                        return 1;
                    }
                    else
                    {
                        return fib_1(n - 1) + fib_1(n - 2);
                    }
                }
                int fib_1(int n)
                {
                    if (n == 0)
                    {
                        return 0;
                    }
                    else if (n == 1)
                    {
                        return 1;
                    }
                    else
                    {
                        return fib_2(n - 1) + fib_2(n - 2);
                    }
                }
                int fib_2(int n)
                {
                    if (n == 0)
                    {
                        return 0;
                    }
                    else if (n == 1)
                    {
                        return 1;
                    }
                    else
                    {
                        return fib_3(n - 1) + fib_3(n - 2);
                    }
                }
                int fib_3(int n)
                {
                    if (n == 0)
                    {
                        return 0;
                    }
                    else if (n == 1)
                    {
                        return 1;
                    }
                    else
                    {
                        return fib_4(n - 1) + fib_4(n - 2);
                    }
                }
                int fib_4(int n)
                {
                    if (n == 0)
                    {
                        return 0;
                    }
                    else if (n == 1)
                    {
                        return 1;
                    }
                    else
                    {
                        return fib_5(n - 1) + fib_5(n - 2);
                    }
                }
                int fib_5(int n)
                {
                    if (n == 0)
                    {
                        return 0;
                    }
                    else if (n == 1)
                    {
                        return 1;
                    }
                    else
                    {
                        return fib_6(n - 1) + fib_6(n - 2);
                    }
                }
                int fib_6(int n)
                {
                    if (n == 0)
                    {
                        return 0;
                    }
                    else if (n == 1)
                    {
                        return 1;
                    }
                    else
                    {
                        return fib_7(n - 1) + fib_7(n - 2);
                    }
                }
                int fib_7(int n)
                {
                    if (n == 0)
                    {
                        return 0;
                    }
                    else if (n == 1)
                    {
                        return 1;
                    }
                    else
                    {
                        return fib_8(n - 1) + fib_8(n - 2);
                    }
                }
                int fib_8(int n)
                {
                    if (n == 0)
                    {
                        return 0;
                    }
                    else if (n == 1)
                    {
                        return 1;
                    }
                    else
                    {
                        return fib_9(n - 1) + fib_9(n - 2);
                    }
                }
                int fib_9(int n)
                {
                    return 0;
                }
                yield return fib_0(0);
                yield return fib_0(1);
                yield return fib_0(2);
                yield return fib_0(3);
                yield return fib_0(4);
                yield return fib_0(5);
                yield return fib_0(6);
                yield return fib_0(7);
                yield return fib_0(8);
                yield return fib_0(9);
            }

ラムダ計算と無限ラムダ多項式(15)

フィボナッチ数列の例

繰り返しの回数が有限のときに、(有限個の)変更しない変数で書けることや関数の再帰的定義を取り除くことができること(また変数や関数定義を取り除くことができること)を示すための例を考えます。

平方根の例は長いので、ここではフィボナッチ数列の例を考えます。フィボナッチ数列は以下のように定義されます(wikipedia:フィボナッチ数を参照)。

  •  F_0 = 0
  •  F_1 = 1
  •  F_{n+2} = F_n + F_{n+1} \ (n \ge 0)

フィボナッチ数列の例(1)

C#イテレーターを使って擬似的な無限の列を考えます。

            IEnumerable<int> fib()
            {
                int x = 0;
                int y = 1;
                yield return x;
                yield return y;
                for (; ; )
                {
                    int z = x + y;
                    yield return z;
                    x = y;
                    y = z;
                }
            }

最初の30項は以下のようになります。

0, 1, 1, 2, 3, 5, 8, 13, 21, 34, 55, 89, 144, 233, 377, 610, 987, 1597, 2584, 4181, 6765, 10946, 17711, 28657, 46368, 75025, 121393, 196418, 317811, 514229

繰り返しの回数が8回以内として「for」を「展開」して取り除き、変数を変更しないようにすると以下のようになります。

            IEnumerable<int> fib()
            {
                int x_0 = 0;
                int y_0 = 1;
                yield return x_0;
                yield return y_0;
                int z_0 = x_0 + y_0;
                yield return z_0;
                int x_1 = y_0;
                int y_1 = z_0;
                int z_1 = x_1 + y_1;
                yield return z_1;
                int x_2 = y_1;
                int y_2 = z_1;
                int z_2 = x_2 + y_2;
                yield return z_2;
                int x_3 = y_2;
                int y_3 = z_2;
                int z_3 = x_3 + y_3;
                yield return z_3;
                int x_4 = y_3;
                int y_4 = z_3;
                int z_4 = x_4 + y_4;
                yield return z_4;
                int x_5 = y_4;
                int y_5 = z_4;
                int z_5 = x_5 + y_5;
                yield return z_5;
                int x_6 = y_5;
                int y_6 = z_5;
                int z_6 = x_6 + y_6;
                yield return z_6;
                int x_7 = y_6;
                int y_7 = z_6;
                int z_7 = x_7 + y_7;
                yield return z_7;
            }

結果は以下のようになります。

0, 1, 1, 2, 3, 5, 8, 13, 21, 34

フィボナッチ数列の例(2)

fib() の中で fib() を参照するようにします。2つの数の和を取らなければいけないのですが、「foreach (…)」 の中では1つしか書くことができないので以下のようになります。

            IEnumerable<int> fib()
            {
                yield return 0;
                yield return 1;
                IEnumerator<int> fib_itr = fib().GetEnumerator();
                fib_itr.MoveNext();
                foreach (int n in fib())
                {
                    fib_itr.MoveNext();
                    yield return n + fib_itr.Current;
                }
            }

foreach をやめて for で書き直すと以下のようになります。

            IEnumerable<int> fib()
            {
                yield return 0;
                yield return 1;
                IEnumerator<int> fib_itr1 = fib().GetEnumerator();
                IEnumerator<int> fib_itr2 = fib().GetEnumerator();
                fib_itr2.MoveNext();
                for (; ; )
                {
                    fib_itr1.MoveNext();
                    fib_itr2.MoveNext();
                    yield return fib_itr1.Current + fib_itr2.Current;
                }
            }

for を展開することはできるのですが、fib_itr1.MoveNext()、fib_itr2.MoveNext() で fib_itr1、fib_itr2 が更新されるので、C#イテレーターを直接使うと変数が変更されないようにはできません。

            IEnumerable<int> fib()
            {
                yield return 0;
                yield return 1;
                IEnumerator<int> fib_itr1 = fib().GetEnumerator();
                IEnumerator<int> fib_itr2 = fib().GetEnumerator();
                fib_itr2.MoveNext();
                fib_itr1.MoveNext();
                fib_itr2.MoveNext();
                yield return fib_itr1.Current + fib_itr2.Current;
                fib_itr1.MoveNext();
                fib_itr2.MoveNext();
                yield return fib_itr1.Current + fib_itr2.Current;
                fib_itr1.MoveNext();
                fib_itr2.MoveNext();
                yield return fib_itr1.Current + fib_itr2.Current;
                fib_itr1.MoveNext();
                fib_itr2.MoveNext();
                yield return fib_itr1.Current + fib_itr2.Current;
                fib_itr1.MoveNext();
                fib_itr2.MoveNext();
                yield return fib_itr1.Current + fib_itr2.Current;
                fib_itr1.MoveNext();
                fib_itr2.MoveNext();
                yield return fib_itr1.Current + fib_itr2.Current;
                fib_itr1.MoveNext();
                fib_itr2.MoveNext();
                yield return fib_itr1.Current + fib_itr2.Current;
                fib_itr1.MoveNext();
                fib_itr2.MoveNext();
                yield return fib_itr1.Current + fib_itr2.Current;
            }

フィボナッチ数列の例(3)

C#イテレーターでは変数を変更しないようにはできなかったので、自作のイテレーターを作ります。

            IEnumerable<int> fib()
            {
                int x = 0;
                int y = 1;
                int next()
                {
                    int z = x + y;
                    x = y;
                    y = z;
                    return z;
                }
                yield return 0;
                yield return 1;
                for (; ; )
                {
                    yield return next();
                }
            }

この next を変数を変更しないように書き直します。

            IEnumerable<int> fib()
            {
                (int,int) next(int x, int y)
                {
                    int z = x + y;
                    return (y, z);
                }
                int x = 0;
                int y = 1;
                yield return 0;
                yield return 1;
                for (; ; )
                {
                    (x, y) = next(x, y);
                    yield return y;
                }
            }

そして for を展開すると変数を変更しないようにすることができます。

            IEnumerable<int> fib()
            {
                (int, int) next(int x, int y)
                {
                    int z = x + y;
                    return (y, z);
                }
                int x_0 = 0;
                int y_0 = 1;
                yield return 0;
                yield return 1;
                (int x_1, int y_1) = next(x_0, y_0);
                yield return y_1;
                (int x_2, int y_2) = next(x_1, y_1);
                yield return y_2;
                (int x_3, int y_3) = next(x_2, y_2);
                yield return y_3;
                (int x_4, int y_4) = next(x_3, y_3);
                yield return y_4;
                (int x_5, int y_5) = next(x_4, y_4);
                yield return y_5;
                (int x_6, int y_6) = next(x_5, y_5);
                yield return y_6;
                (int x_7, int y_7) = next(x_6, y_6);
                yield return y_7;
                (int x_8, int y_8) = next(x_7, y_7);
                yield return y_8;
            }

ラムダ計算と無限ラムダ多項式(14)

有限ラムダ多項式 Lisp

平方根の例」を移植するために Common Lisp のサブセットを目指した Lisp を作成します。これを「有限ラムダ多項式 Lisp」と呼ぶことにします。仕様は以下のようになります。

定数・変数

定数には数値、t (真を表す)、nil (偽を表す)があります。数値は任意の桁数の小数を使うことができます。定数と演算子以外の文字列は変数として使うことができます。

( 関数名 式 式 … 式 )

「式 式 … 式」を引数として関数を実行します。「関数名」は

  • 最初から定義されている関数名(car、cdr、cons、first、second、third、atom、null、list、progn、expt、equal、not、and、or など)
  • 演算子(+、-、*、/、=、/=、<、<=、>、>= など)
  • 定義された関数名
  • 評価されると関数になる式
  • 無名関数

のどれかです。

' 式

または (quote 式) とも書きます。式を評価しないものを表します。「'( 式 式 … 式 )」と書くとリスト「( 式 式 … 式 )」を表します。

(lambda (変数名 変数名 … 変数名) 式 式 … 式)

無名関数を表します。評価されるとクロージャーに変換されます。正式には #'~、または (function ~) と書くようですが、(Common Lisp では)単にこう書いても変換されるようなのでここでもそうします。

setf 変数名 式

(できるだけ Common Lisp に合わせたいのですが Common Lisp の仕様がよくわからないので)ここでは単に変数に式を対応させるものとなっています。setq も同様です。変数は「レキシカルスコープ」とします。これは以前「環境」で定義した変数と同じもので、書いた通りの意味の変数(関数内関数や名前呼びの変数のような)で関数が終了しても使える変数となります。「レキシカルスコープ」の変数が存在すればその変数を変更し、存在しなければ新規作成するとします。

(defun 関数名 (変数名 変数名 … 変数名) 式 式 … 式)

関数を定義します。再帰的定義もできます。「レキシカルスコープ」で関数名とクロージャーを対応させます。この後関数名を評価するとクロージャーに変換されます。

(if 条件式 式1 式2)

条件式を評価した結果が nil でなければ式1を評価、nil ならば式2を評価します。

平方根の例

(defun GetNextDecimalDigitAndNumbers
       (numbers)
       (progn (setf number (first numbers))
              (setf square_difference (second numbers))
              (setf scale (third numbers))
              (defun maxdd (dd)
                           (if (>= dd 0)
                               (progn (setf zd (* dd (expt 10 (- scale))))
                                      (setf number_sq_diff (+ (* (* number zd) 2) (* zd zd)))
                                      (if (<= number_sq_diff square_difference)
                                          (list dd
                                                (list (+ number zd)
                                                      (- square_difference number_sq_diff)
                                                      (+ scale 1)
                                                      )
                                                )
                                          (maxdd (- dd 1))
                                          )
                                      )
                               (list 0 (list 0 0 0))
                               )
                           )
              (maxdd 9)
              )
       )
(defun GenerateDecimal
       ()
       (progn (setf nums (list 0 3 0))
              (setf current_digit 0)
              (defun next
                     ()
                     (progn (setf current_digit (first (GetNextDecimalDigitAndNumbers nums)))
                            (setf nums (second (GetNextDecimalDigitAndNumbers nums)))
                            t
                            )
                     )
              (defun getCurrent () (progn current_digit))
              (defun setCurrent (val) (progn))
              (list next getCurrent setCurrent)
              )
       )
(defun take
       (count gen)
       (if (= count 0)
           ()
           (progn (setf next (first gen))
                  (setf getCurrent (second gen))
                  (setf setCurrent (third gen))
                  (if (next)
                      (cons (getCurrent) (take (- count 1) gen))
                      ()
                      )
                  )
           )
       )
(defun zipn
       (f n list)
       (if (null list)
           ()
           (cons (f (first list) n)
                 (zipn f (+ n 1) (cdr list))
                 )
           )
       )
(defun nlist
       (list)
       (zipn (function (lambda (n e) (* n (expt 10 (- e))))) 0 list)
       )
(defun foldr
       (f n list)
       (if (null list)
           n
           (f (first list) (foldr f n (cdr list)))
           )
       )
(defun number
       (list)
       (foldr (lambda (x y) (+ x y)) 0 (nlist list))
       )

サーバー側で計算し、一桁ずつ取得する例

(setf generator (GenerateDecimal))
(defun GetNextDecimalDigit
       ()
       (progn ((first generator)) ((second generator)))
       )
(defun repeat
       (number e count)
       (if (< e count)
           (repeat (+ number (* (GetNextDecimalDigit) (expt 10 (- e)))) (+ e 1) count)
           number
           )
       )
(setf count 21)
(repeat 0 0 count)

サーバー側で計算し、イテレーターを使う例

(setf count 21)
(number (take count (GenerateDecimal)))

ブラウザー側で計算し、(サーバー側の)データを更新する例

(setf numbers (list 0 3 0))
(defun repeat
       (number e count)
       (if (< e count)
           (progn (setf dd (first (GetNextDecimalDigitAndNumbers numbers)))
                  (setf ns (second (GetNextDecimalDigitAndNumbers numbers)))
                  (setf numbers ns)
                  (repeat (+ number (* dd (expt 10 (- e)))) (+ e 1) count)
                  )
           number
           )
       )
(setf count 21)
(repeat 0 0 count)

ブラウザー側で計算し、(サーバー側の)データを(ジェネレーターで)更新する例

(defun unfoldl
       (next init)
       (progn (setf src init)
              (setf dst 0)
              (defun next_
                     ()
                     (progn (setf dst (first (next src)))
                            (setf src (second (next src)))
                            t
                            )
                     )
              (defun getCurrent () (progn dst))
              (defun setCurrent (val) (progn))
              (list next_ getCurrent setCurrent)
              )
       )
(setf numbers (list 0 3 0))
(setf count 21)
(number (take count (unfoldl GetNextDecimalDigitAndNumbers numbers)))

ラムダ計算と無限ラムダ多項式(13)

有限ラムダ多項式によるクロージャーの定義

有限ラムダ多項式

有限ラムダ多項式は以下のものから構成されます。

演算子  f に対して演算子の項数  n が決まっているとします。定数は項数  0演算子とします。

クロージャーの定義

ラムダ式は以下のものから構成されます。

  • 定数
  • 変数
  •  f(x_1, x_2, \cdots , x_n)
  •  λ( (v_1, v_2, \cdots , v_n) . x, e)
  • let  v =  x in  y
  • subst  v =  x in  y
  • def  f (  v_1, v_2, \cdots , v_n ) =  x in  y
  • fun (  v_1, v_2, \cdots , v_n ) =  x
  • if  x then  y else  z

集合  E の元は変数  v、式  x E \cup \bot の元  e の組  \langle v, x, e \rangle とします。この元は再帰的定義にはなっていないとします。この元を  v \mapsto x : e と書くことにします。集合  E を「時代」、 E \cup \bot の元を「環境」と呼びます。

ある環境  e で変数  v に対応する式  e(v) を以下のように帰納的に定義します。

  •  e = \bot のとき  e(v) = \bot
  •  e = v \mapsto x : e' のとき  e(v) = x
  •  e = v' \mapsto x : e' \ (v \ne v') のとき  e(v) = e'(v)

ある環境  e に対して、変数  v に対応する式を  x で置き換えた環境  e(v \gets x) を以下のように帰納的に定義します。

  •  e = \bot のとき  e(v \gets x) = \bot
  •  e = v \mapsto y : e' のとき  e(v \gets x) = v \mapsto x : e'
  •  e = v' \mapsto y : e' \ (v \ne v') のとき  e(v \gets x) = v' \mapsto y : e'(v \gets x)

ある時代  E と環境  e \in E での式  x の値  \mathrm{val}(e, x) を考えます。

定数  a の値

定数  a の値は  \mathrm{val}(e, a) = a です。

変数  v の値

変数  v の値は  \mathrm{val}(e, v) = e(v) です。

 f(x_1, x_2, \cdots , x_n) の値

 f(x_1, x_2, \cdots , x_n) の値は、 \mathrm{val}(e, f) = λ( (v_1, v_2, \cdots , v_n) . y, e') (クロージャー)のときは
 \mathrm{val}(e, λ( (v_1, v_2, \cdots , v_n) . y, e')(x_1, x_2, \cdots , x_n)) \\
= \mathrm{val}( e', 
\operatorname{let} v_1 = \mathrm{val}(e, x_1) \operatorname{in}
\operatorname{let} v_2 = \mathrm{val}(e, x_2) \operatorname{in} \cdots
\operatorname{let} v_n = \mathrm{val}(e, x_n) \operatorname{in} y)
となります。このときクロージャーが持っている環境  e' を使います。

 \mathrm{val}(e, f)クロージャーではないときは、
 \mathrm{val}(e, f(x_1, x_2, \cdots , x_n)) 
= \mathrm{val}(e, f) ( \mathrm{val}(e, x_1), \mathrm{val}(e, x_2), \cdots , \mathrm{val}(e, x_n) )
とします。 \mathrm{val}(e, f) の部分は定数ではなくても良いものとします。

let  v =  x in  y の値

 v は変数、 x y は式です。

 E の「次の時代」 E' E' = E \cup \{v \mapsto x : e\} とし、 E'
 \mathrm{val}(e, \operatorname{let} v = x \operatorname{in} y) = \mathrm{val}(v \mapsto x : e, y)
とします。

subst  v =  x in  y の値

 v は変数、 x y は式です。

 E の「次の時代」 E' E' = (E \setminus \{v \mapsto x' : e\}) \cup \{v \mapsto x : e\} とし、 E'
 \mathrm{val}(e, \operatorname{subst} v = x \operatorname{in} y) = \mathrm{val}(e(v \gets x), y)
とします。このような  v \mapsto x' : e が存在しないときは
 \mathrm{val}(e, \operatorname{subst} v = x \operatorname{in} y) = \bot
とします。

def  f (  v_1, v_2, \cdots , v_n ) =  x in  y の値

関数定義を表します。 f は変数(関数名)、 v_1, v_2, \cdots , v_n は変数、 x y は式です。
 \mathrm{val}(e, \operatorname{def} f (v_1, v_2, \cdots , v_n) = x \operatorname{in} y) = \mathrm{val}( e', y)
とします。

ここで  e' = (f \mapsto λ( (v_1, v_2, \cdots , v_n) . x, e)) : e です(再帰的定義はしません)。 E の「次の時代」 E' E' = E \cup \{e'\} とします。

fun (  v_1, v_2, \cdots , v_n ) =  x の値

無名関数を表します。 v_1, v_2, \cdots , v_n は変数、 x は式です。
 \mathrm{val}(e, \operatorname{fun} (v_1, v_2, \cdots , v_n) = x) = \mathrm{val}(e, λ( (v_1, v_2, \cdots , v_n) . x, e))
です。

if  x then  y else  z の値

 x y z は式です。 \mathrm{val}(e, \operatorname{if} x \operatorname{then} y \operatorname{else} z) \mathrm{val}(e, x) T (「真」を表す定数)のとき  \mathrm{val}(e, y) \mathrm{val}(e, x) T ではないとき  \mathrm{val}(e, z) となります。

ラムダ計算と無限ラムダ多項式(12)

有限の場合から無限の場合へ

有限の場合(任意の再帰的定義の関数の呼び出しの深さが有限の回数  n 以内の場合)、関数定義、無名関数、クロージャーを取り除くことができて、式の値は以前定義した「一般マグマの多項式」のような形にすることができます。

これの無限の場合(任意の  n の場合)について考えることがこの記事の目的となります。

ラムダ計算と無限ラムダ多項式(11)

有限の場合のポインター除去

再帰的定義の関数が有限の回数で終わるとき、再帰的定義がない形に書き直すことができます。C# で階乗を求める関数で考えてみます。

        private int fac(int n)
        {
            if (n == 1)
            {
                return 1;
            }
            else
            {
                return n * fac(n - 1);
            }
        }

関数呼び出しの深さが3回以内の場合、以下のように書き直すことができます。

        private int fac1(int n)
        {
            return 1;
        }
        private int fac2(int n)
        {
            if (n == 1)
            {
                return 1;
            }
            else
            {
                return n * 1;
            }
        }
        private int fac3(int n)
        {
            if (n == 1)
            {
                return 1;
            }
            else
            {
                if (n - 1 == 1)
                {
                    return n * 1;
                }
                else
                {
                    return n * (n - 1) * 1;
                }
            }
        }

このように書き直すと、再帰的定義を含まない形にすることができます。また同様に、関数の呼び出しを含まない形にすることができます。

こうすることによって以下のような有限個のステートメントからなるブロックに書き直すことができます。これに以下のように上から順に番号を付けます。これを時刻と呼ぶことにします。

            {
                statement(); // 1
                statement(); // 2
                {
                    statement(); // 3
                    statement(); // 4
                    if (cond())
                    {
                        statement(); // 5
                        statement(); // 6
                    }
                    else
                    {
                        statement(); // 7
                        statement(); // 8
                    }
                    statement(); // 9
                    statement(); // 10
                }
                statement(); // 11
                statement(); // 12
            }

前回の集合  A は時刻ごとに存在するとします。これを  A_t とします。 A_t の元は  \langle (v \mapsto x) , e \rangle という形とします。 v は変数、 x は式、 e \in A_t は環境です。時刻  t に次の時刻  t' があるとします。

let  v =  x のとき

 A_{t'} = A_t \cup \{ \langle (v \mapsto x) , e \rangle \} とします。def のときも同様です。