We can more or less start, right?

There is no tradition of waiting too long, is there?

Before I forgot, we're moving to another room tomorrow, which is E1-12.

This is 7.

You will find it, hopefully.

I also know that until the end of the semester on Wednesdays.

Okay, back to the leftovers from the previous lecture.

This is a short version of the substitution.

What I proposed this time was correct until this place, I guess.

So basically, this closes the standard and this one is more or less straightforward because

we're trying to substitute x and x was bound here.

So the result of the substitution at the original term.

And the tricky case is this one.

Hopefully, I wrote it down correctly.

Z, y, t, x, yes.

So I mean the problem with this capture word in substitution is you need to rename the

variable so you first need to say what renaming is, but renaming is also a kind of substitution

but for a variable.

So instead of doing it in two steps, introducing your naming, introducing substitution on top

of it, and just do it in one go.

And I defined this clause like this.

So I repeat the substitution twice, but that substitution is defined in the previous clauses

because the previous clauses, they completely specify substitution for variables.

And here I only replace variables.

Well, okay, here I replace the variable and here I replace this variable by a term.

So basically the argument is that the term I apply the substitution is smaller than the

original term, modulo alpha equivalence.

So hence this notion is well defined.

So I hope you see why we needed this to substitution because if I just wanted to replace x by t

and p, then t could contain the currencies of y and I don't want them to be captured

by this lambda.

So I rename this y to z and replace this lambda y by lambda z.

And then I can substitute x by y because now I know that the term doesn't contain y.

Example.

So if you just take this definition and try to calculate something like this.

So here's the situation precisely the one of interest because we replace y here by the

application yx.

And I don't want this y to be captured.

No, I don't want this x to be captured.

Right?

Hence, I'm using this last clause to reduce it to lambda z.

So I introduce a new variable z and then I substitute.

And then my result is lambda z yx z.

Here.

Second from the top.

So this.

Yes, yes, that's correct.

Thank you.

Right, then I had to get back to the reduction rules which I explained and I need to correct

myself.