FANDOM


プログラムA

         c - r || (
            L ( u) || L ( r) - f ||
            (x /= 2) % 2 && ( u = S (4, d, 4, r ),
                   t = A (t, d) ),
            f / 2 & (x /= 2) % 2 && ( c = P ( d, c ),
                              t = S(4,13,-4, t ),
                              u = S(4,13,-4, u) )
             ),

プログラムB

         c && (x /= 2) % 2 && (
            t = P (
               ~u & 2 | (x /= 2) % 2 && (
                  u = 1 << P ( L ( c ), u) ),
               P ( L ( c ), t) ),
            c = r ),

プログラムC

         u / 2 & (x /= 2) % 2 && (
            c = P ( t, c ),
            u = S(4,13,-4, t ),
            t = 9 );

Aで適用、Bで依存型を生成、Cで折り返し(?)。依存型を生成してから適用に入る。

S (v, y, c, t)
{
   int
      f = L ( t ),
      x = r;
   { return
         f - 2 ?
         f > 2 ?
         f - v ? t - (f > v) * c : y :
         P ( f, P ( S (v, y, c, L ( x) ),
                          S (v+2, t = S(4,13,-4, y ), c, Z (x) )))
         :
         A (S (v, y, c, L ( x) ),
                S (v, y, c, Z (x) ) );}
}
A (y, x)
   { return L ( y) - 1
      ? 5 << P ( y, x)
      : S (4, x, 4, Z (r) );}

vで書き換える変数の番号を指定する。yは適用する目的対象(ツリー)。cは4で変数の番号を1ずつ下げる、-4で1ずつ上げる。tは関数(ツリー)

エンコード

P(0,P(A,B)) PI 依存型?

P(1,P(A,B)) LABMDA λ式?

P(2,P(A,B)) APPLY 適用

P(3,0) STAR 型変数?

P(3,1) BOX 高階の型(カインド)の変数?

P(4n+1,0) n=0,1,2,... VAR(n) 変数?

cは文脈 tは項 uは型

解析

なにかしらの形で与えられた関数を与えられた数だけ繰り返す関数と後者関数(関数fを追加する)が存在する、或いは生成できるはず。できなければならない。

簡略化

loader.c風のε_0 お召し上がりください

int r, a;
P ( y, x)
   { return y - ~y << x;
}
Z (x)
   { return r = x % 2 ? 0 : 1 + Z (x / 2 );}
L ( x)
   { return x / 2 >> Z (x );}

S (v, y, c, t)
{
   int
      f = L ( t ),
      x = r;
   { return
         f - 2 ?
         f > 2 ?
         f - v ? t - (f > v) * c : y :
         P ( f, P ( S (v, y, c, L ( x) ),
                          S (v+2, t = S(4,13,-4, y ), c, Z (x) )))
         :
         A (S (v, y, c, L ( x) ),
                S (v, y, c, Z (x) ) );}
}
A (y, x)
   { return L ( y) - 1
      ? 5 << P ( y, x)
      : S (4, x, 4, Z (r) );}

D (x)
{
xが0の場合はsucc(0)を返す。
D(x-1)からtとuを抽出しそれぞれdとfとする。
fにuを適用、関数の強化。
強化されたuにdを適用。
a=P(P(t,u),a)とでも
}
main ()
   { return D (D (D (D (D (99)))) );}

依存型とwhileループを除いてCoCを単純型付ラムダ計算まで弱めた表現を対角化した強さ、ε_0の強さになるはず。

広告ブロッカーが検出されました。


広告収入で運営されている無料サイトWikiaでは、このたび広告ブロッカーをご利用の方向けの変更が加わりました。

広告ブロッカーが改変されている場合、Wikiaにアクセスしていただくことができなくなっています。カスタム広告ブロッカーを解除してご利用ください。