ローダー数の再定式化

表示をデスクトップ版に切り替えて数式を表示する。

モチベーション[]

みんなが読み慣れた形式でローダー数を定義したかったので，してみた．うまくいっているか不安なので，バグの指摘を歓迎します．

なお，この記事で定義される数はloader.cの出力と一致しません．あくまでもCoCの対角化を「C言語で512文字以内」という縛り無しで定義する場合こうなるだろう，というものです．

再定式化[]

表記[]

集合\(T\)と\(V\)と\(K\)[]

任意の0を含む自然数\(n\)に対し，\(\bar{n} \in T \cap V\)である．
\(* \in T\cap K\)，\(\Box \in T\cap K\)である．
任意の\(M \in T\)と\(N \in T\)に対し，\(\lambda M.N \in T\)である．
任意の\(M \in T\)と\(N \in T\)に対し，\(\Pi M.N \in T\)である．
任意の\(M \in T\)と\(N \in T\)に対し，\((M\,N) \in T\)である．

\(T\)はCoCの項全体，\(V\)はde Brujin indices，\(K\)はソートに対応する．

集合\(C\)[]

\([] \in C\)である．
任意の\(M \in T\)と\(\Gamma \in C\)に対し，\(\Gamma|M \in C\)である．

\(T\)はCoCの文脈全体に対応する．

集合\(J\)[]

\(\otimes \in J\)である．
任意の\(M \in T\)と\(N \in T\)と\(\Gamma \in C\)に対し，\(\Gamma \vdash M:N \in J\)である．

\(J\)はCoCの判断全体に対応する．\(\otimes\)は無効な判断を表す．

\([]\vdash *:\Box \equiv \mathrm{Ax}\)と定義する．これは公理に対応する．

集合\(S\)[]

\([] \in S\)である．
任意の\(t \in S\)に対し，\(\mathrm{var}(t) \in S\)である．
任意の\(s \in S\)と\(t \in S\)に対し，\(\mathrm{weak}(s, t) \in S\)である．
任意の\(s \in S\)と\(t \in S\)に対し，\(\mathrm{abst}(s, t) \in S\)である．
任意の\(t \in S\)に対し，\(\mathrm{form}(t) \in S\)である．
任意の\(s \in S\)と\(t \in S\)に対し，\(\mathrm{app}(s, t) \in S\)である．

\(S\)は証明に使われる推論ルールの木の全体に対応する．

関数[]

代入[]

3つの関数

\[\mathrm{Subst}: V\times T\times \{+1,-1\}\times T \to T\] \[\mathrm{Apply}: T\times T \to T\] \[\mathrm{Lift}: T\to T\]

を同時に再帰的に定める．

\(\mathrm{Subst}(\bar{n},y,c,t)\)の定義[]

\(t = \bar{m}\)なる\(m \in \mathbb{N}\)が存在するとき，
1. \(m = n\)のとき，\(\mathrm{Subst}(\bar{n},y,c,t) = y \)
2. \(m > n\)のとき，\(\mathrm{Subst}(\bar{n},y,c,t) = \overline{m+c} \)
3. \(m < n\)のとき，\(\mathrm{Subst}(\bar{n},y,c,t) = t \)
\(t = *\)または\(t = \Box\)のとき，\(\mathrm{Subst}(\bar{n},y,c,t) = t \)
\(t = (\lambda M.N)\)なる\(M\in T\)と\(N\in T\)が存在するとき，\(\mathrm{Subst}(\bar{n},y,c,t) = \lambda \mathrm{Subst}(\bar{n},y,c,M). \mathrm{Subst}(\overline{n+1},\mathrm{Lift}(y),c,N)\)
\(t = (\Pi M.N)\)なる\(M\in T\)と\(N\in T\)が存在するとき，\(\mathrm{Subst}(\bar{n},y,c,t) = \Pi \mathrm{Subst}(\bar{n},y,c,M). \mathrm{Subst}(\overline{n+1},\mathrm{Lift}(y),c,N)\)
\(t = (M\,N)\)なる\(M\in T\)と\(N\in T\)が存在するとき，\(\mathrm{Subst}(\bar{n},y,c,t) = \mathrm{Apply}(\mathrm{Subst}(\bar{n},y,c,M), \mathrm{Subst}(\bar{n},y,c,N))\)

