Adding Scoping Constructs to Term Rewrite Systems
Keehang Kwon · Journal of Electrical Engineering and Information Science · 1999
We extend first-order tenn rewrite systems with scoping constructs. One of these constructs is the expression of the form D ⇒ E where D is a list of rewrite rules (i.e., a module in our context) and E is an expression to be evaluated. This expression has the following operational semantics: add the rewrite rules in D to the current program and then evaluate E. Thus, the rules in D are local to the expression E. Other constructs are related to controlling the interaction of these modules and to giving constants a scope. To be specific, the construct new and local provides a novel approach that controls the visiblility of the constants in a module and the construct @ permits modules to be organized from submodules. There are subtle interactions among these constructs. We define these interactions carefully by giving a precise semantics of this language and showing some examples of its use. Finally, the operational semantics of the construct ⇒ leads to redundancy in search. We present a new semantics of the construct in which this redundancy can be controlled.