4 deleted 20 characters in body edited Jan 13 '18 at 1:31 Aristu 1,35744 gold badges99 silver badges1919 bronze badges EDIT: Thanks to @ljedrz Comment. Before doing the reduction is worth noting that: $$(\lambda n f x . n ~ f (f ~ x)) = (\lambda n f x .((n f) (f ~ x)))$$ This is a convention, the parenthesis always associate to the left It can be reduced further, but I advise you to change the second expression to an $$\alpha$$-equivalent one. $$\Big(\big(\lambda n f x . (n ~ f) (f ~ x) \big) ~ (\lambda h y . y) \Big)$$ This might not be necessary in this specific problem, but might also save you some headache later trying to keep track if some free variables got captured. \begin{align*} \Big(\big(\lambda \color{red}{n} f x . \color{red}{n} ~ f (f ~ x)\big) ~ \color{red}{(\lambda h y . y)} \Big) &\rightarrow_\beta \big[n ~ / ~(\lambda h y . y)\big] \big(\lambda f x . n ~ f (f ~ x)\big)\\ &\rightarrow_{\alpha} \big( \lambda f x. (\lambda h y. y) ~ f ~ (f~x) \big)\\ \Big( \lambda f x. \big((\lambda \color{red}{h} y. y) ~ \color{red}{f}\big) ~ (f~x) \Big) &\rightarrow_{\beta} \Big(\lambda f x.\big[h ~ / ~ f \big]\big(\lambda y.y\big) ~ (f ~ x) \Big)\\ \Big( \lambda f x. ((\lambda y. y)) ~ (f~x) \Big) &\rightarrow_{\beta} \Big(\lambda f x.\big[y ~ / ~ (f ~ x)\big]\big(\lambda y.y\big)\Big)\\ &\rightarrow_{\alpha} \Big(\lambda f x. (f ~ x) \Big) \end{align*}\begin{align*} \Big(\big(\lambda \color{red}{n} f x . \color{red}{n} ~ f (f ~ x)\big) ~ \color{red}{(\lambda h y . y)} \Big) &\rightarrow_\beta \big[n ~ / ~(\lambda h y . y)\big] \big(\lambda f x . n ~ f (f ~ x)\big)\\ &\rightarrow_{\alpha} \big( \lambda f x. (\lambda h y. y) ~ f ~ (f~x) \big)\\ \Big( \lambda f x. \big((\lambda \color{red}{h} y. y) ~ \color{red}{f}\big) ~ (f~x) \Big) &\rightarrow_{\beta} \Big(\lambda f x.\big[h ~ / ~ f \big]\big(\lambda y.y\big) ~ (f ~ x) \Big)\\ \Big( \lambda f x. ((\lambda y. y)) ~ (f~x) \Big) &\rightarrow_{\beta} \Big(\lambda f x.\big[y ~ / ~ (f ~ x)\big]y\Big)\\ &\rightarrow_{\alpha} \Big(\lambda f x. (f ~ x) \Big) \end{align*} Which cannot be reduced further. EDIT: Thanks to @ljedrz Comment. Before doing the reduction is worth noting that: $$(\lambda n f x . n ~ f (f ~ x)) = (\lambda n f x .((n f) (f ~ x)))$$ This is a convention, the parenthesis always associate to the left It can be reduced further, but I advise you to change the second expression to an $$\alpha$$-equivalent one. $$\Big(\big(\lambda n f x . (n ~ f) (f ~ x) \big) ~ (\lambda h y . y) \Big)$$ This might not be necessary in this specific problem, but might also save you some headache later trying to keep track if some free variables got captured. \begin{align*} \Big(\big(\lambda \color{red}{n} f x . \color{red}{n} ~ f (f ~ x)\big) ~ \color{red}{(\lambda h y . y)} \Big) &\rightarrow_\beta \big[n ~ / ~(\lambda h y . y)\big] \big(\lambda f x . n ~ f (f ~ x)\big)\\ &\rightarrow_{\alpha} \big( \lambda f x. (\lambda h y. y) ~ f ~ (f~x) \big)\\ \Big( \lambda f x. \big((\lambda \color{red}{h} y. y) ~ \color{red}{f}\big) ~ (f~x) \Big) &\rightarrow_{\beta} \Big(\lambda f x.\big[h ~ / ~ f \big]\big(\lambda y.y\big) ~ (f ~ x) \Big)\\ \Big( \lambda f x. ((\lambda y. y)) ~ (f~x) \Big) &\rightarrow_{\beta} \Big(\lambda f x.\big[y ~ / ~ (f ~ x)\big]\big(\lambda y.y\big)\Big)\\ &\rightarrow_{\alpha} \Big(\lambda f x. (f ~ x) \Big) \end{align*} Which cannot be reduced further. EDIT: Thanks to @ljedrz Comment. Before doing the reduction is worth noting that: $$(\lambda n f x . n ~ f (f ~ x)) = (\lambda n f x .((n f) (f ~ x)))$$ This is a convention, the parenthesis always associate to the left It can be reduced further, but I advise you to change the second expression to an $$\alpha$$-equivalent one. $$\Big(\big(\lambda n f x . (n ~ f) (f ~ x) \big) ~ (\lambda h y . y) \Big)$$ This might not be necessary in this specific problem, but might also save you some headache later trying to keep track if some free variables got captured. \begin{align*} \Big(\big(\lambda \color{red}{n} f x . \color{red}{n} ~ f (f ~ x)\big) ~ \color{red}{(\lambda h y . y)} \Big) &\rightarrow_\beta \big[n ~ / ~(\lambda h y . y)\big] \big(\lambda f x . n ~ f (f ~ x)\big)\\ &\rightarrow_{\alpha} \big( \lambda f x. (\lambda h y. y) ~ f ~ (f~x) \big)\\ \Big( \lambda f x. \big((\lambda \color{red}{h} y. y) ~ \color{red}{f}\big) ~ (f~x) \Big) &\rightarrow_{\beta} \Big(\lambda f x.\big[h ~ / ~ f \big]\big(\lambda y.y\big) ~ (f ~ x) \Big)\\ \Big( \lambda f x. ((\lambda y. y)) ~ (f~x) \Big) &\rightarrow_{\beta} \Big(\lambda f x.\big[y ~ / ~ (f ~ x)\big]y\Big)\\ &\rightarrow_{\alpha} \Big(\lambda f x. (f ~ x) \Big) \end{align*} Which cannot be reduced further. 3 added 414 characters in body edited Jan 12 '18 at 16:58 Aristu 1,35744 gold badges99 silver badges1919 bronze badges EDIT: Thanks to @ljedrz Comment. Before doing the reduction is worth noting that: $$(\lambda n f x . n ~ f (f ~ x)) = (\lambda n f x .((n f) (f ~ x)))$$ This is a convention, the parenthesis always associate to the left It can be reduced further, but I advise you to change the second expression to an $$\alpha$$-equivalent one. $$\Big(\big(\lambda n f x . n ~ f (f ~ x) \big) ~ (\lambda h y . y) \Big)$$$$\Big(\big(\lambda n f x . (n ~ f) (f ~ x) \big) ~ (\lambda h y . y) \Big)$$ This might not be necessary in this specific problem, but might also save you some headache later trying to keep track if some free variables got captured. \begin{align*} \Big(\big(\lambda \color{red}{n} f x . \color{red}{n} ~ f (f ~ x)\big) ~ \color{red}{(\lambda h y . y)} \Big) &\rightarrow_\beta \big[n ~ / ~(\lambda h y . y)\big] \big(\lambda f x . n ~ f (f ~ x)\big)\\ &\rightarrow_{\alpha} \big( \lambda f x. (\lambda h y. y) (f(f~x)) \big)\\ \big( \lambda f x. (\lambda \color{red}{h} y. y) \color{red}{(f(f~x))} \big) &\rightarrow_{\beta} \Big(\lambda f x.\big[h ~ / ~ (f(f~x))\big]\big(\lambda y.y\big)\Big)\\ &\rightarrow_{\alpha} \lambda f x . (\lambda y.y) \end{align*}\begin{align*} \Big(\big(\lambda \color{red}{n} f x . \color{red}{n} ~ f (f ~ x)\big) ~ \color{red}{(\lambda h y . y)} \Big) &\rightarrow_\beta \big[n ~ / ~(\lambda h y . y)\big] \big(\lambda f x . n ~ f (f ~ x)\big)\\ &\rightarrow_{\alpha} \big( \lambda f x. (\lambda h y. y) ~ f ~ (f~x) \big)\\ \Big( \lambda f x. \big((\lambda \color{red}{h} y. y) ~ \color{red}{f}\big) ~ (f~x) \Big) &\rightarrow_{\beta} \Big(\lambda f x.\big[h ~ / ~ f \big]\big(\lambda y.y\big) ~ (f ~ x) \Big)\\ \Big( \lambda f x. ((\lambda y. y)) ~ (f~x) \Big) &\rightarrow_{\beta} \Big(\lambda f x.\big[y ~ / ~ (f ~ x)\big]\big(\lambda y.y\big)\Big)\\ &\rightarrow_{\alpha} \Big(\lambda f x. (f ~ x) \Big) \end{align*} Which cannot be reduced further. It can be reduced further, but I advise you to change the second expression to an $$\alpha$$-equivalent one. $$\Big(\big(\lambda n f x . n ~ f (f ~ x) \big) ~ (\lambda h y . y) \Big)$$ This might not be necessary in this specific problem, but might also save you some headache later trying to keep track if some free variables got captured. \begin{align*} \Big(\big(\lambda \color{red}{n} f x . \color{red}{n} ~ f (f ~ x)\big) ~ \color{red}{(\lambda h y . y)} \Big) &\rightarrow_\beta \big[n ~ / ~(\lambda h y . y)\big] \big(\lambda f x . n ~ f (f ~ x)\big)\\ &\rightarrow_{\alpha} \big( \lambda f x. (\lambda h y. y) (f(f~x)) \big)\\ \big( \lambda f x. (\lambda \color{red}{h} y. y) \color{red}{(f(f~x))} \big) &\rightarrow_{\beta} \Big(\lambda f x.\big[h ~ / ~ (f(f~x))\big]\big(\lambda y.y\big)\Big)\\ &\rightarrow_{\alpha} \lambda f x . (\lambda y.y) \end{align*} Which cannot be reduced further. EDIT: Thanks to @ljedrz Comment. Before doing the reduction is worth noting that: $$(\lambda n f x . n ~ f (f ~ x)) = (\lambda n f x .((n f) (f ~ x)))$$ This is a convention, the parenthesis always associate to the left It can be reduced further, but I advise you to change the second expression to an $$\alpha$$-equivalent one. $$\Big(\big(\lambda n f x . (n ~ f) (f ~ x) \big) ~ (\lambda h y . y) \Big)$$ This might not be necessary in this specific problem, but might also save you some headache later trying to keep track if some free variables got captured. \begin{align*} \Big(\big(\lambda \color{red}{n} f x . \color{red}{n} ~ f (f ~ x)\big) ~ \color{red}{(\lambda h y . y)} \Big) &\rightarrow_\beta \big[n ~ / ~(\lambda h y . y)\big] \big(\lambda f x . n ~ f (f ~ x)\big)\\ &\rightarrow_{\alpha} \big( \lambda f x. (\lambda h y. y) ~ f ~ (f~x) \big)\\ \Big( \lambda f x. \big((\lambda \color{red}{h} y. y) ~ \color{red}{f}\big) ~ (f~x) \Big) &\rightarrow_{\beta} \Big(\lambda f x.\big[h ~ / ~ f \big]\big(\lambda y.y\big) ~ (f ~ x) \Big)\\ \Big( \lambda f x. ((\lambda y. y)) ~ (f~x) \Big) &\rightarrow_{\beta} \Big(\lambda f x.\big[y ~ / ~ (f ~ x)\big]\big(\lambda y.y\big)\Big)\\ &\rightarrow_{\alpha} \Big(\lambda f x. (f ~ x) \Big) \end{align*} Which cannot be reduced further. 2 deleted 6 characters in body edited Jan 12 '18 at 3:38 Aristu 1,35744 gold badges99 silver badges1919 bronze badges It can be reduced further, but I advise you to change the second expression to an $$\alpha$$-equivalent one. $$\Big(\big(\lambda n f x . n ~ f (f ~ x) \big) ~ (\lambda h y . y) \Big)$$ This might not be necessary in this specific problem, but might also save you some headache later trying to keep track if one of thesome free variables got captured. \begin{align*} \Big(\big(\lambda \color{red}{n} f x . \color{red}{n} ~ f (f ~ x)\big) ~ \color{red}{(\lambda h y . y)} \Big) &\rightarrow_\beta \big[n ~ / ~(\lambda h y . y)\big] \big(\lambda f x . n ~ f (f ~ x)\big)\\ &\rightarrow_{\alpha} \big( \lambda f x. (\lambda h y. y) (f(f~x)) \big)\\ \big( \lambda f x. (\lambda \color{red}{h} y. y) \color{red}{(f(f~x))} \big) &\rightarrow_{\beta} \Big(\lambda f x.\big[h ~ / ~ (f(f~x))\big]\big(\lambda y.y\big)\Big)\\ &\rightarrow_{\alpha} \lambda f x . (\lambda y.y) \end{align*} Which cannot be reduced further. It can be reduced further, but I advise you to change the second expression to an $$\alpha$$-equivalent one. $$\Big(\big(\lambda n f x . n ~ f (f ~ x) \big) ~ (\lambda h y . y) \Big)$$ This might not be necessary in this specific problem, but might also save you some headache later trying to keep track if one of the free variables got captured. \begin{align*} \Big(\big(\lambda \color{red}{n} f x . \color{red}{n} ~ f (f ~ x)\big) ~ \color{red}{(\lambda h y . y)} \Big) &\rightarrow_\beta \big[n ~ / ~(\lambda h y . y)\big] \big(\lambda f x . n ~ f (f ~ x)\big)\\ &\rightarrow_{\alpha} \big( \lambda f x. (\lambda h y. y) (f(f~x)) \big)\\ \big( \lambda f x. (\lambda \color{red}{h} y. y) \color{red}{(f(f~x))} \big) &\rightarrow_{\beta} \Big(\lambda f x.\big[h ~ / ~ (f(f~x))\big]\big(\lambda y.y\big)\Big)\\ &\rightarrow_{\alpha} \lambda f x . (\lambda y.y) \end{align*} Which cannot be reduced further. It can be reduced further, but I advise you to change the second expression to an $$\alpha$$-equivalent one. $$\Big(\big(\lambda n f x . n ~ f (f ~ x) \big) ~ (\lambda h y . y) \Big)$$ This might not be necessary in this specific problem, but might also save you some headache later trying to keep track if some free variables got captured. \begin{align*} \Big(\big(\lambda \color{red}{n} f x . \color{red}{n} ~ f (f ~ x)\big) ~ \color{red}{(\lambda h y . y)} \Big) &\rightarrow_\beta \big[n ~ / ~(\lambda h y . y)\big] \big(\lambda f x . n ~ f (f ~ x)\big)\\ &\rightarrow_{\alpha} \big( \lambda f x. (\lambda h y. y) (f(f~x)) \big)\\ \big( \lambda f x. (\lambda \color{red}{h} y. y) \color{red}{(f(f~x))} \big) &\rightarrow_{\beta} \Big(\lambda f x.\big[h ~ / ~ (f(f~x))\big]\big(\lambda y.y\big)\Big)\\ &\rightarrow_{\alpha} \lambda f x . (\lambda y.y) \end{align*} Which cannot be reduced further. 1 answered Jan 12 '18 at 2:37 Aristu 1,35744 gold badges99 silver badges1919 bronze badges