You are here: irt.org | FOLDOC | Head Normal Form
<theory, reduction> (HNF) A term describing a lambda expression 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.
An expression in HNF may contain redexes in argument postions whereas a normal form may not.
Compare Weak Head Normal Form.
(2003-01-08)
Nearby terms: hdx « Head Disk Assembly « header « Head Normal Form » head normalisation theorem » heads down » head-strict
FOLDOC, Topics, A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, ?, ALL