de Bruijn Indexの練習問題
-
2022_AW_12 の 0起源のde Bruijn Indexの定義に基づく。
-
記号はTAPLの6章を使っているが、TAPLの定義とは異なる。
-
演習問題はTAPLから。結果は異なる箇所がある。
0. de Bruijn Index とは
それぞれのλでは引数の名前を書かない。引数は、通常の記法でその引数を宣
言するλが、なん階層だけ外側にあるかを表す自然数の番号で表記する。
例えば、$ \lambda z.(\lambda y. y (\lambda x. x)) (\lambda x. z x) $ は、$ \lambda(\lambda 0 (\lambda 0)) (\lambda 1 0) $ となる。
自由変数は、それ以降の自然数を順番に付与する。
演習
$ \lambda x. x (\lambda y. y x) $
$ \lambda a. b a $
$ \lambda b. b a $
$ b (\lambda x. \lambda y. b) $
$ \lambda b. b (\lambda x. \lambda y. b) $
λx. λy. x
λx. λy. λz. x z (y z)
λz. (λy. y (λx. x)) (λx. z x)
1. シフト
$ \uparrow^d_k n = n $ ただし $n \lt k $
$ \uparrow^d_k n = n+d $ ただし $n \ge k $
$ \uparrow^d_k(\lambda e) = \lambda\uparrow^d_{k+1} e $
$ \uparrow^d_k(e_1 e_2) = (\uparrow^d_k e_1)(\uparrow^d_k e_2) $
演習 6.2.2 (1)
$ \uparrow^2_0(\lambda\lambda 1 (0 2)) $
演習 6.2.2 (2)
$ \uparrow^2_0 (\lambda 0 1 (\lambda 0 1 2)) $
2. 代入
$ [k \mapsto u]k = u $
$ [k \mapsto u]n = n-1 $ ただし、$ k \lt n $
$ [k \mapsto u]n = n $ ただし、$ k \gt n $
$ [k \mapsto u] (\lambda e) = \lambda [k+1 \mapsto\uparrow^1_0u]e $
$ [k \mapsto u] (e_1 e_2) = ([k \mapsto u]e_1)([k \mapsto u]e_2) $
演習 6.2.5 (1)
$ [0 \mapsto 1] (0 (\lambda\lambda 2))) $
演習 6.2.5 (2)
$ [0\mapsto 1\lambda 2] (0\lambda 1) $
演習 6.2.5 (3)
$ [0\mapsto 1] (\lambda 0 2) $
演習 6.2.5 (4)
$ [0\mapsto 1] (\lambda 1 0) $
3. 評価
$ (\lambda e_1)e_2 = [0\mapsto e_2]e_1 $
例 6.3
$ (\lambda((1 0)2))(\lambda 0) $
答え
0. de Bruijn Index とは
演習
$ \lambda x. x (\lambda y. y x) $ は、$ \lambda 0 (\lambda 0 1) $
$ \lambda a. b a $ は、$ \lambda 1 0 $
$ \lambda b. b a $ は、$ \lambda 0 1 $
$ b (\lambda x. \lambda y. b) $ は、 $ 0 (\lambda\lambda 2) $
$ \lambda b. b (\lambda x. \lambda y. b) $ は、 $ \lambda 0 (\lambda\lambda 2) $
λx. λy. x is λλ1
λx. λy. λz. x z (y z) is λλλ2 0(1 0)
λz. (λy. y (λx. x)) (λx. z x) is λ(λ0(λ0))(λ1 0)
1. シフト
演習 6.2.2 (1)
$ \uparrow^2_0(\lambda\lambda 1 (0 2)) $
$ = \lambda(\uparrow^2_1\lambda(1 (0 2))) $
$ = \lambda\lambda(\uparrow^2_2 (1 (0 2))) $
$ = \lambda\lambda((\uparrow^2_2 1) ((\uparrow^2_2 0) (\uparrow^2_2 2))) $
$ = \lambda\lambda(1(0 4)) $
演習 6.2.2 (2)
$ \uparrow^2_0 (\lambda 0 1 (\lambda 0 1 2)) $
$ = \lambda (\uparrow^2_1 (0 1 (\lambda 0 1 2))) $
$ = \lambda (\uparrow^2_1 0)(\uparrow^2_1 1) (\uparrow^2_1(\lambda 0 1 2)) $
$ = \lambda 0 3 (\lambda \uparrow^2_2(0 1 2)) $
$ = \lambda 0 3 (\lambda (\uparrow^2_2 0)(\uparrow^2_2 1)(\uparrow^2_2 2)) $
$ = \lambda 0 3 (\lambda 0 1 4) $
2. 代入
演習 6.2.5 (1)
$ [0 \mapsto 1] (0 (\lambda\lambda 2))) $
$ = ([0 \mapsto 1]0)([0 \mapsto 1] (\lambda\lambda 2)) $
$ = ([0 \mapsto 1]0)(\lambda[1 \mapsto\uparrow^1_0 1]\lambda 2) $
$ = ([0 \mapsto 1]0)(\lambda\lambda[2 \mapsto\uparrow^2_0 1] 2) $
$ = ([0 \mapsto 1]0)(\lambda\lambda[2 \mapsto 3] 2) $
$ = 1 (\lambda\lambda 3) $
演習 6.2.5 (2)
$ [0\mapsto 1\lambda 2] (0\lambda 1) $
$ = ([0\mapsto 1\lambda 2]0)([0\mapsto 1\lambda 2]\lambda 1) $
$ = ([0\mapsto 1\lambda 2]0)(\lambda[1\mapsto\uparrow^1_0 1\lambda 2] 1) $
$ = (1\lambda 2) (\lambda(2\lambda 3)) $
ただし、
$ \uparrow^1_0 1\lambda 2 $
$ = (\uparrow^1_0 1)(\uparrow^1_0 \lambda 2) $
$ = (\uparrow^1_0 1)\lambda(\uparrow^1_1 2) $
$ = 2 \lambda 3 $
演習 6.2.5 (3)
$ [0\mapsto 1] (\lambda 0 2) $
$ = \lambda [1\mapsto\uparrow^1_0 1] (0 2) $
$ = \lambda [1\mapsto 2] (0 2) $
$ = \lambda ([1\mapsto 2]0) ([1\mapsto 2]2) $
$ = \lambda 0 (2-1) $
$ = \lambda 0 1 $
演習 6.2.5 (4)
$ [0\mapsto 1] (\lambda 1 0) $
$ = \lambda [1\mapsto\uparrow^1_0 1] (1 0) $
$ = \lambda [1\mapsto 2] (1 0) $
$ = \lambda ([1\mapsto 2]1)([1\mapsto 2]0) $
$ = \lambda 2 0 $
3. 評価
例 6.3
$ (\lambda((1 0)2))(\lambda 0) $
$ = [0\mapsto \lambda 0] ((1 0)2) $
$ = (([0\mapsto \lambda 0] 1)([0\mapsto \lambda 0] 0))([0\mapsto \lambda 0] 2) $
$ = ((1-1)(\lambda 0))(2-1) $
$ = (0(\lambda 0))1 $
以上