\(\mathrm{Apply}(y,x)\)の定義[]

\(y = (\lambda M.N)\)なる\(M\in T\)と\(N\in T\)が存在するとき，\(\mathrm{Apply}(y,x) = \mathrm{Subst}(\bar{0},x,-1,N)\)
それ以外のとき，\(\mathrm{Apply}(y,x) = (y\, x)\)

\(\mathrm{Lift}(x)\)の定義[]

\(\mathrm{Lift}(x) = \mathrm{Subst}(\bar{0},\bar{1},+1,x)\)

これらの関数はCoCの項への代入と正規化を司る．CoCの強正規化性を使えばこれらの関数が計算可能であることを証明できるはず[I WIN]．

推論[]

\[\mathrm{Step}: J\times S \to J\] \[\mathrm{Infer}: S \to J\]

を同時に再帰的に定める．

\(\mathrm{Step}(j,q)\)の定義[]

\(j = \otimes\)のとき，\(\mathrm{Step}(j,q) = \otimes \)
\(j \neq \otimes\)のとき，\(j = \Gamma\vdash M:N\)なる\(M \in T\)と\(N \in T\)と\(\Gamma \in C\)をとる．
1. \(q = []\)のとき，\(\mathrm{Step}(j,q) = j \)
2. \(q = \mathrm{var}(t)\)なる\(t \in S\)が存在するとき，
  1. \(N \in K\)のとき，\(\mathrm{Step}(j,q) = \mathrm{Step}(\Gamma | M\vdash\bar{0}:\mathrm{Lift}(M), t)\)
  2. それ以外の時，\(\mathrm{Step}(j,q) = \otimes \)
3. \(q = \mathrm{weak}(s, t)\)なる\(s \in S\)と\(t \in S\)が存在し，\(\mathrm{Infer}(s) = \Delta\vdash A:B\)なる\(A \in T\)と\(B \in T\)と\(\Delta \in C\)が存在するとき，
  1. \(\Gamma = \Delta\)かつ\(B \in K\)のとき，\(\mathrm{Step}(j,q) = \mathrm{Step}(\Gamma|A\vdash \mathrm{Lift}(M):\mathrm{Lift}(N), t)\)
  2. それ以外の時，\(\mathrm{Step}(j,q) = \otimes \)
4. \(q = \mathrm{abst}(s, t)\)なる\(s \in S\)と\(t \in S\)が存在し，\(\mathrm{Infer}(s) = \Delta\vdash A:B\)なる\(A \in T\)と\(B \in T\)と\(\Delta \in C\)が存在するとき，
  1. \(\Gamma = \Delta\)かつ\(\Gamma \neq []\)かつ\(B \in K\)かつ\(N = A\)のとき，\(\Gamma = \Gamma' |Z\)なる\(Z \in T\)をとる．このとき，\(\mathrm{Step}(j,q) = \mathrm{Step}(\Gamma'\vdash \lambda Z.M:\Pi Z.N, t)\)
  2. それ以外の時，\(\mathrm{Step}(j,q) = \otimes \)
5. \(q = \mathrm{form}(t)\)なる\(t \in S\)が存在するとき，
  1. \(\Gamma \neq []\)かつ\(N \in K\)のとき，\(\Gamma = \Gamma' |A\)なる\(A \in T\)をとる．このとき，\(\mathrm{Step}(j,q) = \mathrm{Step}(\Gamma'\vdash \Pi A.M:N, t)\)
  2. それ以外の時，\(\mathrm{Step}(j,q) = \otimes \)
6. \(q = \mathrm{app}(s, t)\)なる\(s \in S\)と\(t \in S\)が存在し，\(\mathrm{Infer}(s) = \Delta\vdash A:B\)なる\(A \in T\)と\(B \in T\)と\(\Delta \in C\)が存在するとき，
  1. \(\Gamma = \Delta\)かつ\(N = \Pi B.Z\)なる\(Z \in T\)が存在するとき，\(\mathrm{Step}(j,q) = \mathrm{Step}(\Gamma\vdash \mathrm{Apply}(M,A):\mathrm{Subst}(\bar{0},A,-1,Z), t)\)
  2. それ以外の時，\(\mathrm{Step}(j,q) = \otimes \)

\(\mathrm{Infer}(q)\)の定義[]

