combinators yes no, z is free yes yes no, z is free normal form or diverge? converges no, diverges converges beta reduce z bb qq yy yy aac 𝜆z.za - close, need to distinguish between bound and free z variables