Normalization of S-terms is decidable.

The combinator S has the reduction rule Sx y z → x z (y z). We investigate properties of ground terms built from S alone. We show that it is decidable whether such an S-term has a normal form. The decision procedure makes use of rational tree languages. We also exemplify and summarize other properties of S-terms and hint at open questions. [ABSTRACT FROM AUTHOR]