Only supports reducing applying a function to a variable.
Good start.
When you’re doing that deep replace, don’t you have to check for the same variable name you’re reducing away appearing in a lambda expression inside the expression you’re reducing?
Not sure how to interpret those words, I’m guessing “don’t replace (\a. x (\a.a))y with x (\y.y),” which is invalid anyway i think. edit: Maybe “don’t replace (\a. a a)(\a.a) with (\a. (\a.a) (\a.a))?” Yeah that makes more sense edit 2: wait “don’t replace (\y x.y y)(\x.x) with \x. (\x. x)(\x. x)” makes more sense
Yeah. You don’t have to look at what’s surrounding the inner lambda, just know that inside that inner lambda that variable name means this variable and can’t be substituted. So your recursive deep replace has to have another input, initially empty, which is a list of variables protected against substitution.