Lambda the Ultimate

inactiveTopic Term rewriting system for code generation, and its termination analysis
started 8/4/2003; 3:34:36 AM - last post 8/4/2003; 3:34:36 AM
Ehud Lamm - Term rewriting system for code generation, and its termination analysis  blueArrow
8/4/2003; 3:34:36 AM (reads: 1225, responses: 0)
Term rewriting system for code generation, and its termination analysis
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.

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.

Of specific interest is the discussion on termination analysis. More info on the unification algorithm can be found here.

Instead of discussing the details, let me make a more general observation. This example explores two interesting uses of linguistic abstraction: optimal code generation and termination analysis. Both "holy grails" for computer science and software engineering. Notice how these goals become more manageable by using the, ultimately linguistic, abstraction of term rewriting, itself a form of declerative programming.

These issues are also related to discussions of languages that prohibit recursion and multi-stage programming.


Posted to Logic/Declerative by Ehud Lamm on 8/4/03; 3:40:14 AM