Proof checking
Weak head normal form
Abbreviated WHNF
A term reduced enough to expose its outermost form.
Definition
Weak head normal form
Weak head normal form (WHNF) exposes the leading constructor, function, or type former without fully reducing every nested term.
A kernel often needs only the outer shape to continue type checking. Stopping early avoids work that cannot affect the current judgment.
01
Example
A function call may reduce until the result is visibly a function type while its body remains partly unreduced.
02
Important distinction
WHNF is not a fully normalized expression.
After reading this article, you should be able to
- Define WHNF in the sense used on this site.
- Explain why a kernel can compare some terms without fully normalizing them.