Typed Generic Traversal With Term Rewriting Strategies
<|reference_start|>Typed Generic Traversal With Term Rewriting Strategies: 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'_{gamma}. The calculus employs a many-sorted type system extended by designated generic strategy types gamma. We consider two generic strategy types, namely the types of type-preserving and type-unifying strategies. S'_{gamma} 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 gamma. 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.<|reference_end|>
@article{laemmel2002typed,
    title={Typed Generic Traversal With Term Rewriting Strategies},
    author={Ralf Laemmel},
    journal={arXiv preprint arXiv:cs/0205018},
    year={2002},
    archivePrefix={arXiv},
    eprint={cs/0205018},
    primaryClass={cs.PL}
}