## 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: | 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). |

Pages: | 8 |

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

Paper: |