An interesting analogy. Extending that, what we want to explicitly avoid is simple alpha reduction (where we simply replace one variable with another (unbound) variable). Extending the analogy to cover eta reduction is probably a bit of a stretch, or at least I can’t see a meaningful way to do so.
Replacing the symbol with what it signifies? In CS terms, this is “beta reduction”, no?
An interesting analogy. Extending that, what we want to explicitly avoid is simple alpha reduction (where we simply replace one variable with another (unbound) variable). Extending the analogy to cover eta reduction is probably a bit of a stretch, or at least I can’t see a meaningful way to do so.