Alpha Conversion Definition

One of the three rewrite rules of lambda calculus , in which a bound variable of a lambda term gets replaced by another variable across its entire scope. So if there is a lambda term of the form (\lambda x. t) and it is desired to have x replaced with y, then the rewritten lambda term would have the form (\lambda y. ty/x) where ty/x, "t with y in stead of x", has had all free instances of x in t replaced with y.