On Quasi Ordinal Diagram Systems

Mitsuhiro Okada
(Keio University)
Yuta Takahashi
(Nagoya University)

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.

In Maribel Fernández and Ian Mackie: Proceedings Tenth International Workshop on Computing with Terms and Graphs (TERMGRAPH 2018), Oxford, UK, 7th July 2018, Electronic Proceedings in Theoretical Computer Science 288, pp. 38–49.
Published: 6th February 2019.

ArXived at: https://dx.doi.org/10.4204/EPTCS.288.4 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org