Desired property: uniqueness of normal forms

A desirable property of a Lambda calculus where every term always evaluates to the same Normal form. This property should hold in all deterministic systems.