Skip to main content
Post Made Community Wiki
Source Link
Mike Shulman
  • 66.8k
  • 7
  • 162
  • 368

I don't think there is any solution to the problem as you pose it. Neil and Carl have mentioned the standard approach, which is to rename bound variables, whenever you perform a substitution, to avoid variable capture. This works, but it is tedious and error-prone if you have to write it down or implement it explicitly; for this reason I have heard it said that "variable binding is one of the most annoying aspects of formalizing anything." But you may be interested in some of the workarounds that smart people have come up with:

(People who know more about the subject than I do, please add and comment!)