53

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
7
  • The wikipedia article on lambda calculus beta reduction is simple to understand. Dec 7, 2015 at 18:58
  • 1
    @rp.beltran (λx.xx) does not imply recursion. there's no calling of self there, only calling a thing with itself as its argument. only if that thing (x) calls its argument (x), will there be a recursion i.e. calling (by x) of self (x). in short what we have there is IUIx = UIx = IIx = Ix = x (where Ix === x and Ux === xx).
    – Will Ness
    Dec 29, 2020 at 19:49
  • 1
    @WillNess good catch! I 100% agree. In other words while (λx.xx) is a frequent way of introducing recursion, it is not recursion itself, and there are cases where (λx.xx) appears without any recursion happening at all.
    – rp.beltran
    Dec 29, 2020 at 20:23
  • 1
    @rp.beltran right. like UI = II = I while UU = UU = UU = ... or BU(CBU)f = U(CBUf) = U(BfU) = BfU(BfU) = f(U(BfU)) = ... = f(f(U(BfU))) = ....
    – Will Ness
    Dec 29, 2020 at 20:32

4 Answers 4

168

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.

5
  • 7
    it would be nice to see that tutorial in community wiki.
    – anon
    Nov 14, 2017 at 18:35
  • 1
    @BulatM. why? why shouldn't a user that authored 99+% of the content not get reputation points for it? am I misunderstanding something?
    – Will Ness
    Dec 29, 2020 at 19:55
  • Great job. Just a little thought though, shouldn't "abc reduces as ((ab)c), where b is applied to a" actually be "a is applied to b?". This might save a head twist ergonomically as more instances are used through out the answer. In LISP it's like this IMHO (as we are talking about functional programming) ONE=(add1 ZERO) //apply function add1 to zero TWO=(add1 (add1 ZERO))**//apply add1 to ZERO to get a new value, then apply add1 to the new value to deduce TWO. Also in math, **with X->Y, f(x)=y implies f maps x (when applied) onto y.
    – Mustafa R
    Aug 19, 2021 at 5:54
  • what does the term reduction mean more generally in PLFM theory? Mar 4, 2022 at 18:23
  • I agree with Mustafa's point about my wording. I'll edit my answer when I have some time. As for what "reduction means in the most general sense" I think it's just being used in the sense described by wikipedia as "In mathematics, reduction refers to the rewriting of an expression into a simpler form" en.wikipedia.org/wiki/Reduction_(mathematics). When we perform reduction in Lambda Calculus it's just a rewrite of the same formula (though technically this could be said of most maths as even replacing 2*3 with 6 is just a simpler representation of the same value.
    – rp.beltran
    Mar 16, 2022 at 19:38
3

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.

0

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:


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.

0

Well, first: the notion "substitution" is redundant and is not needed. It can be eliminated by simply treating β-reduction as a definition ... of substitution, rather than as a rule. Instead, the clauses that go into the usual definition of substitution are moved over into the replacements for the β-rule.

To state them, properly, requires first the notion of a "free variable" set. Given a λ-term A, the set of variables occurring freely in a λ-term shall be denoted ∂A. This can be defined recursively by:

    ∂x = {x},
    ∂(BC) = ∂B ∪ ∂C,
    ∂(λx·A) = ∂A - {x},

where x denotes a variable, and A, B and C denote λ-terms.

In place of the β-rule are the following rules:

    βI:     (λx·x) D = D,
    βK:     (λx·y) D = y, for all variables y ≠ x,
    βS:     (λx·B C) D = ((λx·B) D) ((λx·C) D),
    βλ1:    (λx·λx·A) D = λx·A,
    βλ2:    (λx·λy·A) D = λy·(λx·A) D, if y ∉ {x} ∪ ∂D,
    βλ3:    (λx·λy·A) D = λz·(λx·(λy·A) z) D, if z ∉ {x,y} ∪ ∂A ∪ ∂D,

where x, y, z denote variables, A, B, C and D denote λ-terms.

Where the βλ rules overlap, they are applied in the precedence order βλ1, or else βλ2, or else βλ3.

In place of the α-rule is the following rewritten version of it:

    α:      λx·A = λz·(λx·A) z,

where x and z are arbitrary variables and A is a λ-term. Written this way, it is now a special case of the η-rule:

    η:      λx·A x = A, if x ∉ ∂A.

So, if the η-rule is included, then the α-rule will also become redundant.

Let I = λx·x and D = λx·x x. Then, your expression is:

    (λx·λy·λz·x y z) D I x
    (λy·(λx·λz·x y z) D) I x, by βλ2
    (λy·λz·(λx·x y z) D) I x, by βλ2
    (λy·λz·((λx·x) D) ((λx·y) D) ((λx·z) D)) I x, by βS
    (λy·λz·D ((λx·y) D) ((λx·z) D)) I x, by βI
    (λy·λz·D y z) I x, by βK
    (λz·(λy·D y z)I) x, by βλ2
    (λz·((λy·D) I) ((λy·y) I) ((λy·z) I)) x, by βS
    (λz·((λy·D) I) I ((λy·z) I)) x, by βI
    (λz·D I z) x, by βK
    ((λz·D) x) ((λz·I) x) ((λz·z) x), by βS
    ((λz·D) x) ((λz·I) x) x, by βI
    D I x, by βK
    (λx·x x) I x, by the definition of D
    ((λx·x) I) ((λx·x) I) x, by βS
    I I x, by βI
    (λx·x) I x, by the definition of I
    I x, by βI
    (λx·x) x, by the definition of I
    x, by βI

It's not meant to be used as an algorithm, because of how much it micromanages the structure of the terms, but to just make the point that you can do this rigorously by a fixed set of axioms without making any use of any notion of substitution. It's nothing but β's (well ... except with a little sprinkling of α's and/or η's).

The combinator engine Combo, which I put up on GitHub, dodges the substitution issue by turning everything into combinators. The λ-term you presented gets compiled as I D I x, and reduces as

    I D I x ⇒ D I x ⇒ I I x ⇒ I x ⇒ x.

The only reductions it actually does are

    I D ⇒ D,        D I ⇒ I I,      I I ⇒ I,        I x ⇒ x

and from that, alone, it concludes that I D I x ⇒ x, by context.

Not the answer you're looking for? Browse other questions tagged or ask your own question.