4 ms·
λ calculus is left associative - that is, a sequence of applications A B C is interpreted as (A B) C, so we first reduce (λf x. f (f x)) (λy.* 2 y), yielding λx
by icen 10y ago
λ calculus is left associative - that is, a sequence of applications A B C is interpreted as (A B) C, so we first reduce (λf x. f (f x)) (λy.* 2 y), yielding λx . (λy. * 2 y) ((λy.2 * y) x), and only then apply 5 to it, which finally lets us unravel everything and get 20.