Generation of a Linear Time Query Processing Algorithm Based on Well-Quasi-Orders
This paper demonstrates the generation of a linear time query processing algorithm based on the constructive proof of Higman’s lemma described by Murthy-Russell (IEEE LICS 1990). A linear time evaluation of a fixed disjunctive monadic query in an indefinite database on a linearly ordered domain, first posed by Van der Meyden (ACM PODS 1992), is used as an example. Van der Meyden showed the existence of a linear time algorithm, but an actual construction has, until now, not been published elsewhere.
Unable to display preview. Download preview PDF.
- 1.J. Chomicki. Temporal query languages: a survey. In D.M. Gabbay and H.J. Ohlbach, editors, Temporal Logic: (ICTL’94), pages 506–534, 1994. Lecture Notes in Artificial Intelligence, Vol. 827, Springer-Verlag.Google Scholar
- 2.T. Coquand and D. Fridlender. A proof of Higman’s lemma by structural induction, November 1993. available at http://www.md.chalmers.se/~coquand/intuitionism.html.
- 4.D. Fridlender. Higman’s lemma in type theory. In E. Gimnez and C. P.-Mohring, editors, Types for Proofs andPr ograms, TYPES’96, pages 112–133, 1996. Lecture Notes in Computer Science, Vol. 1512, Springer-Verlag.Google Scholar
- 5.A. Geser. A proof of Higman’s lemma by open induction. Technical Report MIP-9606, Passau University, April 1996.Google Scholar
- 9.C.R. Murthy and J.R. Russell. A constructive proof of Higman’s lemma. In Proc. 5th IEEE sympo. on Logic in Computer Science, pages 257–267, 1990.Google Scholar
- 12.L. Perković and B. Reed. An improved algorithm for finding tree decompositions of small width. In et.al. Widmayer, editor, WG’99, pages 148–154, 1999. Lecture Notes in Computer Science, Vol. 1665, Springer-Verlag.Google Scholar
- 14.N. Robertson and P.D. Seymour. Graph minors XX. Wagner’s conjecture, 1988. Manuscript.Google Scholar
- 17.W. Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, chapter 4, pages 133–192. Elsevier Science Publishers, 1990.Google Scholar
- 19.W. Veldman. An intuitionistic proof of Kruskal’s theorem. Technical Report 17, Department of Mathematics, University of Nijmegen, April 2000.Google Scholar