On Quasi Ordinal Diagram Systems
Logic in Computer Science
2019-02-07 v1 Programming Languages
Abstract
The purposes of this note are the following two; we first generalize Okada-Takeuti's well quasi ordinal diagram theory, utilizing the recent result of Dershowitz-Tzameret's version of tree embedding theorem with gap conditions. Second, we discuss possible use of such strong ordinal notation systems for the purpose of a typical traditional termination proof method for term rewriting systems, especially for second-order (pattern-matching-based) rewriting systems including a rewrite-theoretic version of Buchholz's hydra game.
Keywords
Cite
@article{arxiv.1902.02012,
title = {On Quasi Ordinal Diagram Systems},
author = {Mitsuhiro Okada and Yuta Takahashi},
journal= {arXiv preprint arXiv:1902.02012},
year = {2019}
}
Comments
In Proceedings TERMGRAPH 2018, arXiv:1902.01510