Abstract
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.
Preview
Unable to display preview. Download preview PDF.
References
T. Becker and V. Weispfenning, Grôbner Bases, Graduate Texts in Mathematics 141, (Springer, 1993).
D. H. J. de Jongh and R. Parikh, Well-partial orderings and hierarchies, Indagationes Math. 39 (1977) 195–207.
N. Dershowitz, Orderings for term-rewriting systems, Theoretical Computer Sci. 17 (1982) 279–301.
N. Dershowitz and Z. Manna, Proving termination with multiset orderings, Communications ACM 22 (1979) 465–476.
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.
J.-Y. Girard, II 21 -logic, part I; dilators, Ann. Math. Logic 21 (1981) 75–219.
J.-Y. Girard, Normal functors, power series and λ-calculus, Ann. Pure Applied Logic 37 (1988) 129–177.
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.
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.
G. Higman, Ordering by divisibility in abstract algebras, Proc. London Math. Soc., Third Series 2 (1952) 326–336.
A. Joyal, Une théorie combinatoire des séries formelles, Advances Math. 42 (1981) 1–82.
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.
J. B. Kruskal, Well-quasi-ordering, the tree theorem, and Vazsonyi's conjecture, Transactions American Math. Soc. 95 (1960) 210–225.
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.
S. Mac Lane and I. Moerdijk, Sheaves in Geometry and Logic, A First Introduction to Topos Theory, (Springer, 1992).
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.
A. Middeldorp and H. Zantema, Simple termination of rewrite systems, Theoretical Computer Sci., 175 (1997) 127–158.
C. St. J. A. Nash-Williams, On well-quasi-ordering finite trees, Proc. Cambridge Philosophical Soc. 59 (1963) 833–835.
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.
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.
G. Takeuti, Proof Theory, Studies in Logic and the Foundations of Mathematics, Vol. 81, (North-Holland, 1975).
A. Weiermann, A functorial property of the Aczel-Buchholz-Feferman function, J. Symbolic Logic, 59 (1994) 945–955.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hasegawa, R. (1997). An analysis of divisibility orderings and recursive path orderings. In: Shyamasundar, R.K., Ueda, K. (eds) Advances in Computing Science — ASIAN'97. ASIAN 1997. Lecture Notes in Computer Science, vol 1345. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63875-X_59
Download citation
DOI: https://doi.org/10.1007/3-540-63875-X_59
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63875-9
Online ISBN: 978-3-540-69658-2
eBook Packages: Springer Book Archive