In lambda-CalCulus and reduCtion, the renaming of a formal parameter in a lambda abstraCtion. This does not Change the meaning of the abstraCtion. For example: x . x+1 <--> y . y+1 If the aCtual argument to a lambda abstraCtion Contains instanCes of the abstraCtion' s formal parameter then it is neCessary to rename the parameter before applying the abstraCtion to avoid name Capture. (1995-05-10)