Lambda calculus beta reduction variables

Question

I have the following expression:

(((\x y -> x y (\z -> z + 1)) 5)

Besides that I have the following formula:

I (think) I know how to reduce it correctly:

((\y -> y)(\z -> z + 1) 5) 

((\y -> y)6)

(6)

But then I don't understand how to fill in the variables stated in the formula. I don't understand where to put what and the why behind it. Besides this example I have another one with the following expression:

(\x y x -> ( (y z) x) )5

With the following formula:

Again I think I know how to reduce it:

(\y -> (y z) 5))

(5 z)

But then I again I don't know how to fill in the variables.

Could anyone help me out to fill in the variables and besides that explain me why that variable should have it's value

Answer 1

The first formula means: if you have an application (t u), you first reduce t to a value t', which should be a function. Then you reduce u to a value u', which will be the argument to the function, and then you make the function call. In your first code snippet the parentheses are not balanced. Let's suppose that what you intended to write was:
((\x y -> x y) (\z -> z + 1) 5)
The first step is to call the function (\x y -> x y) with two arguments, and get
((\z -> z + 1) 5)
Then you pass 5 to the function that adds 1, so the result is 6.

The second formula is saying that when you want to do a function call, you substitute the argument for the function's formal parameter in the function body. So, you change the xs to us in t. In this step, you need to be a little careful to avoid variable capture. Take a look at capture-avoiding substitution.