On quasi ordinal diagram systems

Authors: Mitsuhiro Okada and Yuta Takahashi

Paper Information

Title:On quasi ordinal diagram systems
Authors:Mitsuhiro Okada and Yuta Takahashi
Proceedings:TERMGRAPH Pre-proceedings
Editors: Maribel Fernandez and Ian Mackie
Keywords:Reduction orderings, termination proofs, ordinal diagram system

ABSTRACT. We generalize the ordinal diagram system (a strong non-monotonic ordinal notation system) of Takeuti in a quasi-well-ordering form. We sketch two ways of showing well-quasi-orderedness; one by means of Dershowitz-Tzameret’s version of tree-embedding theorem with gap-condition (on the path comparable trees), the other by means of the generalized system of transfinite inductive definition. Although the ordinal diagrams (and other strong ordinal notation systems) could be a good tool for termination proof for certain pattern-based rewrite rule programs, there are some difficulties in applying them, at a slight look; the traditional termination proof paradigm of term rewrite theory uses the monotonicity property and the substitution property, but the strong ordering systems do not have them in general. In this paper, we note some possible uses of the strong well-quasi-ordinal systems for termination proofs by taking an example of pattern-based rewrite rules from the hydra game (of Buchholz).

Talk:Jul 07 12:00 (Session 26P: Frameworks)