Previous Up

Chapter 16  Encoding rewrite systems

16.1  Transition systems

Problem:
Encode a simple transition system and compute normal forms.

Solution:
Use the hook mechanism provided by Gom.

16.2  Computing all reachable terms

Problem:
Given a rewrite system and a term, compute the immediate successors.

Solution:
This cannot be done using hooks, use a strategy instead.


Suppose we have the following Gom definition: 
%gom {
  module Term
  abstract syntax
  Term = a()
       | b()
       | s(pred:Term)
       | f(arg1:Term)
}


Given a rewriting system s, we want to construct all the terms generated by s. In Tom, the solution consists in defining the rewriting system by a basic strategy %strategy and apply it to each subterm using the MuTraveler operator BottomUp. All possible terms reachable in one step are collected in a collection.

public void collectOneStep(final Collection collection, Term subject) { 
 try {
  MuTraveler.init(`BottomUp(OneStep(subject,collection))).visit(subject);
  System.out.println(collection);
 } catch (VisitFailure e) {
   System.out.println("Failed to get successors " +subject);
 }
}

%strategy OneStep(subject:Term,c:Collection) extends `Identity() {
  visit Term {
    f(x)    -> { c.add(MuTraveler.getReplace(this,`f(s(x))).visit(subject)); }
    f(s(x)) -> { c.add(MuTraveler.getReplace(this,`f(f(x))).visit(subject)); }
    s(s(x)) -> { c.add(MuTraveler.getReplace(this,`f(x)).visit(subject)); }
  }
}


Notice that we need to use the MuTraveler static method getReplace that replaces at the current position (given due to the parameter this corresponding to the current strategy) with the term given in the second parameter (for example f(s(x)) in the first rule). For more explanations, see 7.2.

Moreover, to use a Java Collection as an algebraic sort, we need to add the following code: 
 %typeterm Collection {
    implement { Collection }
  }


From now, we have just a collection of reachable terms in one step. If we want to know if a term is reachable in an undetermined number of steps, we define the function reach(Term start,Term end):

public boolean reach(Term start,Term end) {
    Collection result = new HashSet();
    Collection predResult = new HashSet();
    Collection c1 = new HashSet();
    c1.add(start);
    while (result.isEmpty() || predResult.containsAll(result)) {
      Collection c2 = new HashSet();
      Iterator it = c1.iterator();
      while(it.hasNext()) {
        collectOneStep(c2,(Term)it.next());
      }
      c2.removeAll(result);
      c1 = c2;
      predResult.addAll(result);
      result.addAll(c2);
      if(result.contains(end)) {
        return true;
      }
    }
    return false;
  }
This function can loop if the system s is not terminating or if no term is reachable from start.

Previous Up