previous
|
top
|
next
We are mostly interested in closed lambda-terms
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.