flatlineの日記跡地

■[CS] Church Numeralsのベキ乗が分からない

pow = λm n. n m とか謎過ぎる... λm n. n (λl s. m (l s)) (λs z. s z) なら分かるんだけど．つまり times m を one に対し n 回適用するの．

分からないので pow two three を手計算*1してみた：

Applicative:

three two = (λs z. s (s (s z))) (λs z. s (s z))
= λz. (λs w. s (s w)) ((λs w. s (s w)) ((λs w. s (s w)) z))
= λz. (λs w. s (s w)) ((λs w. s (s w)) (λw. z (z w)))
= λz. (λs w. s (s w)) (λw. (λx. z (z x)) ((λx. z (z x)) w))
= λz. (λs w. s (s w)) (λw. (λx. z (z x)) (z (z w)))
= λz. (λs w. s (s w)) (λw. z (z (z (z w))))
= λz w. (λx. z (z (z (z x)))) ((λx. z (z (z (z x)))) w)
= λz w. (λx. z (z (z (z x)))) (z (z (z (z w))))
= λz w. z (z (z (z (z (z (z (z w)))))))

WHNF:

three two = (λs z. s (s (s z))) (λs z. s (s z))
= λz. (λs w. s (s w)) ((λs w. s (s w)) ((λs w. s (s w)) z))

Normal:

three two = (λs z. s (s (s z))) (λs z. s (s z))
= λz. (λs w. s (s w)) ((λs w. s (s w)) ((λs w. s (s w)) z))
= λz w. ((λs x. s (s x)) ((λs x. s (s x)) z)) (((λs x. s (s x)) ((λs x. s (s x)) z)) w)
= λz w. (λx. ((λs y. s (s y)) z) (((λs y. s (s y)) z) x)) (((λs x. s (s x)) ((λs x. s (s x)) z)) w)
= λz w. ((λs y. s (s y)) z) (((λs y. s (s y)) z) (((λt u. t (t u)) ((λt u. t (t u)) z)) w))
= λz w. (λy. z (z y)) (((λs y. s (s y)) z) (((λt u. t (t u)) ((λt u. t (t u)) z)) w))
= λz w. z (z (((λs y. s (s y)) z) (((λt u. t (t u)) ((λt u. t (t u)) z)) w)))
= λz w. z (z ((λy. z (z y)) (((λt u. t (t u)) ((λt u. t (t u)) z)) w)))
= λz w. z (z (z (z (((λt u. t (t u)) ((λt u. t (t u)) z)) w))))
= λz w. z (z (z (z ((λu. ((λt v. t (t v)) z) (((λt v. t (t v)) z) u)) w))))
= λz w. z (z (z (z (((λt v. t (t v)) z) (((λt v. t (t v)) z) w)))))
= λz w. z (z (z (z ((λv. z (z v)) (((λt v. t (t v)) z) w)))))
= λz w. z (z (z (z (z (z (((λt v. t (t v)) z) w))))))
= λz w. z (z (z (z (z (z ((λv. z (z v)) w))))))
= λz w. z (z (z (z (z (z (z (z w)))))))

何ら直感的なものが見えてこないんですが．