返回Google圖書搜尋

Semantics of Non-terminating Rewrite Systems Using Minimal Coverings

José BarrosJoseph GoguenOxford University Computing Laboratory. Programming Research Group

出版	Oxford University Computing Laboratory, Programming Research Group, 1995
URL	http://books.google.com.hk/books?id=1rFrPgAACAAJ&hl=&source=gbs_api

註釋Abstract: "We propose a new semantics for rewrite systems based on interpreting rewrite rules as inequations between terms in an ordered algebra. In particular, we show that the algebra of normal forms in a terminating system is a uniquely minimal covering of the term algebra. In the non-terminating case, the existence of the minimal covering is established in the completion of an ordered algebra formed by rewriting sequences. We thus generalize the properties of normal forms for non- terminating systems to this minimal covering. These include the existence of normal forms for arbitrary rewrite systems, and their uniqueness for confluent systems, in which case the algebra of normal forms is isomorphic to the canonical quotient algebra associated with the rules when seen as equations. This extends the benefits of algebraic semantics to systems with non-deterministic and non-terminating computations. We first study properties of abstract orders, and then instantiate these to term rewriting systems."