Generic type-preserving traversal strategies

✍ Scribed by Ralf Lämmel

• Book ID: 104444673
• Publisher: Elsevier Science
• Year: 2001
• Tongue: English
• Weight: 424 KB
• Volume: 57
• Category: Article
• ISSN: 1571-0661
• DOI: 10.1016/s1571-0661(04)00268-3

✦ Synopsis

A typed model of strategic rewriting with coverage of generic traversals is developed. The corresponding calculus offers, for example, a strategy operator (\square(\cdot)), which applies the argument strategy to all immediate subterms. To provide a typeful model for generic strategies, one has to identify signature-independent, that is, generic types. In the present article, we restrict ourselves to TP-the generic type of all Type-Preserving strategies. TP is easily integrated into a standard many-sorted type system for rewriting. To inhabit TP, we need to introduce a (left-biased) type-driven choice operator (\cdot & \cdot). The operator applies its left argument (corresponding to a many-sorted strategy) if the type of the given term fits, and the operator resorts to the right argument (corresponding to a generic default) otherwise. This approach dictates that the semantics of strategy application must be type-dependent to a certain extent.