An applicative-order term rewriting system for code generation, and its termination analysis

We describe an applicative order term re-writing system for code generation, and its application for efficient realizations of median filters as decision trees. We further describe a polynomial time termination analysis to prove termination of the median filter generating rules. The systems are implemented in the pure functional subset of Scheme. The full source code is available from this site.

A short talk presented on June 22, 2003 at the Eighteenth Annual IEEE Symposium on Logic in Computer Science (LICS 2003). June 22-25, 2003. Ottawa, Canada.

  1. Motivation
  2. Code generation term re-writing system
  3. Termination analysis
  4. Conclusions

  

Motivation

Median filtering is a classic method of eliminating impulse noise in speech and image processing [Huang]. The filter replaces a signal sample with the median of the samples within a filter window. The median filter effectively removes outliers while largely preserving signal features such as sharp image edges. One of the major problems with the median filter is that it is relatively expensive and complex to compute.

One of the approaches to determining the median is a decision tree: For example, given three samples x1, x2, x3, we can find their median as follows:

     (if (less? x2 x3)
       (if (less? x2 x1) (if (less? x3 x1) x3 x1) x2)
       (if (less? x3 x1) (if (less? x2 x1) x2 x1) x3))

This code needs no extra storage, has no loops, and particularly lends itself to an implementation as a combinational circuit. However, writing such decision trees is quite challenging even for 5 inputs, especially if we strive for optimality in terms of the maximum or average depths of the tree.

This paper describes a code generation system that can produce, inter alia, median decision trees for an arbitrary number of inputs. For example, for five inputs, the system generates code that finds the median in at least 5 and at most 7 comparisons.

The code generator is an instance of a term re-writing system. The next section presents the system and the re-writing rules for generating median decision trees. In Section 3, we briefly describe a termination analysis of those code generation rules.


  

Code generation term re-writing system

Our code generator is an instance of a term re-writing system [Baader]. The re-writing process however is more structured due to the explicit marking of redexes and an applicative order of applying them.

As usual, Sigma is a set of function symbols and constants, and a V is a set of variables. The members of both sets are Scheme symbols; variable names are distinguished by a leading underscore. Like in Prolog, a sole underscore is the anonymous variable. We partition the set of function symbols of arity at least 1 into two disjoint subsets, of V- and M-function symbols. Terms over V-function symbols, constants, and variables are called V-terms. A simple M-term is an application of an M-function symbol to V-terms; a term with M symbols is an M-term. In Scheme, we represent V- and M- functional terms as S-expressions of the form (symbol term ...) or (M symbol term ...) correspondingly.

Only M-terms are subject to re-writing rules, each of which has a form ( <pattern> => <consequent> ) where <pattern> is a simple M-term, which almost always contains variables. A variable may occur within a pattern several times. The evaluator of the system takes an M-term without variables -- the subject term -- and a set of re-writing rules. The evaluator scans the rules in order, trying to match a redex of the term, which is by necessity a simple M-term, against the pattern of a rule. It is an error if the redex did not match any rule. When a redex matches a rule, variables in the pattern are bound to the corresponding subterms in the redex. Different occurrences of the same variable must match identical subterms [Match-Unify]. If the subject M-term has several redexes, the leftmost innermost is reduced first. If the re-written redex is not a V-term, it will be reduced again.

The explicit marking of redexes (as M-terms) and the applicative order of reductions make it easy to write and analyze rules. In particular, the applicative order guarantees composability of the rules. The complete source code for the reduction engine along with many sample rulesets and the validation code are given in [PostL].

For example, the following rules represent the Ackerman function:

     (((M Ack (zero) _n)           => (succ _n))
      ((M Ack (succ _m) (zero))    => (M Ack _m (succ (zero))))
      ((M Ack (succ _m) (succ _n)) => (M Ack _m (M Ack (succ _m) _n)))
      ((M mult (zero) _x)    => (zero))
      ((M mult _x (zero))    => (zero))
      ((M mult (succ _x) _y) => (M add _y (M mult _x _y)))
      ((M add (zero) _x)     => _x)
      ((M add _x (zero))     => _x)
      ((M add (succ _x) _y)  => (succ (M add _x _y))))

