I was reading = in these two boxes more like a mere syntactic renaming, but the = on p.26 looks a lot more like a reduction in context. But probably it’s the same idea, just with more stuff.

Yes, just more stuff. I view the top box as defining a relation with the elaborate name FV(_)= and the second relation with the even more elaborate name _[_ <- _]=.

(I hope the copy I’m looking at has the right page numbers. My normal copies are on campus.)

Yes, that makes perfect sense!

But then for _[_ <- _]=, wouldn’t it be more correct if the box was defining the mere relation (just replacing = with some R ), and then say that the equality is obtained by …-closure? In particular, the box doesn’t say that it’s reflexive for example. (Of course it would make it more difficult for the reader.)

I would say that the _[_ <- _]= relation is between three terms (or a tuple of three terms, of you prefer) and one term, so it’s domain and range are not the same; it won’t be an equality relation. That is, not just the = would be replaced by a simpler R, but the whole _[_ <- _]=. In any case, I agree that = is used in many different ways, perhaps unhelpfully even if traditionally.

Ok, that’s a lot clearer now. Thank you

So, writing the relation _[_ <- _]R in predicate form, this would be: R( [X1, X1, M], M) R( [X2, X1, M], X2) if X1≠X2 R( [λX1.M1, X1, M2], λX1.M1) R( [λX1.M1, X2, M2], M4) where R( [λX3.M1, X1, X3], M3) and R( [M3, X2, M2], M4), if X1≠X2, X3 ∉ FV(λX1.M1), X3 ∉ FV(M2) R( [(M1 M2), X, M3], (M4 M5) ) where R( [M1, X, M3], M4) and R( [M2, X, M3], M5) As you say, the domain and ranges are not the same, but this can easily be fixed by replacing all last arguments M with, say, [M, ε, ε] where ε <- ε is the identity element for substitutions.