ラムダ計算と無限ラムダ多項式(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'$ があるとします。