Unicity of normal forms

Unicity of normal forms: in (pure) functional languages, the value of an expression is uniquely determined by its components, and is independent of the order of reduction