A Comparison of Well-Quasi Orders on Trees

Torben Æ. Mogensen
(DIKU, University of Copenhagen, Denmark)

Well-quasi orders such as homeomorphic embedding are commonly used to ensure termination of program analysis and program transformation, in particular supercompilation.

We compare eight well-quasi orders on how discriminative they are and their computational complexity. The studied well-quasi orders comprise two very simple examples, two examples from literature on supercompilation and four new proposed by the author.

We also discuss combining several well-quasi orders to get well-quasi orders of higher discriminative power. This adds 19 more well-quasi orders to the list.

In Anindya Banerjee, Olivier Danvy, Kyung-Goo Doh and John Hatcliff: Semantics, Abstract Interpretation, and Reasoning about Programs: Essays Dedicated to David A. Schmidt on the Occasion of his Sixtieth Birthday (Festschrift for Dave Schmidt), Manhattan, Kansas, USA, 19-20th September 2013, Electronic Proceedings in Theoretical Computer Science 129, pp. 30–40.
Published: 19th September 2013.

ArXived at: http://dx.doi.org/10.4204/EPTCS.129.3 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org