I will repair a few issues about the recent lecture.

I looked up the spelling of Christopher Strachey.

This is the coinventor of the indentation semantic together with Donnuskott.

I wanted to detail a bit on the substitution.

We have been discussing untyped lambda calculus.

So that lambda calculus that I presented previously, it's called untyped lambda calculus.

Because it's very simple, it doesn't contain any types.

And it's historically the first version has been developed by mathematicians very long

time ago when people didn't use types extensively like now.

So I refer to free and bound variables and I didn't precisely say what it means.

So the notion of free variables is defined recursively over the term structure.

So we say that free of x, so this is like an operator which we apply to a term and

it returns the set of free variables.

So the free variables of a variable is the set containing this variable only.

And there are three variables of an application, as t say, and these are free s union with

free t.

And the third clause is the interesting one, lambda x s, this is free s minus x.

So here we remove this x from the set of free variables of s.

And so by definition, A very s free n t if

x belongs to free t and a variable is bound in t if x doesn't belong to free t.

So and this explains why lambda is also called a binder.

So we've got a variable which we bind with lambda and hence is bound.

Alright and then there is the substitution, this capture awarding substitution I have

been talking about and formal definition looks like this.

So if we have a variable and we substitute this variable with a term then we get this

term unconditionally.

And if we have a variable x and we substitute another variable with some term t then the

result is again x provided that x is not equal to y.

So these are the boring clauses and the interesting ones are like this, s t.

This is equal to what?

This is also fairly boring.

And then we have lambda x t s equal to.

2 x, 2 is not equal to 1.

Does it look correct?

I just found a definition in the book.

Now it looks suspicious actually.

Nope.

Perhaps this is wrong, right?

Yes, so right, it doesn't have the effect that we wanted because we do not want an occurrence of Y and S to be bound here.

So right, just the wrong definition, apparently a book on lambda calculus may contain a definition of non-capture avoiding substitution.

I should have checked it.

Couldn't you just fix this?

Yeah, you can fix it. The problem is when you try to design the right definition on your own, you always run through dead ends every time.

So you can design it, but it takes time because you remember one thing, then some other thing happens.

So it's some iteration, so I didn't want to spend time on it because I wanted to just take the definition that is ready to use.

Perhaps we need to postpone it to the next lecture again when I find it because I thought it was the capture avoiding, but it's not capture avoiding.

Yeah, it's a good topic for an exercise, but I didn't want to spend time on this. I just wanted to present it.

Sorry, just let's assume for the time being that the right definition exists and yeah, I need to postpone it until the next lecture, I think.

Yeah, anyway, let's just assume that we have a right notion. We can suitably rename the variables and I mean this definition can work too if you rename the variables properly.

It just doesn't work in a general case.