top

next
The usual definition of lambdaterms
The set of lambdaterms, L, is defined inductively:
x is in L
M in L implies (\x.M) is in L
M, N in L implies (MN) is in L
where x is an arbitrary variable.