Paper Info
Title
Specification of reduction strategies in term rewriting systems
Abstract
There is a growing interest in Term Rewriting Systems (TRS's), which are used as a conceptual basis for new programming languages such as functional languages and algebraic specification languages. TRS's serve as a computational model for (parallel) implementations of these languages. They also form the foundation for a calculus for Graph Rewriting Systems (GRS's). In Rewriting Systems reduction strategies play an important role because they control the actual rewriting process. Strategies determine the order of the rewriting and the rules to apply. Hence they have a great influence on the efficiency and the amount of parallelism in the computation. In ambiguous or non-deterministic TRS's, they even influence the outcome of the computation. Some of the reduction strategies used in TRS's are extremely complex algorithms. Unfortunately, there is no common formal specification method for reduction strategies yet. In this paper three formal methods for specifying reduction strategies in TRS's are presented. In the first method the reduction strategy is encoded in the TRS itself. The original TRS is transformed to a so called annotation TRS in which the strategy is encoded using functions. This annotation TRS itself may use any normalizing reduction strategy. Unfortunately, compared with the number of rules of the original TRS, the annotation TRS may contain an exponential number of additional rules. In the second method this drawback is prevented, simply by using a priority TRS as annotation TRS. The desire to specify a strategy uniformly for all TRS's leads to the third method. A new TRS system is introduced that uses two basic primitives for matching and rewriting and that is build out of three separate TRS's. The use of this abstract-interpretation TRS is shown to be the most promising method.
Year
Venue
Keywords
1986
Proc. of a workshop on Graph reduction
reduction strategy,computer model,programming language,formal specification,formal method,graph rewriting,functional language
Field
DocType
ISBN
Algebraic specification,Specification language,Programming language,Computer science,Formal specification,Theoretical computer science,Language Of Temporal Ordering Specification,Confluence,Graph rewriting,Rewriting,Formal methods
Conference
0-387-18420-1
Citations 
PageRank 
References 
8
1.34
7
Authors
2
Name
Order
Citations
PageRank
marko c j d van eekelen123930.37
Marinus J. Plasmeijer221023.72