The Combinator S

The combinator S has the reduction rule S xyz→xz(yz). We investigate properties of ground terms built from S alone. The first part of the paper shows that this term rewriting system admits no ground loops. This extends the known result of the absence of cycles. In the second part, we give a procedure that decides whether an S-term has a normal form. This algorithm makes use of rational tree languages. Finally we show that the set of normalizing S-terms is in itself a rational tree language, by explicitly giving its grammar. In all, this paper shows the surprisingly rich structures that are implied by a seemingly small rewrite rule.

Authors

• Johannes Waldmann

Keywords

No keywords are indexed for this paper.