Search Results

Documents authored by Yamada, Akihisa

Document
DOI: 10.4230/LIPIcs.FSCD.2024.27
A Verified Algorithm for Deciding Pattern Completeness

Authors: René Thiemann and Akihisa Yamada

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
Pattern completeness is the property that the left-hand sides of a functional program cover all cases w.r.t. pattern matching. In the context of term rewriting a related notion is quasi-reducibility, a prerequisite if one wants to perform ground confluence proofs by rewriting induction. In order to certify such confluence proofs, we develop a novel algorithm that decides pattern completeness and that can be used to ensure quasi-reducibility. One of the advantages of the proposed algorithm is its simple structure: it is similar to that of a regular matching algorithm and, unlike an existing decision procedure for quasi-reducibility, it avoids enumerating all terms up to a given depth. Despite the simple structure, proving the correctness of the algorithm is not immediate. Therefore we formalize the algorithm and verify its correctness using the proof assistant Isabelle/HOL. To this end, we not only verify some auxiliary algorithms, but also design an Isabelle library on sorted term rewriting. Moreover, we export the verified code in Haskell and experimentally evaluate its performance. We observe that our algorithm significantly outperforms existing algorithms, even including the pattern completeness check of the GHC Haskell compiler.
Cite as

René Thiemann and Akihisa Yamada. A Verified Algorithm for Deciding Pattern Completeness. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 27:1-27:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{thiemann_et_al:LIPIcs.FSCD.2024.27,
  author =	{Thiemann, Ren\'{e} and Yamada, Akihisa},
  title =	{{A Verified Algorithm for Deciding Pattern Completeness}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{27:1--27:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.27},
  URN =		{urn:nbn:de:0030-drops-203566},
  doi =		{10.4230/LIPIcs.FSCD.2024.27},
  annote =	{Keywords: Isabelle/HOL, pattern matching, term rewriting}
}
Document
DOI: 10.4230/LIPIcs.ITP.2023.34
Formalizing Results on Directed Sets in Isabelle/HOL (Proof Pearl)

Authors: Akihisa Yamada and Jérémy Dubut

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)

Abstract
Directed sets are of fundamental interest in domain theory and topology. In this paper, we formalize some results on directed sets in Isabelle/HOL, most notably: under the axiom of choice, a poset has a supremum for every directed set if and only if it does so for every chain; and a function between such posets preserves suprema of directed sets if and only if it preserves suprema of chains. The known pen-and-paper proofs of these results crucially use uncountable transfinite sequences, which are not directly implementable in Isabelle/HOL. We show how to emulate such proofs by utilizing Isabelle/HOL’s ordinal and cardinal library. Thanks to the formalization, we relax some conditions for the above results.
Cite as

Akihisa Yamada and Jérémy Dubut. Formalizing Results on Directed Sets in Isabelle/HOL (Proof Pearl). In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 34:1-34:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{yamada_et_al:LIPIcs.ITP.2023.34,
  author =	{Yamada, Akihisa and Dubut, J\'{e}r\'{e}my},
  title =	{{Formalizing Results on Directed Sets in Isabelle/HOL (Proof Pearl)}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{34:1--34:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.34},
  URN =		{urn:nbn:de:0030-drops-184092},
  doi =		{10.4230/LIPIcs.ITP.2023.34},
  annote =	{Keywords: Directed Sets, Completeness, Scott Continuous Functions, Ordinals, Isabelle/HOL}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSCD.2023.4
Termination of Term Rewriting: Foundation, Formalization, Implementation, and Competition (Invited Talk)

Authors: Akihisa Yamada

Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)

Abstract
Automated termination analysis is a central topic in the research of term rewriting. In this talk, I will first review the theoretical foundation of termination of term rewriting, leading to the recently established tuple interpretation method. Then I will present an Isabelle/HOL formalization of the theory. Although the formalization is based on the existing library IsaFoR (Isabelle Formalization of Rewriting), the present work takes another approach of representing relations (predicates rather than sets) so that the notation is more human friendly. Then I will present a unified implementation of the termination analysis techniques via SMT encoding, leading to the termination prover NaTT. Many tools have been developed for termination analysis and have been competing annually in termCOMP (Termination Competition) for two decades. At the end of the talk, I will share my experience in organizing termCOMP in the last five years.
Cite as

Akihisa Yamada. Termination of Term Rewriting: Foundation, Formalization, Implementation, and Competition (Invited Talk). In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 4:1-4:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{yamada:LIPIcs.FSCD.2023.4,
  author =	{Yamada, Akihisa},
  title =	{{Termination of Term Rewriting: Foundation, Formalization, Implementation, and Competition}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{4:1--4:5},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-277-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{260},
  editor =	{Gaboardi, Marco and van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.4},
  URN =		{urn:nbn:de:0030-drops-179882},
  doi =		{10.4230/LIPIcs.FSCD.2023.4},
  annote =	{Keywords: Term rewriting, Termination, Isabelle/HOL, Competition}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSCD.2020.4
Certifying the Weighted Path Order (Invited Talk)

Authors: René Thiemann, Jonas Schöpf, Christian Sternagel, and Akihisa Yamada

Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)

Abstract
The weighted path order (WPO) unifies and extends several termination proving techniques that are known in term rewriting. Consequently, the first tool implementing WPO could prove termination of rewrite systems for which all previous tools failed. However, we should not blindly trust such results, since there might be problems with the implementation or the paper proof of WPO. In this work, we increase the reliability of these automatically generated proofs. To this end, we first formally prove the properties of WPO in Isabelle/HOL, and then develop a verified algorithm to certify termination proofs that are generated by tools using WPO. We also include support for max-polynomial interpretations, an important ingredient in WPO. Here we establish a connection to an existing verified SMT solver. Moreover, we extend the termination tools NaTT and TTT2, so that they can now generate certifiable WPO proofs.
Cite as

René Thiemann, Jonas Schöpf, Christian Sternagel, and Akihisa Yamada. Certifying the Weighted Path Order (Invited Talk). In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 4:1-4:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{thiemann_et_al:LIPIcs.FSCD.2020.4,
  author =	{Thiemann, Ren\'{e} and Sch\"{o}pf, Jonas and Sternagel, Christian and Yamada, Akihisa},
  title =	{{Certifying the Weighted Path Order}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{4:1--4:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Ariola, Zena M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.4},
  URN =		{urn:nbn:de:0030-drops-123263},
  doi =		{10.4230/LIPIcs.FSCD.2020.4},
  annote =	{Keywords: certification, Isabelle/HOL, reduction order, termination analysis}
}
Document
DOI: 10.4230/LIPIcs.ITP.2019.30
Complete Non-Orders and Fixed Points

Authors: Akihisa Yamada and Jérémy Dubut

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)

Abstract
In this paper, we develop an Isabelle/HOL library of order-theoretic concepts, such as various completeness conditions and fixed-point theorems. We keep our formalization as general as possible: we reprove several well-known results about complete orders, often without any property of ordering, thus complete non-orders. In particular, we generalize the Knaster - Tarski theorem so that we ensure the existence of a quasi-fixed point of monotone maps over complete non-orders, and show that the set of quasi-fixed points is complete under a mild condition - attractivity - which is implied by either antisymmetry or transitivity. This result generalizes and strengthens a result by Stauti and Maaden. Finally, we recover Kleene’s fixed-point theorem for omega-complete non-orders, again using attractivity to prove that Kleene’s fixed points are least quasi-fixed points.
Cite as

Akihisa Yamada and Jérémy Dubut. Complete Non-Orders and Fixed Points. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 30:1-30:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{yamada_et_al:LIPIcs.ITP.2019.30,
  author =	{Yamada, Akihisa and Dubut, J\'{e}r\'{e}my},
  title =	{{Complete Non-Orders and Fixed Points}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{30:1--30:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{Harrison, John and O'Leary, John and Tolmach, Andrew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.30},
  URN =		{urn:nbn:de:0030-drops-110852},
  doi =		{10.4230/LIPIcs.ITP.2019.30},
  annote =	{Keywords: Order Theory, Lattice Theory, Fixed-Points, Isabelle/HOL}
}
Document
DOI: 10.4230/LIPIcs.CSL.2016.8
AC Dependency Pairs Revisited

Authors: Akihisa Yamada, Christian Sternagel, René Thiemann, and Keiichirou Kusakari

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

Abstract
Rewriting modulo AC, i.e., associativity and/or commutativity of certain symbols, is among the most frequently used extensions of term rewriting by equational theories. In this paper we present a generalization of the dependency pair framework for termination analysis to rewriting modulo AC. It subsumes existing variants of AC dependency pairs, admits standard dependency graph analyses, and in particular enjoys the minimality property in the standard sense. As a direct benefit, important termination techniques are easily extended; we describe usable rules and the subterm criterion for AC termination, which properly generalize the non-AC versions. We also perform these extensions within IsaFoR - the Isabelle formalization of rewriting - and thereby provide the first formalization of AC dependency pairs. Consequently, our certifier CeTA now supports checking proofs of AC termination.
Cite as

Akihisa Yamada, Christian Sternagel, René Thiemann, and Keiichirou Kusakari. AC Dependency Pairs Revisited. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 8:1-8:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{yamada_et_al:LIPIcs.CSL.2016.8,
  author =	{Yamada, Akihisa and Sternagel, Christian and Thiemann, Ren\'{e} and Kusakari, Keiichirou},
  title =	{{AC Dependency Pairs Revisited}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{8:1--8:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.8},
  URN =		{urn:nbn:de:0030-drops-65488},
  doi =		{10.4230/LIPIcs.CSL.2016.8},
  annote =	{Keywords: Equational Rewriting, Termination, Dependency Pairs, Certification}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact