Please report here any issue you find with Bob’s lectures.
In lecture 3.1 I believe “rename” should only work on the free variables instead of recursively changing names of b.v. It should match “subst” on lambda abstractions. As was pointed out in the lecture it’s a special form of substitution after all.
I’m not sure we are on the page but here is my two cents: The renaming function rename(t, x, y) replaces all occurrences of x by y, whether free or bound. So it will change the term \x. x to \y. y. And if the variable x happens to be free it will be replaced by y as well, which is also free given y must be fresh.
Ah, I think you are right: given that the new variable is fresh the change should be safe. From the way it is used in subst, rename does not need to change any bound variables. But that is only a minor point.
1 Like