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.
|Number of pages||12|
|Journal||Electronic Proceedings in Theoretical Computer Science, EPTCS|
|Publication status||Published - 2019 Jan 1|
|Event||10th International Workshop on Computing with Terms and Graphs, TERMGRAPH 2018 - Oxford, United Kingdom|
Duration: 2018 Jul 7 → 2018 Jul 7
ASJC Scopus subject areas