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.
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.
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.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:
<conseq>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].
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.
[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
This site's top page is http://okmij.org/ftp/
Converted from SXML by SXML->HTML