Generation of a Linear Time Query Processing Algorithm Based on Well-Quasi-Orders

  • Mizuhito Ogawa
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2215)


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.

Unable to display preview. Download preview PDF.


  1. 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. 2.
    T. Coquand and D. Fridlender. A proof of Higman’s lemma by structural induction, November 1993. available at
  3. 3.
    R.M. Fellows and M.A. Langston. Nonconstructive tools for proving polynomialtime decidability. Journal of the ACM, 35(3):727–739, 1988.zbMATHCrossRefMathSciNetGoogle Scholar
  4. 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. 5.
    A. Geser. A proof of Higman’s lemma by open induction. Technical Report MIP-9606, Passau University, April 1996.Google Scholar
  6. 6.
    A. Gupta. A constructive proof that tree are well-quasi-ordered under minors. In A. Nerode and M. Taitslin, editors, Logical foundations of computer science-Tver’92, pages 174–185, 1992. Lecture Notes in Computer Science, Vol. 620, Springer-Verlag.CrossRefGoogle Scholar
  7. 7.
    G. Higman. Ordering by divisibility in abstract algebras. Proc. London Mathematical Society, 2:326–336, 1952.zbMATHCrossRefMathSciNetGoogle Scholar
  8. 8.
    M. Koubarakis. The complexity of query evaluation in indefinite temporal constraint databases. Theoretical Computer Science, 171:25–60, 1997.zbMATHCrossRefMathSciNetGoogle Scholar
  9. 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
  10. 10.
    C.ST.J.A. Nash-Williams. On well-quasi-ordering finite trees. Proc. Cambridge Phil. Soc., 59:833–835, 1963.zbMATHMathSciNetCrossRefGoogle Scholar
  11. 11.
    N. Dershowitz and Z. Manna. Proving termination with multiset orderings. Communications of the ACM, 22(8):465–476, 1979.zbMATHCrossRefMathSciNetGoogle Scholar
  12. 12.
    L. Perković and B. Reed. An improved algorithm for finding tree decompositions of small width. In Widmayer, editor, WG’99, pages 148–154, 1999. Lecture Notes in Computer Science, Vol. 1665, Springer-Verlag.Google Scholar
  13. 13.
    F. Richman and G. Stolzenberg. Well quasi-ordered sets. Advances in Mathematics, 97:145–153, 1993.zbMATHCrossRefMathSciNetGoogle Scholar
  14. 14.
    N. Robertson and P.D. Seymour. Graph minors XX. Wagner’s conjecture, 1988. Manuscript.Google Scholar
  15. 15.
    N. Robertson and P.D. Seymour. Graph minors XIII. the disjoint path problem. Journal of Combinatorial Theory Series B, 63:65–110, 1995.zbMATHCrossRefMathSciNetGoogle Scholar
  16. 16.
    S.G. Simpson. Ordinal numbers and the Hilbert basis theorem. Journal of Symbolic Logic, 53(3):961–974, 1988.zbMATHCrossRefMathSciNetGoogle Scholar
  17. 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
  18. 18.
    R. van der Meyden. The complexity of querying indefinite data about linearly ordered domains. Journal of Computer andSystem Science, 54(1):113–135, 1997. Previously presented at 11th ACM sympo. on Principles of Database Systems, pp.331-345, 1992.zbMATHCrossRefGoogle Scholar
  19. 19.
    W. Veldman. An intuitionistic proof of Kruskal’s theorem. Technical Report 17, Department of Mathematics, University of Nijmegen, April 2000.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Mizuhito Ogawa
    • 1
  1. 1.NTT Communication Science LaboratoriesJapan

Personalised recommendations