If the rewriting system is not guaranteed to terminate (e.g., if the user oriented an equation into a rewrite rule manually), the normal form computation may not terminate. When the rewriting system is not known to terminate, LP stops the rewriting process and issues a warning after a very large number of rewrites during a normal form computation. See the rewriting-limit setting.
If the rewriting system is not confluent, a term may have more than one normal form.
LP uses normalization as a method of forward and backward inference.