Next:DiscussionUp:Operational Semantics of Rewriting Previous:Operational Semantics as

# Hint about Specifying Local Strategies

In this section a hint about giving local strategies to operators (or function symbols) is presented. The on-demand E-strategy gives us two ways of postponing evaluating some terms. If we want to postpone evaluating the kth argument of a term f(t1, ..., tn), the operator f is given a local strategy excluding k or a local strategy including -k. There are at least two things that can be carried out by postponing evaluating terms: avoiding wasteful evaluation and dealing with infinite data structures such as infinite lists.

It is possible to avoid wasteful evaluation by giving local strategies excluding some positive integers to operators (i.e. functions). A typical example of avoiding wasteful evaluation is the conditional operator if_then_else_fi.

Example 7 (Conditional operator if_then_else_fi).
op if_then_else_fi : Bool S S -> S  { strat: (1 0) }
eq if true then X:S else Y:S fi = X .
eq if false then X:S else Y:S fi = Y .

A term with if_then_else_fi as its top operation such as ``if cond then comp1 else comp2 fi'' is replaced by the second argument comp1 or the third argument comp2 depending on the result (i.e. true or false) of evaluating the first argument cond. If the result of evaluating the first argument is true (or false), the second (or third) argument replaces the whole term, and the third (or second) argument is just discarded and does not cause wasteful evaluation.

It is possible to deal with infinite data structures by giving local strategies including negative integers to operators (data constructors). For example, infinite lists can be dealt with by giving the local strategy (1 -2 0) to the list constructor _ _ as follows: _ _ : Nat ooList-> ooList { strat: (1 -2 0) } ( ooList stands for infinite lists and lists of natural numbers are considered for brevity). The result of evaluating some term denoting an infinite list is in head normal form, but the evaluation does not lead to infinite rewriting. Suppose that inf is declared as inf : Nat-> ooList and inf(X: Nat) = X inf(X + 1), the result of evaluating inf(0) is ``0 inf(1).'' But the result of evaluating even some term denoting a finite list might be in head normal form. For example, the result of evaluating ``tp(1 2 nil) tl(1 2 3 nil)'' is ``1 tl(1 2 3 nil)'' that is in head normal form, but not in normal form. The result of evaluating some term denoting a finite list should be in normal form. Since CafeOBJ supports order-sorted rewriting, infinite lists are allowed to coexist with finite lists well by having the sort ooList have a subsort List for finite lists and declaring the constructor for finite lists. The constructor for finite lists is given the eager local strategy (1 2 0).

Example 8 (Coexistence of infinite lists with finite lists).
[ List < ooList ]
op nil : -> List
op _ _ : Nat List -> List  { strat: (1 2 0) }
op _ _ : Nat ooList -> ooList  { strat: (1 -2 0) }
op tp : ooList -> Nat
op tl : List -> List
op tl : ooList -> ooList

The result of evaluating ``tp(1 2 nil) tl(inf(0))'' is ``1 tl(inf(0)),'' while the result of evaluating `` tp(1 2 nil) tl(1 2 3 nil)'' is ``1 2 3 nil.'' Since the top operator _ _ of the former term is the constructor for infinite lists because the second term tl(inf(0)) denotes an infinite list, the second argument is not evaluated because of the local strategy (1 -2 0) of the operator. The top operator _ _ of the latter term is the constructor for finite lists because the second argument tl(1 2 3 nil) is finite, and the both of the first and second arguments are evaluated.

Next:DiscussionUp:Operational Semantics of Rewriting Previous:Operational Semantics as

Kazuhiro Ogata

Mon Nov 29 13:47:22 JST 1999