Typed Generic Traversals in S'(underscore)Gamma; Software engineering rept

摘要

A typed model of strategic rewriting is developed. An innovation is that generic traversals are covered. To this end, we define a rewriting calculus S'(underscore)Gamma. The calculus offers a few strategy combinators for generic traversals. There is, for example, a combinator to apply a strategy to all immediate subterms of a given term. This idiom is relevant for generic type-preserving traversals. We also go beyond type-preservation which corresponds to another innovation. There is, for example, a combinator to reduce all the immediate subterms of a term. S'(underscore)Gamma employs a many-sorted type system extended by distinguished signature-independent (say generic) strategy types Gamma. To inhabit generic types, we need to add a fundamental combinator to lift a many-sorted strategy S to a generic type Gamma. The reduction semantics for this kind of lifting states that s is only applied if the type of the term at hand fits, otherwise the strategy fails. This approach dictates that the semantics of strategy application must be type-dependent to a certain extent. Typed strategic rewriting with generic traversals is a simple but expressive model of generic programming. It has applications in program transformation and program analysis.