Yeah I don’t see much from this notation (I also find it hard to tell the difference between the result of an abstraction and an application which feels like a

Yeah I don’t see much from this notation (I also find it hard to tell the difference between the result of an abstraction and an application which feels like a somewhat important difference). I mostly wanted to suggest that diagrams or notation changes in general can be very useful. It’s true that variable renaming comes up in other parts of mathematics but scope matters a lot less in most other mathematics, so much so that it is basically implicit and left to be inferred based on the mathematical context. You wouldn’t normally rename a variable to avoid a conflict so much as you would avoid giving it a conflicting name in the first place. The recursive nature of the lambda calculus means you can’t avoid the problem this way.