Abstract

During the development of the ASF+SDF compiler it became clear that a simplification of the back-end could be achieved by eliminating associative lists and conditional equations in an early phase of compilation. In this thesis the transformation of conditional equational term rewrite systems with \em associative lists to term rewrite systems without lists is described by means of an algebraic specification. To make as much of the specification reusable the specification is written in a style called {\em Combinatory Algebraic Specification}. In this style it is possible to define polymorphic higher-order functions (or combinators) and use these as arguments to functions and as results of computations. Using this style a vast library of general purpose combinators is developed. The specification of the combinatory language, the library of combinators and the specification of the transformation are written in a \em Literate Specification style, meaning that the specification and the text explaining it are integrated.