Search Results

Documents authored by Kikuchi, Kentaro

Document
DOI: 10.4230/LIPIcs.FSTTCS.2021.49
Simple Derivation Systems for Proving Sufficient Completeness of Non-Terminating Term Rewriting Systems

Authors: Kentaro Kikuchi and Takahito Aoto

Published in: LIPIcs, Volume 213, 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)

Abstract
A term rewriting system (TRS) is said to be sufficiently complete when each function yields some value for any input. Proof methods for sufficient completeness of terminating TRSs have been well studied. In this paper, we introduce a simple derivation system for proving sufficient completeness of possibly non-terminating TRSs. The derivation system consists of rules to manipulate a set of guarded terms, and sufficient completeness of a TRS holds if there exists a successful derivation for each function symbol. We also show that variations of the derivation system are useful for proving special cases of local sufficient completeness of TRSs, which is a generalised notion of sufficient completeness.
Cite as

Kentaro Kikuchi and Takahito Aoto. Simple Derivation Systems for Proving Sufficient Completeness of Non-Terminating Term Rewriting Systems. In 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 213, pp. 49:1-49:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{kikuchi_et_al:LIPIcs.FSTTCS.2021.49,
  author =	{Kikuchi, Kentaro and Aoto, Takahito},
  title =	{{Simple Derivation Systems for Proving Sufficient Completeness of Non-Terminating Term Rewriting Systems}},
  booktitle =	{41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)},
  pages =	{49:1--49:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-215-0},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{213},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Chekuri, Chandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2021.49},
  URN =		{urn:nbn:de:0030-drops-155602},
  doi =		{10.4230/LIPIcs.FSTTCS.2021.49},
  annote =	{Keywords: Term rewriting, Sufficient completeness, Local sufficient completeness, Non-termination, Derivation rule, Well-founded induction schema}
}
Document
DOI: 10.4230/LIPIcs.RTA.2015.301
Confluence of Orthogonal Nominal Rewriting Systems Revisited

Authors: Takaki Suzuki, Kentaro Kikuchi, Takahito Aoto, and Yoshihito Toyama

Published in: LIPIcs, Volume 36, 26th International Conference on Rewriting Techniques and Applications (RTA 2015)

Abstract
Nominal rewriting systems (Fernandez, Gabbay, Mackie, 2004; Fernandez, Gabbay, 2007) have been introduced as a new framework of higher-order rewriting systems based on the nominal approach (Gabbay, Pitts, 2002; Pitts, 2003), which deals with variable binding via permutations and freshness conditions on atoms. Confluence of orthogonal nominal rewriting systems has been shown in (Fernandez, Gabbay, 2007). However, their definition of (non-trivial) critical pairs has a serious weakness so that the orthogonality does not actually hold for most of standard nominal rewriting systems in the presence of binders. To overcome this weakness, we divide the notion of overlaps into the self-rooted and proper ones, and introduce a notion of alpha-stability which guarantees alpha-equivalence of peaks from the self-rooted overlaps. Moreover, we give a sufficient criterion for uniformity and alpha-stability. The new definition of orthogonality and the criterion offer a novel confluence condition effectively applicable to many standard nominal rewriting systems. We also report on an implementation of a confluence prover for orthogonal nominal rewriting systems based on our framework.
Cite as

Takaki Suzuki, Kentaro Kikuchi, Takahito Aoto, and Yoshihito Toyama. Confluence of Orthogonal Nominal Rewriting Systems Revisited. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 301-317, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{suzuki_et_al:LIPIcs.RTA.2015.301,
  author =	{Suzuki, Takaki and Kikuchi, Kentaro and Aoto, Takahito and Toyama, Yoshihito},
  title =	{{Confluence of Orthogonal Nominal Rewriting Systems Revisited}},
  booktitle =	{26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
  pages =	{301--317},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-85-9},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{36},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.301},
  URN =		{urn:nbn:de:0030-drops-52042},
  doi =		{10.4230/LIPIcs.RTA.2015.301},
  annote =	{Keywords: Nominal rewriting, Confluence, Orthogonality, Higher-order rewriting, alpha-equivalence}
}
Document
DOI: 10.4230/LIPIcs.CSL.2013.395
Proving Strong Normalisation via Non-deterministic Translations into Klop's Extended lambda-Calculus

Authors: Kentaro Kikuchi

Published in: LIPIcs, Volume 23, Computer Science Logic 2013 (CSL 2013)

Abstract
In this paper we present strong normalisation proofs using a technique of non-deterministic translations into Klop's extended lambda-calculus. We first illustrate the technique by showing strong normalisation of a typed calculus that corresponds to natural deduction with general elimination rules. Then we study its explicit substitution version, the type-free calculus of which does not satisfy PSN with respect to reduction of the original calculus; nevertheless it is shown that typed terms are strongly normalising with respect to reduction of the explicit substitution calculus. In the same framework we prove strong normalisation of Sørensen and Urzyczyn's cut-elimination system in intuitionistic sequent calculus.
Cite as

Kentaro Kikuchi. Proving Strong Normalisation via Non-deterministic Translations into Klop's Extended lambda-Calculus. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 395-414, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{kikuchi:LIPIcs.CSL.2013.395,
  author =	{Kikuchi, Kentaro},
  title =	{{Proving Strong Normalisation via Non-deterministic Translations into Klop's Extended lambda-Calculus}},
  booktitle =	{Computer Science Logic 2013 (CSL 2013)},
  pages =	{395--414},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-60-6},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{23},
  editor =	{Ronchi Della Rocca, Simona},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.395},
  URN =		{urn:nbn:de:0030-drops-42108},
  doi =		{10.4230/LIPIcs.CSL.2013.395},
  annote =	{Keywords: Strong normalisation, Klop's extended lambda-calculus, Explicit substitution, Cut-elimination}
}
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 About DROPS Imprint Privacy Contact