Lambda Calculus Reduction steps
Lambda calculus
Lambda calculus has a way of spiraling into a lot of steps, making solving problems tedious, and it can look real hard, but it isn't actually that bad. In lambda calculus, there are only lambdas, and all you can do with them is substitution. Lambdas are like a function or a method - if you are familiar with programming, they are functions that take a function as input, and return a new function as output.
There are basically two and a half processes in lambda calculus:
1) Alpha Conversion - if you are applying two lambda expressions with the same variable name inside, you change one of them to a new variable name. For example (λx.xx)(λx.x) becomes something like (λx.xx)(λy.y) or (λx.xx)(λx'.x') after reduction. The result is equivalent to what you start out with, just with different variable names.
2) Beta Reduction - Basically just substitution. This is the process of calling the lambda expression with input, and getting the output. A lambda expression is like a function, you call the function by substituting the input throughout the expression. Take (λx.xy)z, the second half of (λx.xy), everything after the period, is output, you keep the output, but substitute the variable (named before the period) with the provided input. z is the input, x is the parameter name, xy is the output. Find all occurrences of the parameter in the output, and replace them with the input and that is what it reduces to, so (λx.xy)z => xy with z substituted for x, which is zy.
2.5) Eta Conversion/Eta Reduction - This is special case reduction, which I only call half a process, because it's kinda Beta Reduction, kinda, as in technichally it's not. You may see it written on wikipedia or in a textbook as "Eta-conversion converts between λx.(f x) and f whenever x does not appear free in f", which sounds really confusing. All that really means is λx.(f x) = f if f does not make use of x. if It actually makes complete sense but is better shown through an example. Consider (λx.(λy.yy)x), this is equivalent through eta reduction to (λy.yy), because f = (λy.yy), which does not have an x in it, you could show this by reducing it, as it would solve to (λx.xx), which is observably the same thing. You said to focus on beta reduction, and so I am not going to discuss eta conversion in the detail it deserves, but plenty of people gave their go at it on the cs theory stack exchange
On the Notation for Beta Reduction:
I'm going to use the following notation for substituting the provided input into the output:
(λ param . output)input => output [param := input] => result
This means we substitute occurrences of param in output, and that is what it reduces down to
Example:
(λx.xy)z
= (xy)[x:=z]
= (zy)
= zy
Enough theory, let's solve this. Lambda Calculus is good fun.
The problem you came up with can be solved with only Alpha Conversion, and Beta Reduction, Don't be daunted by how long the process below is. It's pretty long, no doubt, but no step in solving it is real hard.
(λxyz.xyz)(λx.xx)(λx.x)x
= (((λxyz.xyz)(λx.xx))(λx.x))x - Let's add the parenthesis in "Normal Order", left associativity, abc reduces as ((ab)c), where b is applied to a, and c is applied to the result of that
= (((λxyz.xyz)(λx.xx))(λx.x))x - Select the deepest nested application and reduce that first.
The bolded section reduces as:
(λxyz.xyz)(λx.xx)
= (λx.λyz.xyz)(λx.xx) - means the same thing, but we pull out the first parameter since we are going to reduce it away and so I want it to be clear
= (λx.λyz.xyz)(λx'.x'x') - Alpha conversion, some people stick to new letters, but I like appending numbers at the end or `s, either way is fine. Because both expressions use the parameter x we have to rename them on one side, because the two Xs are local variables, and so do not have to represent the same thing.
= (λyz.xyz)[x := λx'.x'x'] - Notation for a beta reduction, we remove the first parameter, and replace it's occurrences in the output with what is being applied [a := b] denotes that a is to be replaced with b.
= (λyz.(λx'.x'x')yz) - The actual reduction, we replace the occurrence of x with the provided lambda expression.
= (λyz. ((λx'.x'x')y) z) - Normal order for parenthesis again, and look, another application to reduce, this time y is applied to (λx'.x'x'), so lets reduce that now
= (λyz. ((x'x')[x' := y]) z) - Put this into notation for beta reduction.
= (λyz. (yy) z) - we swap the two occurrences of x'x' for Ys, and this is now fully reduced.
Add this back into the original expression:
(((λxyz.xyz)(λx.xx))(λx.x))x
= ((λyz.(yy)z)(λx.x))x - This is not new, just putting what we found earlier back in.
= ((λyz.(yy)z)(λx.x))x - Grab the deepest nested application, it is of (λx.x) applied to (λyz.(yy)z)
We'll solve this out separately again:
(λyz.(yy)z)(λx.x)
= (λy.λz.(yy)z)(λx.x) - Just bringing the first parameter out for clarity again.
= (λz.(yy)z)[y := (λx.x)] - Put into beta reduction notation, we pop out the first parameter, and note that Ys will be switched for (λx.x)
= (λz.((λx.x)(λx.x))z) - The actual reduction/substitution, the bolded section can now be reduced
= (λz.((x)[x := λx.x])z) - Hopefully you get the picture by now, we are beginning to beta reduce (λx.x)(λx.x) by putting it into the form (x)[x := λx.x]
= (λz.((λx.x))z) - And there is the substitution
= (λz.(λx.x)z) - Cleaned off the excessive parenthesis, and what do we find, but another application to deal with
= (λz.(x)[x:=z]) - Pop the x parameter, put into notation
= (λz.(z)) - Perform the substitution
= (λz.z) - Clean off the excessive parenthesis
Put it back into the main expression:
((λyz.(yy)z)(λx.x))x
= ((λz.z))x - Filling in what we proved above
= (λz.z)x - cleaning off excessive parenthesis, this is now reduced down to one final application, x applied to(λz.z)
= (z)[z:=x] - beta reduction, put into notation
= (x) - make the substitution
= x - clean off the excessive parenthesis
So, yeah. The answer is x, it reduced down just groovy.
Just substitute thing for its corresponding thing:
(λxyz . x y z )(λx . xx )(λx . x )x
= _________________________ ~~~~~~~~~~
(λyz . (λx . x x )y z ) (λx . x )x
= _________ ~~~~~~~~~
(λz . (λx . x x )(λx . x )z ) x
= ___ ~~~
(λx . x x )(λx . x )x
= ________ ________ ~~~~~~~~~
(λx . x )(λx . x ) x
= ____ ~~~~~~~~~
(λx.x) x
= ___ ~~~
xBut really, what we have here is nothing more than just
IUIx = UIx = IIx = Ix = x
where Ux === xx and Ix === x by definition (and so, Ixy === xy and Ixyz === xyz as well).
See? It's a notation thing.