\(\mathrm{Infer}(q) = \mathrm{Step}(\mathrm{Ax}, q)\)と定義する．

これらの関数は与えられた推論ルールに応じて判断を変形していく．ただし，ルールが適用できない形になっている場合は\(\otimes\)にする．\(q\)が「正しい証明」である場合にのみ\(\otimes\)でない判断が返る．

補助[]

\[\mathrm{Length}_T: T \to \mathbb{N}\]

\(t \in V \cup K \)のとき，\(\mathrm{Length}_T(t) = 1\)
\(t = (\lambda M.N)\)なる\(M\in T\)と\(N\in T\)が存在するとき，\(\mathrm{Length}_T(t)=\mathrm{Length}_T(M)+\mathrm{Length}_T(N)+1\)
\(t = (\Pi M.N)\)なる\(M\in T\)と\(N\in T\)が存在するとき，\(\mathrm{Length}_T(t)=\mathrm{Length}_T(M)+\mathrm{Length}_T(N)+1\)
\(t = (M\,N)\)なる\(M\in T\)と\(N\in T\)が存在するとき，\(\mathrm{Length}_T(t)=\mathrm{Length}_T(M)+\mathrm{Length}_T(N)+1\)

\[\mathrm{Length}_C: C \to \mathbb{N}\]

\(\Gamma = []\)のとき，\(\mathrm{Length}_C(\Gamma) = 0\)
\(\Gamma = \Gamma'|M\)なる\(M \in T\)が存在するとき，\(\mathrm{Length}_C(\Gamma) = \mathrm{Length}_C(\Gamma')+\mathrm{Length}_T(M)+1\)

\[\mathrm{Length}_J: J \to \mathbb{N}\]

\(j = \otimes\)のとき，\(\mathrm{Length}_J(j) = 0\)
\(j = \Gamma \vdash M:N\)なる\(M \in T\)と\(N \in T\)と\(\Gamma \in C\)が存在するとき，\(\mathrm{Length}_J(j) = \mathrm{Length}_C(\Gamma)+\mathrm{Length}_T(M)+\mathrm{Length}_T(N)+1\)

\[\mathrm{Length}_S: S \to \mathbb{N}\]

\(q = []\)のとき，\(\mathrm{Length}_S(q) = 0\)
\(q = \mathrm{var}|t\)または\(q = \mathrm{form}|t\)なる\(t \in S\)が存在するとき，\(\mathrm{Length}_S(q) = \mathrm{Length}_S(t)+1\)
\(q = \mathrm{weak}(s)|t\)または\(q = \mathrm{abst}(s)|t\)または\(q = \mathrm{app}(s)|t\)なる\(s \in S\)と\(t \in S\)が存在するとき，\(\mathrm{Length}_S(q) = \mathrm{Length}_S(s) + \mathrm{Length}_S(t)+1\)

これらの関数は文字数（っぽいもの）を数えているだけである．

巨大関数[]

\[\mathrm{Derive}: \mathbb{N} \to \mathbb{N}\]

\(\mathrm{Length}_S(q) \le x\)となるようなすべての\(q \in S\)を考えると，これは有限集合になる．これらの\(q\)について，\(\mathrm{Length}_J(\mathrm{Infer}(q))\)を足し上げたものを\(\mathrm{Derive}(x)\)と定義する．

ほとんどの\(q\)に対して\(\mathrm{Length}_J(\mathrm{Infer}(q)) = 0\)だが，\(q\)がチャーチ数についての巨大関数を構成して，巨大チャーチ数を作るような証明木になっている場合などに，\(\mathrm{Length}_J(\mathrm{Infer}(q))\)は巨大な数になる．短い証明木でCoC上で増加速度の速い関数が構成できれば，この関数の増加速度に直結する．

巨大数[]

\(\mathrm{Derive}^5(9^9)\)を弱ローダー数と定義する．また，この定義文自体をloader¬cと呼ぶことにする．

備考[]

Upquark11111氏のブログを大いに参考にしている．

CoC(Calculus of Construction)[]

CoCのinference ruleは次の6つである： \[ \frac{}{\Gamma \vdash * : \Box}(\text{axiom}) \]

\[ \frac{\Gamma \vdash X : K}{\Gamma, x : X \vdash x : X}(\text{variable}) \]

