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)))))))
何ら直感的なものが見えてこないんですが.
*1:ここでサクッとevaluatorが書けない/書いたこともない辺りが私の限界を示している.