Избегание захвата - это предотвращение захвата свободных переменных.«Захват» связанных переменных не повредит так сильно: в
λx.(λf.λx.fx)((λf.λx.fx)x)
два использования x действительно являются разными переменными, но это уже закодировано в термине: В общем,новая абстракция в подтерме будет «перезаписывать» привязку дальнейших внешних абстракций. Это просто из-за того, как работает оценка лямбда-терминов: если есть новая абстракция над той же переменной, то старая абстракция будет дальшев конечном итоге он потеряет свой эффект в подтерме с новой абстракцией, и переменные, связанные внутренней абстракцией, будут эффективно отличаться от переменных, связанных только внешней абстракцией.
Вы можете попробовать это: если вы примените λx.(λf.λx.fx)((λf.λx.fx)x) к какому-либо термину N, то, согласно определению бета-сокращения, этот термин будет уменьшен до (λf.λx.fx)((λf.λx.fx)x)[N/x], т.е. термин, полученный путем замены каждогосвободный (!) вхождение x в (λf.λx.fx)((λf.λx.fx)x) на N (подстановка действует только для свободных переменных по определению).Единственное свободное вхождение x в этом термине является самым последним;другие два x в двух подтермах (λf.λx.fx) связаны их соответствующими λx.Таким образом, единственным x, который будет заменен на N, является последний, следовательно, (λx.(λf.λx.fx)((λf.λx.fx)x))N уменьшится до (λf.λx.fx)((λf.λx.fx)N) - границы x в подтермах (λf.λx.fx) остаются неизменными.
Таким образом, x, связанные внутренней абстракцией и x в конце термина, действительно являются различными переменными, принадлежащими к различным абстракциям.Поэтому не переименовывать их во время применения.
При этом иногда бывает полезно сделать такие переименования для облегчения чтения.Полученный термин будет альфа-конгруэнтным с термином, полученным прямой заменой без переименования.