\[ \frac{\Gamma \vdash X:Y \quad \Gamma \vdash S:K}{\Gamma,x:S \vdash X:Y}(\text{weakening}) \]

\[ \frac{\Gamma, x:A \vdash X:Y \quad \Gamma \vdash (\Pi x:A.Y):K}{\Gamma \vdash (\lambda x:A.X):(\Pi x:A.Y)}(\text{abstraction}) \]

\[ \frac{\Gamma, x:A \vdash X : K}{\Gamma \vdash (\Pi:A.X):K}(\text{formation}) \]

\[ \frac{\Gamma \vdash X:(\Pi x:T.Z) \quad \Gamma \vdash S:T}{\Gamma \vdash (X \,\, S):Z[x:=S]}(\text{application}) \]

ただし，\( K \in \{*, \Box\} \)とする．

ローダーのオリジナルのプログラムでは，abstractionの二つ目の条件\(\Gamma \vdash (\Pi x:A.Y):K\)のチェックをしない．これにより，CoCでは型が付かないラムダ項が生成されてしまう．だが，これによってシステム全体が矛盾する（型\(\Pi P:*.P\)をもつ項が空の文脈から作れてしまう）ようなことはないらしい（正直よくわかっていない）．

この記事ではチェックするようにしているので，その分Derive関数は弱くなっている（「弱ローダー数」の由来はここ）

リファクタリングされたloader.c[]

Upquark11111氏のブログはとても分かりやすいが，ブログで参照されているプログラムはオリジナルのローダー氏による解説付きプログラム^[1]ではなく，Upquark11111氏によって書き直されたものであり，その全体プログラムが明示されていない．下にブログから筆者が復元し，追加コメントを加えたプログラムを掲載する．正確性を保証することはできない...

// accumlator: ここに列挙された判断を「足し上げ」ていく．
int acc = 0;

// returns pair <y, x>: 整数yとxのペアリング．
int Pair(y, x) {
    return (2*y+1) << x;
}

// right of pair: ペアの右側．2で何回割れるか数える．
int R(x) {
    if (x % 2 == 1) {
        return 0;
    } else {
        return 1 + R(x/2);
    }
}

// left of pair: ペアの左側．
// 2^R(x)で割ればよいが，それはビットシフトで実装できる．
int L(x) {
    return x/2 >> R(x);
}

// エンコード．
// de Brujin indexを使うので「束縛変数の名前」をエンコードする必要がない．
// PI(A,B) = <0,<A,B>>
// LAMBDA(A,B) = <1,<A,B>>
// APPLY(A,B) = <2,<A,B>>
// STAR = <3,0> = 7
// BOX = <3,1> = 14
// VAR(n) = <4+2n,0> = 9 + 4n [n >= 0]
// 空の文脈は0, Gamma,Aの形をした文脈は<A,Gamma>でエンコード．
// STARとBOXは2ビット目が1である唯一の項．
// VAR(n)のエンコードが奇妙なのはこのため．

// Substitute y for v in term, and normalise.  Variables > v get adjusted by
// -c.  [The precise normalisation is: if y and term are normal, and the
// substitution has a normal form, then the normal form is returned.]
// termに現れるvにyを代入し，正規化する．vよりde Brujin indexが大きい
// 変数はインデックスが-cされる．
int Subst(v, y, c, term)
{
    int aux = L(term);
    int x = R(term);

    if (aux == 2) {
        // APPLY
        return Apply(Subst(v, y, c, L(x)), Subst(v, y, c, R(x)));
    } else if (aux > 2) {
        if (aux == 4 + 2*v) {
            // substitute
            return y;
        } else if (aux > 4 + 2*v) {
            // shift
            return Pair(aux - 2*c, 0);
        } else {
            return term;
        }
    } else {
        // PI or LAMBDA
        // consider de Brujin indices
        return Pair(aux,
                    Pair(Subst(v, y, c, L(x)),
                         Subst(v+1, Lift(y), c, R(x))));
    }
}

// Increment the index of each variable in x.  Uses Subst.
// 項に現れるすべてのde Brujin indexを+1する．
int Lift(x) {
    return Subst(0, Pair(4 + 2*1, 0), -1, x);
}

