previous

top

next
We are mostly interested in closed lambdaterms
FV(M) is the set of free variables in M and can be defined inductively:
FV(x) = {x}
FV(\x.M) = FV(M)  {x}
FV(MN) = FV(M) U FV(N)
M is closed if FV(M) is empty.