Converted with LaTeX2HTML 96.1 (Feb 5, 1996) by Nikos Drakos (nikos@cbl.leeds.ac.uk), CBLU, University of Leeds

# Introduction

This thesis analyzes the rewriting system CL(S):     combinatory logic with the single combinator   S x y z -> x z (y z) We show that rational tree languages can be used   in order to describe interesting properties of S-terms.

Term rewrite systems are complicated in the following sense: they constitute a model of computation   that is Turing-complete. Therefore, a lot of questions are undecidable in general.

On the other hand, rational languages are handy: they can be described by finite machines (tree automata),   and here a lot of questions are decidable and a lot of operations on rational languages are effectively computable.

It is desirable to explore the borderline between these two realms: How far can we go in using rational languages when describing properties of term rewriting systems?

This thesis is intended to be a very detailed case study, yielding data that invites finding a more abstract description of the phenomena that are presented here.

We regard combinatory logic as a special term rewriting system. It acts on term algebras with some nullary function symbols (namely, the combinators) and exactly one binary function symbol (usually called application). Further, each combinator has an associated reduction rule whose left hand side must be of a simple shape.

Because of these restrictions, combinatory logic has the nice property that it is a confluent term rewrite system.   Moreover, CL(S) is non-erasing.

Still, combinatory logic remains complicated in general because there are complete sets (called bases) of combinators   that can simulate arbitrary rewrites, and therefore are computationally equivalent to Turing machines.   A well known example is the two-element base S,K with     K x y -> x

If we now drop K from cl(S,K), we arrive at the system CL(S), which is no longer complete. Since CL(K) looks easy, we feel that S is responsible for the difficulty of cl(S,K). Therefore, CL(S) should be nearly as hard as cl(S,K). However some questions for CL(S) really are solvable, and we present these new results:

• CL(S) is top-terminating.
• CL(S) admits no ground loops.
• It is decidable whether an S-term normalizes.
• The set of normalizing S-terms is rational.
In this list, the last item has to be taken cum grano salis because it depends on a proof by computer that has only been partially completed.

This thesis also includes the description of the software system RX.   It handles rational tree languages, and it has been used in finding and verifying results presented in this thesis.

Basically, RX acts as a desk top calculator that operates on rational languages. It is not tied to CL(S), but can do computations in arbitrary term algebras (with fixed arities).

On top of this, RX processes its input and output so that it co-operates nicely with text formatters as LaTeX [],       in the spirit of a literate programming [] tool.     For instance, RX had been used to format [].

http://www.informatik.uni-leipzig.de/~joe/ mailto:joe@informatik.uni-leipzig.de