Lambda calculus reductions

Page 1 of 1

4 Replies - 2152 Views - Last Post: 10 January 2013 - 08:44 AM

#1 Mike+9

Reputation: 13
• Posts: 104
• Joined: 10-July 12

Lambda calculus reductions

Posted 08 January 2013 - 02:11 AM

Hello DIC! I have tried for a couple of hours to learn about lambda calculus for an exam I have in 2 days and I keep on getting stuck at some reductions and substitutions. Here are some examples:

```(^f g x. f x (g x))(^x y. x)(^x y. x)
```

with ^ being lambda.
The result should be ^x. x
What I have tried so far and got to a result:

-do an alfa reduction for the 2 x's at the end with z = (^z y. z)
-replace f with (^z y. z) and I get this: (^g x. ((^z y. z)) x (g x))(^z y. z)
-the I replace g with (^z y. z) and get: (^x. ((^z y. z)) x ((^z y. z) x))
-now I replace both z's with x and get: (^x. (^y. x) (^y. x))
-now since I do not have a y in the first (^y. x) I can get rid of the second (^y. x) and get finally: ^x. x

I got the right answer but I am not 100% sure it's OK how I did it. If anyone could point out if there are any errors I would appreciate it.

The second one which I can't seem to get is this:

```(^y. x (^x. x))[(^y. y x)/x]
```

Here I am supposed to substitute x with (^y. y x). The book states that in cases like this I should rename some variables so they do not affect the expression. But I'm really confused and don't know which one. I would go for the y first because if I would substitute the first x with the expression after it that y would become bound.

If anyone could explain this example a bit that would be great.

Is This A Good Question/Topic? 0

Replies To: Lambda calculus reductions

#2 mojo666

Reputation: 352
• Posts: 770
• Joined: 27-June 09

Re: Lambda calculus reductions

Posted 08 January 2013 - 08:04 PM

Quote

-do an alfa reduction for the 2 x's at the end with z = (^z y. z)
-replace f with (^z y. z) and I get this: (^g x. ((^z y. z)) x (g x))(^z y. z)
-the I replace g with (^z y. z) and get: (^x. ((^z y. z)) x ((^z y. z) x))
-now I replace both z's with x and get: (^x. (^y. x) (^y. x))
-now since I do not have a y in the first (^y. x) I can get rid of the second (^y. x) and get finally: ^x. x

I got the right answer but I am not 100% sure it's OK how I did it. If anyone could point out if there are any errors I would appreciate it.

Your wording is a little hand-wavy, but your methodology is correct. For example, it would be clearer in the last step to first perform an alpha reduction

(^x. (^y. x) (^z. t))

Then perform a beta reduction substituting all occurences of y with (^z. t) leaving (^x. x)

It is important to show why you can "just get rid of the second (^y. x)" instead of merely stating that you are doing it.

Quote

```(^y. x (^x. x))[(^y. y x)/x]
```

Here I am supposed to substitute x with (^y. y x). The book states that in cases like this I should rename some variables so they do not affect the expression. But I'm really confused and don't know which one. I would go for the y first because if I would substitute the first x with the expression after it that y would become bound.

In this example, renaming is not necessary. You only need to rename if the substituting expression contains a free variable that would become bound upon performing the substitution. The only free variable in (^y. y x) is the x and it will not be bound to anything when you perform the substitution.

This post has been edited by mojo666: 08 January 2013 - 08:05 PM

#3 Mike+9

Reputation: 13
• Posts: 104
• Joined: 10-July 12

Re: Lambda calculus reductions

Posted 08 January 2013 - 10:24 PM

Yeah, the last step is should practically be 2 steps, I got that now. What I tried to say is that I first try to replace y in the first (^y. x), and since there is no y there I should get:

```(^x. x)
```

But your way with the alpha conversion first is way better and easier to understand.

Thanks a lot for the help! I've also read some tutorials and some courses online and got the hang of it.

mojo666, on 08 January 2013 - 08:04 PM, said:

Quote

```(^y. x (^x. x))[(^y. y x)/x]
```

Here I am supposed to substitute x with (^y. y x). The book states that in cases like this I should rename some variables so they do not affect the expression. But I'm really confused and don't know which one. I would go for the y first because if I would substitute the first x with the expression after it that y would become bound.

In this example, renaming is not necessary. You only need to rename if the substituting expression contains a free variable that would become bound upon performing the substitution. The only free variable in (^y. y x) is the x and it will not be bound to anything when you perform the substitution.

So, when I want to replace x with (^y. y x) I would have to replace both x's in the main expression? This would be one of the things I still do not know for sure.

#4 mojo666

Reputation: 352
• Posts: 770
• Joined: 27-June 09

Re: Lambda calculus reductions

Posted 09 January 2013 - 01:02 PM

Quote

So, when I want to replace x with (^y. y x) I would have to replace both x's in the main expression? This would be one of the things I still do not know for sure.

When performing a substitution, you can only substitute free variables. In the expression (^y. x (^x. x)), the first x is the only free variable. The second x is bound to ^x so you cannot substitute it. Doing so would change the definition of the expression. It is the equivalent of doing the following

```//turning this
function foo1(x)  //(^x.x)
{
return x;
}

//into this
function foo1(x) //(^x.(^y.y x))
{
function foo2(y)
{
return y x;
}
return foo2(y)
}

```

This post has been edited by mojo666: 09 January 2013 - 04:27 PM

#5 Mike+9

Reputation: 13
• Posts: 104
• Joined: 10-July 12

Re: Lambda calculus reductions

Posted 10 January 2013 - 08:44 AM

Got it. Thanks a lot for the help. I had the exam today and I did pretty good.