// Apply y to x and normalise.  [Precisely, if y and x are normal, and
// y(x) is normalisable, Apply(y, x) returns the normal form of y(x).]
// yにxを適用する．yがラムダ式の場合ベータ簡約する．
// CoCの強正規化性から，この関数は停止する．
int Apply(y, x) {
    if (L(y) != 1) {
        return Pair(2, Pair(y, x));
    } else {
        // beta reduction of lambda
        return Subst(0, x, 1, R(R(y)));
    }
}

// Derive parses a bit stream into terms of CoC and normalises everything.  The
// outputs are accumulated into the variable acc.  We also recurse, so as to
// cover all the BitStreams which are < x.
// xをビット列と見做し，Axiomから始めて，CoCの推論ルールをビット列に伴って
// 適用していく．
int Derive(x) {
    int lem;
    int lem_type;
    int lem_term;
    int lem_context;

    int theorem;

    // axiom (Rule 1)
    //  :- STAR : BOX
    int context = 0; // context : empty
    int term = Pair(3, 0); // term : STAR
    int type = Pair(3, 1); // type : BOX

    // ビット列適用ループ
    while (1) {
        if (x > 0) {
            // recurse and accumlate its output
            // 再帰でx以下のビット列すべてについて数え上げる．
            // 計算結果はaccに累積される．
            Derive(x - 1);
        }

        // xの次のビットが0なら証明終了．
        if ((x /= 2) % 2 == 0) {
            // there is nothing to prove anymore
            break;
        }

        // 補題：推論ルールに必要な2つ目の判断．
        // 1つしかないルールでもとりあえず計算し，捨てる．
        // エンコードは <lem_term, <lem_type, <x, lem_context>>>
        lem = L(Derive(x));

        lem_term = L(lem);    // term of lemma
        lem_type = L(R(lem)); // type of lemma
        x = L(R(R(lem)));     // remained bit stream
        lem_context = R(R(R(lem_term))); // context of lemma

        // same context
        if (context == lem_context) {
            // If type == PI(lem_type, -)
            if (L(type) == 0 && L(R(type)) == lem_type && (x /= 2) % 2) {
                // application (Rule 6)
                //    Gamma  :- X : (PI T.Z),   S : T
                // => Gamma  :- (X S) : Z[0:=S]
                type = Subst(0, lem_term, 1, R(R(type)));
                term = Apply(term, lem_term);
            }

            // If type of lemma is STAR or BOX
            if ((x /= 2) % 2 && lem_type&2 == 1) {
                // weakening (Rule 3)
                //    Gamma     :- X : Y,   S : K
                // => Gamma, S  :- X : Y (X and Y is lifted)

                // It is safe to do this immediately after an APPLY above,
                // because APPLY does not change contexts.
                context = Pair(lem_term, context);
                term = Lift(term);
                type = Lift(type);
            }
        };

        // context is non-empty
        if (context) {
            if ((x /= 2) % 2) {
                if ((x /= 2) % 2 || type&2 == 0) {
                    // LAMBDA intro. (Rule 4) -- strong!
                    //    Gamma, A  :- X : Y
                    // => Gamma     :- (\A.X) : (PI A.Y)

                    // We allow LAMBDA introduction whenever the context is non-empty.
                    // This extension is a conservative extension of CoC.
                    // 一番難しい場所．実はここでCoCの限界を突破している．
                    term = Pair(1, Pair(L(context), term));
                    type = Pair(0, Pair(L(context), type));
                    context = R(context);
                } else {
                    // type is STAR or BOX
                    // PI form. (Rule 5)
                    //    Gamma, A  :- X : K
                    // => Gamma     :- (PI A.X) : K
                    term = Pair(0, Pair(L(context), term));
                    context = R(context);
                }
            }
        }

        // type is STAR or BOX
        if ((x /= 2) % 2 && type&2 == 1) {
            // variable (Rule 2)
            //    Gamma     :- X : K
            // => Gamma, X  :- x : X
            context = Pair(term, context);
            type = Lift(term);
            term = Pair(4, 0);
        }
    }

    // theorem = <term, <type, <remained_bit_stream, context>>>
    theorem = Pair(term, Pair(type, Pair(x, context)));
    // acc = <therem, acc>
    acc = Pair(theorem, acc);
    return acc;
}

int main() {
    return Derive(Derive(Derive(Derive(Derive(99)))));
}

↑ https://github.com/rcls/busy

[1] ttps://github.com/rcls/busy

[1]