A typed model of strategic term rewriting is developed. The key innovation is that generic traversal is covered. To this end, we define a typed rewriting calculus S′γ. The calculus employs a many-sorted type system extended by designated generic strategy types γ. We consider two generic strategy types, namely the types of type-preserving and type-unifying strategies. S′γ offers traversal combinators to construct traversals or schemes thereof from many-sorted and generic strategies. The traversal combinators model different forms of one-step traversal, that is, they process the immediate subterms of a given term without anticipating any scheme of recursion into terms. To inhabit generic types, we need to add a fundamental combinator to lift a many-sorted strategy s to a generic type γ. This step is called strategy extension. The semantics of the corresponding combinator states that s is only applied if the type of the term at hand fits, otherwise the extended strategy fails. This approach dictates that the semantics of strategy application must be type-dependent to a certain extent. Typed strategic term rewriting with coverage of generic term traversal is a simple but expressive model of generic programming. It has applications in program transformation and program analysis. © 2002 Elsevier Science Inc. All rights reserved.
CITATION STYLE
Lämmel, R. (2003). Typed generic traversal with term rewriting strategies. Journal of Logic and Algebraic Programming, 54(1–2), 1–64. https://doi.org/10.1016/S1567-8326(02)00028-0
Mendeley helps you to discover research relevant for your work.