The elimination rule of union types (denoted by (UE)) can break strong normalization (i.e. is unsafe) in presence of non- determinism. This is quite disturbing, since union types are often required in presence of non-deterministic computations. Surprisingly, there are also confluent systems for which this rule is unsafe.
We study the safety of the elimination rule of union types for an extension of the lambda calculus with simple rewrite rules. We prove that the union and intersection types discipline is complete w.r.t. strong normalization. This allows to show that (UE) is safe if and only if an interpretation of types based on biorthogonals is sound for it.
We then discuss two sufficient conditions for the safety of (UE). The first one is issued from the closure by union of Girard's reducibility candidates while the second is the closure by union of a biorthogonality operator. It turns out that the first condition implies completeness of intersection type assignment w.r.t. strong normalization while the second (which is strictly more general) corresponds to the ability to define sound Tait's saturated sets for the calculus under consideration.
Finally, we discuss an alternative biorthogonality relation based on the observation of the least reducibility candidate.