The last six rules encode addition and multiplication of integers. To compute Ack(2,2), we evaluate the following Scheme expression

     (reduce '(M Ack (succ (succ (zero))) (succ (succ (zero)))) rule-Ackerman)

which will reduce the given subject term using the set rule-Ackerman above. Similarly, the evaluation of

     (reduce '(M median (seq x1 (seq x2 (seq x3 (seq-empty))))) rule-median)

yields a term that represents the decision tree in Section 1 for the median of three inputs, x1, x2, and x3. The term can later be written in the concrete syntax of a target language. The complete 53-rule ruleset for generating median filters, with detailed explanations, is given in [Median-Filter-Gen]. Sample median filters for 3-6 inputs are included in [Median-Filter-Test], along with validation tests and complexity estimates. In particular, the median filter for 5 inputs requires at least 5 and at most 7 comparisons to find a median: the average, given uniformly distributed inputs, is 5.97 comparisons, which is within 2% of the optimum average number of comparisons quoted in Knuth (5.87). Knuth does not give the code though.

Our algorithm: we split the sequence in two halves, merge-sort both halves and use the result to find the floor((n-1)/2)-th minimum. By "sort" above we mean the abstract syntax tree that will sort the sequence at run time. The excerpt below shows the merge-sort part.

     ( (M merge-pass (seq _s1 (seq _s2 _r)) _target _n _c) =>
       (M merge-two _s1 _s2 (seq-empty) _r _target _n _c) )
     
     ( (M merge-two (seq _x _s1) (seq _y _s2) _t _ur _ut _n _c)
       =>
       (if (less? _x _y)
        (M merge-two _s1 (seq _y _s2) (seq _x _t) _ur _ut _n _c)
        (M merge-two (seq _x _s1) _s2 (seq _y _t) _ur _ut _n _c)) )
     
     ( (M merge-two (seq-empty) (seq _y _s2) _t _ur _ut _n _c)
       =>
       (M merge-two (seq-empty) _s2 (seq _y _t) _ur _ut _n _c) )
     
     ( (M merge-two (seq-empty) (seq-empty) (seq _th _tt)
          _ur _ut (succ (succ _n)) _c) =>
       (M merge-pass _ur (seq (M reverse (seq _th _tt)) _ut)
          (succ _n) _c) )
The code is highly recursive: merge-pass invokes merge-two, merge-two uses merge-pass, there is another set of recursive rules that determine that the sort is finished. When the first half is done we come here again to sort the second half.
  

Termination analysis

We have implemented a termination analysis for the re-writing rules, also in the pure functional subset of Scheme. Given a set of re-writing rules, the analysis will attempt to prove that any subject M-term will be reduced, in a finite number of steps, to a V-term or an error. The proof is an instance of an approximate size-change termination analysis for the set of program multipaths, somewhat similar to the ones described in [Jones] [Lee].

Proving termination of the merge sort, which underlies the rules, is quite challenging, because the sorting algorithm deconstructs some lists but builds some other lists. Furthermore, the algorithm is intricately mutually recursive.

The analysis proceeds by repeatedly applying the following strategies to the rules:

A strategy tries to soundly remove a rule from the ruleset while preserving or weakening ruleset's termination properties. A strategy can extend the ruleset with new rules: proof subgoals. If we managed to remove all the rules, then the original ruleset terminates. The prover is strongly normalizing: The strategies are applied until they can no longer be applied. If there are some rules left, they have to be analyzed by hand or with some new strategies. The leftover rules are far fewer than the original ones. Thus the analyzer acts as a proof assistant, good at eliminating the dirty work. The analyzer is not very efficient at the moment -- the gross over-estimate for the time complexity is the 4th power of the number of rules, although I have only seen a quadratic growth.

Simple strategies deal with the rules whose consequent matches only its own pattern (simple recursion). If the result of matching causes some subterm to shrink, the entire rule is terminating provided all embedded M-terms are contractive as well.

The most challenging aspect is handling mutually recursive rules. Given a ruleset, we choose a rule which is neither directly nor indirectly recursive. We then symbolically expand all other rules with the chosen rule. The chosen rule becomes redundant and can be dropped. If this strategy applies, cycles of mutual recursion become simple recursion or become clusterized. A cluster -- a maximal set of mutually recursive rules for the same M-term -- is searched for a lexicographic ordering on the subset of subterms of the consequents. If such size-based ordering is found, the cluster is proven terminating, provided all embedded M-terms if any are contractive as well.

The complete source code for the termination analyzer and the detailed descriptions of the strategies are in the second half of [PostL]. The application of strategies requires unification of (non-linear) terms. The latter source code is available at [Match-Unify].


  

Conclusions

We have presented a code generation term re-writing system and its polynomial-time termination analysis. We have applied the two systems to median filtering. The generated decision procedures have no iterations, require no intermediate storage, and need at most Theta (n log n) comparisons for n inputs. There are better algorithms [Knuth], however, their advantage emerges at n>32, when decision trees become impractical.

Currently our median filters are not incremental, and thus do not take advantage of spatial coherency. On the other hand, the generated code can be used when the median filter is a stage in a more complex filtering operation, where incremental approach is not applicable. Our system is not specific to one particular algorithm of finding a median, or even to median at all. Nevertheless, we plan to investigate incremental median filters in the future research.

Although our current filters are quite nearly optimal, occasionally we execute more comparisons than strictly necessary. We plan to fix that. Finally, we'd like to make our size-changing termination analysis more precise so it can handle a more subtle descent.


  

References

[Baader] Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, 1998.

[Huang] Huang, T.S.: Two-Dimensional Signal Processing II: Transforms and Median Filters. Berlin: Springer-Verlag, 1981.

[Jones] Jones, N., Glenstrup, A.: Program Generation, Termination, and Binding-time Analysis. In: D. Batory, C. Consel, and W. Taha (Eds.): GPCE 2002, LNCS 2487, pp. 1-31, 2002.

[Knuth] Knuth, D.E.: The Art of Computer Programming. Vol 3. Sorting and Searching. Addison-Wesley, 1973.

[Lee] Lee, Chin Soon: Program Termination Analysis in Polynomial Time. In: D. Batory, C. Consel, and W. Taha (Eds.): GPCE 2002, LNCS 2487, pp. 218-235, 2002.

[Pitas] Pitas, I., Venetsanopoulos, A.N.: Nonlinear Digital Filters: Principles and Applications, Kluwer Academic Publishers, 1990.

[Match-Unify] tree-unif.scm [30K]
Non-linear matching and fast (cyclic) unification

[Median-Filter-Gen] median-filt.scm [25K]
Re-writing rules for generating median filters

[Median-Filter-Test] median-filt-test.scm [13K]
Sample median filters, validation tests and complexity estimates

[PostL] PostL.scm [68K]
An applicative-order term rewriting system, and its termination analysis



Last updated July 4, 2003

This site's top page is http://pobox.com/~oleg/ftp/

oleg-at-pobox.com or oleg-at-okmij.org or oleg-at-computer.org
Your comments, problem reports, questions are very welcome!

Converted from SXML by SXML->HTML