文献类型：期刊文献

英文题名：Term rewriting systems with sort priorities

作者：Shao, ZQ; Song, GX

年份：1995

卷号：56

期号：3-4

起止页码：151

外文期刊名：INTERNATIONAL JOURNAL OF COMPUTER MATHEMATICS

收录：;WOS:【SCI-EXPANDED(收录号:WOS:A1995UG67400003)】；

语种：英文

外文关键词：rewriting system; sort priority; termination; recursive program; semantics

摘要：In this paper we propose a concept of term rewriting system with sort priorities, which is simply a partial order on the sorts. According to the partial order and a set of function symbols specified in a system, for every term we define another partial order on the set of all subterms by assigning a priority to each subterm. We also define a subterm to require attention if it is an instance of the left-hand side of some rewrite rule. The procedural meaning of such a rewriting system is that at some stage a subterm is allowed to be rewritten only if it requires attention and no subterm of a higher (or stronger) priority requires attention. This reduction strategy may transform some nonterminating (unrestricted) reduction sequences into terminating ones. We discuss the semantics of our systems and give an application to the operational semantics of recursive programs.