Lambda Calculus Reduction steps

Question

I am studying Lambda Calculus and I am stuck at Reduction.... Can anyone explain the types of reduction with this example, especially beta reduction in the simplest way possible. Also wouldn't mind an easy to understand tutorial.

(λxyz .xyz )(λx .xx )(λx .x )x

Answer 1

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.

Answer 2

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
=                   ___                  ~~~
                     x

But 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.

Answer 3

Terminology:

• reduction = Reduction is a model for computation that consists of a set of rules that determine how a term is stepped forwards.
• alpha-equivalence = when two terms are equal modulo the name of bound variables e.g. lambda x. x === lambda x. y but the body alone x !== y since these specifically say they are different symbolic objects...unless u cheat and do x=y (ok seems alpha reduction terminology does not exist)
• beta-reduction = reduction by function application i.e. (?x.e1) e2 = e1[ x := e2 ].

---

Refs:

• beta-red wiki: https://en.wikipedia.org/wiki/Lambda_calculus#%CE%B2-reduction
• nice website on beta: https://prl.ccs.neu.edu/blog/2016/11/02/beta-reduction-part-1/

---

What is ?-reduction? More generally, what is reduction? Reduction is a model for computation that consists of a set of rules that determine how a term is stepped forwards. ?-reduction is reduction by function application. When you ?-reduce, you remove the ? from the function and substitute the argument for the function’s parameter in its body. More formally, we can define ?-reduction as follows:

(?x.e1) e2 = e1[ x := e2 ]

---

?-reduction The ?-reduction rule states that an application of the form {\displaystyle (\lambda x.t)s}(\lambda x.t)s reduces to the term {\displaystyle t[x:=s]}t[x:=s]. The notation {\displaystyle (\lambda x.t)s\to t[x:=s]}(\lambda x.t)s\to t[x:=s] is used to indicate that {\displaystyle (\lambda x.t)s}(\lambda x.t)s ?-reduces to {\displaystyle t[x:=s]}t[x:=s]. For example, for every {\displaystyle s}s, {\displaystyle (\lambda x.x)s\to x[x:=s]=s}(\lambda x.x)s\to x[x:=s]=s. This demonstrates that {\displaystyle \lambda x.x}\lambda x.x really is the identity. Similarly, {\displaystyle (\lambda x.y)s\to y[x:=s]=y}(\lambda x.y)s\to y[x:=s]=y, which demonstrates that {\displaystyle \lambda x.y}\lambda x.y is a constant function.

The lambda calculus may be seen as an idealized version of a functional programming language, like Haskell or Standard ML. Under this view, ?-reduction corresponds to a computational step. This step can be repeated by additional ?-reductions until there are no more applications left to reduce. In the untyped lambda calculus, as presented here, this reduction process may not terminate. For instance, consider the term {\displaystyle \Omega =(\lambda x.xx)(\lambda x.xx)}\Omega =(\lambda x.xx)(\lambda x.xx). Here {\displaystyle (\lambda x.xx)(\lambda x.xx)\to (xx)[x:=\lambda x.xx]=(x[x:=\lambda x.xx])(x[x:=\lambda x.xx])=(\lambda x.xx)(\lambda x.xx)}(\lambda x.xx)(\lambda x.xx)\to (xx)[x:=\lambda x.xx]=(x[x:=\lambda x.xx])(x[x:=\lambda x.xx])=(\lambda x.xx)(\lambda x.xx). That is, the term reduces to itself in a single ?-reduction, and therefore the reduction process will never terminate.

Another aspect of the untyped lambda calculus is that it does not distinguish between different kinds of data. For instance, it may be desirable to write a function that only operates on numbers. However, in the untyped lambda calculus, there is no way to prevent a function from being applied to truth values, strings, or other non-number objects.