TY - JOUR
T1 - On quasi ordinal diagram systems
AU - Okada, Mitsuhiro
AU - Takahashi, Yuta
N1 - Funding Information:
∗The first author is supported by KAKENHI 17H02263, 17H02265 and JSPS-AYAME. †The second author is supported by KAKENHI (Grant-in-Aid for JSPS Fellows) 16J04925.
Publisher Copyright:
© M. Okada & Y. Takahashi.
PY - 2019
Y1 - 2019
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85065991229&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85065991229&partnerID=8YFLogxK
U2 - 10.4204/EPTCS.288.4
DO - 10.4204/EPTCS.288.4
M3 - Conference article
AN - SCOPUS:85065991229
SN - 2075-2180
VL - 288
SP - 38
EP - 49
JO - Electronic Proceedings in Theoretical Computer Science, EPTCS
JF - Electronic Proceedings in Theoretical Computer Science, EPTCS
T2 - 10th International Workshop on Computing with Terms and Graphs, TERMGRAPH 2018
Y2 - 7 July 2018 through 7 July 2018
ER -