On quasi ordinal diagram systems

Mitsuhiro Okada, Yuta Takahashi

Research output: Contribution to journalConference article

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.

Original languageEnglish
Pages (from-to)38-49
Number of pages12
JournalElectronic Proceedings in Theoretical Computer Science, EPTCS
Volume288
DOIs
Publication statusPublished - 2019 Jan 1
Event10th International Workshop on Computing with Terms and Graphs, TERMGRAPH 2018 - Oxford, United Kingdom
Duration: 2018 Jul 72018 Jul 7

Fingerprint

Pattern matching

ASJC Scopus subject areas

  • Software

Cite this

On quasi ordinal diagram systems. / Okada, Mitsuhiro; Takahashi, Yuta.

In: Electronic Proceedings in Theoretical Computer Science, EPTCS, Vol. 288, 01.01.2019, p. 38-49.

Research output: Contribution to journalConference article

@article{9b1f7ad2b2a44a179b38f194544b7d48,
title = "On quasi ordinal diagram systems",
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.",
author = "Mitsuhiro Okada and Yuta Takahashi",
year = "2019",
month = "1",
day = "1",
doi = "10.4204/EPTCS.288.4",
language = "English",
volume = "288",
pages = "38--49",
journal = "Electronic Proceedings in Theoretical Computer Science, EPTCS",
issn = "2075-2180",
publisher = "Open Publishing Association",

}

TY - JOUR

T1 - On quasi ordinal diagram systems

AU - Okada, Mitsuhiro

AU - Takahashi, Yuta

PY - 2019/1/1

Y1 - 2019/1/1

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

VL - 288

SP - 38

EP - 49

JO - Electronic Proceedings in Theoretical Computer Science, EPTCS

JF - Electronic Proceedings in Theoretical Computer Science, EPTCS

SN - 2075-2180

ER -