Reduction Sequences

In pure functional languages the value of an expression is uniquely determined by its components, and is independent of the order of reduction, this is the Unicity of normal forms and provides the advantage of increased readability in programs. Some reduction sequences however, might not lead to a value, some do not terminate.

The function $fortytwo(x) = 42$, and $infinity(x)=infinity(x)$ for example.

Some reduction sequences of the expression $fortytwo(infinity(x))$ will lead to $42$, but some will not terminate, this expression has Unicity in its normal forms, since all the sequences which evaluate fully lead to $42$.