1.NounOne of the three rewrite rules of lambda calculus, in which a bound variable of a lambda term is replaced by another variable across its entire scope. So if there is a lambda term of the form
(
λ
x
.
t
)
{\displaystyle (\lambda x.t)}
and it is desired to have x replaced with y, then the rewritten lambda term would have the form
(
λ
y
.
t
[
y
/
x
]
)
{\displaystyle (\lambda y.t[y/x])}
where
t
[
y
/
x
]
{\displaystyle t[y/x]}
, "t with y instead of x", has had all free instances of x in t replaced with y.