0

$ + = λmnab.m a((n a) b)$
I have to show that $2 + 3 \triangleright_\beta $ 5
what I understand from the lambda expression of + is that it takes
4 arguments m, n , a , b But when I have to evaluate $2 + 3$, I only have $2$ arguments
How do I go about evaluating it.

Amit wadhwa
  • 13
  • When you pass two arguments to a function that expects four arguments, the result is a function that expects the remaining two arguments. – frabala Mar 24 '21 at 07:52

1 Answers1

0

I guess, the numbers here are Church numerals: \begin{align} 2 &= \lambda f.\lambda x. f (f x) \\ 3 &= \lambda f.\lambda x. f (f (f x)) \end{align} Applying the first argument (numeral 2) to addition, we get: $$\begin{split} & (\lambda m n a b.ma ((na)b))(\lambda fx. f (f x))&~~~~~~~~~\text{($\beta$-reduction)}\\ \to~ & \lambda n a b.((\lambda fx. f (f x))a) ((na)b) \end{split}$$ Applying the second argument (numeral 3) to the above result, we get: $$\begin{split} & \big(\lambda n a b.((\lambda fx. f (f x))a) ((na)b)\big)\bigl(\lambda fx. f(f (f x))\bigr)&~~~~~~~~~\text{($\beta$-reduction)}\\ \to~ & \lambda a b.((\lambda fx. f (f x))a) (((\lambda fx. f(f (f x)))a)b) \end{split}$$

frabala
  • 3,732
  • thanks. Also is this call-by-value reduction ? I am kind of confused between call by value and call by name – Amit wadhwa Mar 24 '21 at 09:38
  • @Amitwadhwa Yes, it is call-by-value. Say you have an application $e_1, e_2$. In both reduction strategies you have to first reduce $e_1$ to a lambda expression. Once $e_1$ is reduced to some function, in call-by-name you perform the $\beta$-reduction immediately, while in call-by-value you have to also reduce $e_2$ before doing the $\beta$-reduction. In your exercise though, the arguments are already irreducible (they are functions), so even with call-by-value, the $\beta$-reduction happens immediately. – frabala Mar 24 '21 at 09:53
  • @Amitwadhwa If my answer is satisfactory, please consider upvoting it and/or accepting it. – frabala Mar 24 '21 at 09:54
  • done. I have one more doubt. In lambda xor = (x (y F T) y). Now I could easily show xor T F = T by writing like (T (F F T) F) = (T T F) = T . But I have to do it using call by name reduction could you provide some pointers to it? – Amit wadhwa Mar 24 '21 at 10:33
  • @Amitwadhwa In call-by-name, the reduction would be (T (F F T) F) = (F F T) = T. – frabala Mar 24 '21 at 10:53
  • Thanks a lot for your help. I really appreciate it – Amit wadhwa Mar 24 '21 at 11:13