theory, reduction (HNF) A term describing a lambdaexpression whose top level is either a variable, a data

value, a built-in function applied to too few arguments, or a

lambda abstraction whose body is not reducible. I.e. the

top level is neither a redex nor a lambda abstraction with a

reducible body.