§ Head normal form

• a data constructor applied to arguments which are in normal form
• a lambda abstraction whose body is in normal form