An analysis of divisibility orderings and recursive path orderings

  • Ryu Hasegawa
Session 7
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1345)


We show that normal and analytic functors provide a foundation to the theory of divisibility orderings and recursive path orderings. These functors are used to give intrinsic definitions independent from particular syntactic presentations.


Linear Order Binary Tree Ordinal Diagram Normal Functor Finite Tree 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    T. Becker and V. Weispfenning, Grôbner Bases, Graduate Texts in Mathematics 141, (Springer, 1993).Google Scholar
  2. 2.
    D. H. J. de Jongh and R. Parikh, Well-partial orderings and hierarchies, Indagationes Math. 39 (1977) 195–207.CrossRefGoogle Scholar
  3. 3.
    N. Dershowitz, Orderings for term-rewriting systems, Theoretical Computer Sci. 17 (1982) 279–301.CrossRefGoogle Scholar
  4. 4.
    N. Dershowitz and Z. Manna, Proving termination with multiset orderings, Communications ACM 22 (1979) 465–476.CrossRefGoogle Scholar
  5. 5.
    N. Dershowitz and M. Okada, Proof theoretic techniques for term rewriting theory, in: Third Annual Symposium on Logic in Computer Science, 1988, Edinburgh, Scotland, (IEEE, 1988) pp. 104–111.Google Scholar
  6. 6.
    J.-Y. Girard, II 12-logic, part I; dilators, Ann. Math. Logic 21 (1981) 75–219.CrossRefGoogle Scholar
  7. 7.
    J.-Y. Girard, Normal functors, power series and λ-calculus, Ann. Pure Applied Logic 37 (1988) 129–177.CrossRefGoogle Scholar
  8. 8.
    J.-Y. Girard and J. Vauzeilles, Functors and ordinal notations II: A functorial construction of the Bachmann-hierarchy, J. Symbolic Logic 49 (1984) 713–729.Google Scholar
  9. 9.
    R. Hasegawa, Well-ordering of algebras and Kruskal's theorem, in: Logic, Language and Computation, Festschrift in Honor of Satoru Takasu, N. D. Jones, M. Hagiya, M. Sato, eds., Lecture Notes in Computer Science 792, (Springer, 1994) pp. 133–172.Google Scholar
  10. 10.
    G. Higman, Ordering by divisibility in abstract algebras, Proc. London Math. Soc., Third Series 2 (1952) 326–336.Google Scholar
  11. 11.
    A. Joyal, Une théorie combinatoire des séries formelles, Advances Math. 42 (1981) 1–82.CrossRefGoogle Scholar
  12. 12.
    A. Joyal, Foncteurs analytiques et espèces de structures, in: Combinatoire Enumérative, Proceedings, Montreal, Québec, Canada, 1985, G. Labelle, P. Leroux, eds., Lecture Notes in Mathematics 1234, (Springer, 1986) pp. 126–159.Google Scholar
  13. 13.
    J. B. Kruskal, Well-quasi-ordering, the tree theorem, and Vazsonyi's conjecture, Transactions American Math. Soc. 95 (1960) 210–225.Google Scholar
  14. 14.
    P. Lescanne, Uniform termination of term rewriting systems, recursive decomposition ordering with status, in: Ninth Colloquium on Trees in Algebra and Programming, 1984, Bordeaux, France, B. Courcelle ed., (Cambridge University Press, 1984) pp. 181–194.Google Scholar
  15. 15.
    S. Mac Lane and I. Moerdijk, Sheaves in Geometry and Logic, A First Introduction to Topos Theory, (Springer, 1992).Google Scholar
  16. 16.
    U. Martin and E. Scott, The order types of termination orderings on monadic terms, strings and multisets, in: Proc. Eighth Annual IEEE Symposium on Logic in Computer Science, 1992, Montreal, Canada, (IEEE, 1993) pp. 356–363.Google Scholar
  17. 17.
    A. Middeldorp and H. Zantema, Simple termination of rewrite systems, Theoretical Computer Sci., 175 (1997) 127–158.CrossRefGoogle Scholar
  18. 18.
    C. St. J. A. Nash-Williams, On well-quasi-ordering finite trees, Proc. Cambridge Philosophical Soc. 59 (1963) 833–835.Google Scholar
  19. 19.
    K. Sakai, Knuth-Bendix algorithm for Thue system based on kachinuki ordering, ICOT Technical Memorandum: TM-0087, ICOT, Institute for New Generation Computer Technology, Dec. 1984.Google Scholar
  20. 20.
    S. G. Simpson, Nonprovability of certain combinatorial properties of finite trees, in: Harvey Friedman's research on the foundations of mathematics, L. A. Harrington, M. D. Morley, A. Scedrov, S. G. Simpson, eds., (North-Holland, 1985) pp. 87–117.Google Scholar
  21. 21.
    G. Takeuti, Proof Theory, Studies in Logic and the Foundations of Mathematics, Vol. 81, (North-Holland, 1975).Google Scholar
  22. 22.
    A. Weiermann, A functorial property of the Aczel-Buchholz-Feferman function, J. Symbolic Logic, 59 (1994) 945–955.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Ryu Hasegawa
    • 1
  1. 1.Graduate School of MathematicsThe University of TokyoMeguro-ku, TokyoJapan

Personalised recommendations