带术语重写策略的类型化泛型策略
Typed Generic Traversal With Term Rewriting Strategies
摘要：
提出了一种策略性术语改写的类型化模型。关键的创新是覆盖了泛型遍历。为此，我们定义了一个类型化重写演算S '_{gamma}。演算采用了一个多排序的类型系统扩展指定的通用策略类型伽马。我们考虑两种通用的策略类型，即类型保持和类型统一的策略。S ′_{gamma}提供遍历组合子，用于从多分类和一般策略中构造遍历或遍历方案。遍历组合子模拟了不同形式的单步遍历，也就是说，它们处理给定项的直接子项，而不期望任何递归到项的方案。为了适应泛型类型，我们需要添加一个基本的组合子来将多排序策略$s$提升为泛型类型gamma。这一步称为策略扩展。对应的组合子的语义表明，只有当手头的项的类型适合时才应用s，否则扩展策略失败。这种方法要求策略应用的语义必须在一定程度上依赖于类型。覆盖泛型项遍历的类型化策略项重写是泛型编程的一个简单但富有表现力的模型。它在程序转换和程序分析中有应用。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
