5 Search Results for "Ikebuchi, Mirai"


Document
A Homological Condition on Equational Unifiability

Authors: Mirai Ikebuchi

Published in: LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)


Abstract
Equational unification is the problem of solving an equation modulo equational axioms. In this paper, we provide a relationship between equational unification and homological algebra for equational theories. We will construct a functor from the category of sets of equational axioms to the category of abelian groups. Then, our main theorem gives a necessary condition of equational unifiability that is described in terms of abelian groups associated with equational axioms and homomorphisms between them. To construct our functor, we use a ringoid (a category enriched over the category of abelian groups) obtained from the equational axioms and a free resolution of a "good" module over the ringoid, which was developed by Malbos and Mimram.

Cite as

Mirai Ikebuchi. A Homological Condition on Equational Unifiability. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 61:1-61:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{ikebuchi:LIPIcs.MFCS.2021.61,
  author =	{Ikebuchi, Mirai},
  title =	{{A Homological Condition on Equational Unifiability}},
  booktitle =	{46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
  pages =	{61:1--61:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-201-3},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{202},
  editor =	{Bonchi, Filippo and Puglisi, Simon J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.61},
  URN =		{urn:nbn:de:0030-drops-145010},
  doi =		{10.4230/LIPIcs.MFCS.2021.61},
  annote =	{Keywords: Equational unification, Homological algebra, equational theories}
}
Document
Idempotent Turing Machines

Authors: Keisuke Nakano

Published in: LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)


Abstract
A function f is said to be idempotent if f(f(x)) = f(x) holds whenever f(x) is defined. This paper presents a computation model for idempotent functions, called an idempotent Turing machine. The computation model is necessarily and sufficiently expressive in the sense that not only does it always compute an idempotent function but also every idempotent computable function can be computed by an idempotent Turing machine. Furthermore, a few typical properties of the computation model such as robustness and universality are shown. Our computation model is expected to be a basis of special-purpose (or domain-specific) programming languages in which only but all idempotent computable functions can be defined.

Cite as

Keisuke Nakano. Idempotent Turing Machines. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 79:1-79:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{nakano:LIPIcs.MFCS.2021.79,
  author =	{Nakano, Keisuke},
  title =	{{Idempotent Turing Machines}},
  booktitle =	{46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
  pages =	{79:1--79:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-201-3},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{202},
  editor =	{Bonchi, Filippo and Puglisi, Simon J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.79},
  URN =		{urn:nbn:de:0030-drops-145191},
  doi =		{10.4230/LIPIcs.MFCS.2021.79},
  annote =	{Keywords: Turing machines, Idempotent functions, Computable functions, Computation model}
}
Document
Arithmetic Expression Construction

Authors: Leo Alcock, Sualeh Asif, Jeffrey Bosboom, Josh Brunner, Charlotte Chen, Erik D. Demaine, Rogers Epstein, Adam Hesterberg, Lior Hirschfeld, William Hu, Jayson Lynch, Sarah Scheffler, and Lillian Zhang

Published in: LIPIcs, Volume 181, 31st International Symposium on Algorithms and Computation (ISAAC 2020)


Abstract
When can n given numbers be combined using arithmetic operators from a given subset of {+,-,×,÷} to obtain a given target number? We study three variations of this problem of Arithmetic Expression Construction: when the expression (1) is unconstrained; (2) has a specified pattern of parentheses and operators (and only the numbers need to be assigned to blanks); or (3) must match a specified ordering of the numbers (but the operators and parenthesization are free). For each of these variants, and many of the subsets of {+,-,×,÷}, we prove the problem NP-complete, sometimes in the weak sense and sometimes in the strong sense. Most of these proofs make use of a rational function framework which proves equivalence of these problems for values in rational functions with values in positive integers.

Cite as

Leo Alcock, Sualeh Asif, Jeffrey Bosboom, Josh Brunner, Charlotte Chen, Erik D. Demaine, Rogers Epstein, Adam Hesterberg, Lior Hirschfeld, William Hu, Jayson Lynch, Sarah Scheffler, and Lillian Zhang. Arithmetic Expression Construction. In 31st International Symposium on Algorithms and Computation (ISAAC 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 181, pp. 12:1-12:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{alcock_et_al:LIPIcs.ISAAC.2020.12,
  author =	{Alcock, Leo and Asif, Sualeh and Bosboom, Jeffrey and Brunner, Josh and Chen, Charlotte and Demaine, Erik D. and Epstein, Rogers and Hesterberg, Adam and Hirschfeld, Lior and Hu, William and Lynch, Jayson and Scheffler, Sarah and Zhang, Lillian},
  title =	{{Arithmetic Expression Construction}},
  booktitle =	{31st International Symposium on Algorithms and Computation (ISAAC 2020)},
  pages =	{12:1--12:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-173-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{181},
  editor =	{Cao, Yixin and Cheng, Siu-Wing and Li, Minming},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ISAAC.2020.12},
  URN =		{urn:nbn:de:0030-drops-133568},
  doi =		{10.4230/LIPIcs.ISAAC.2020.12},
  annote =	{Keywords: Hardness, algebraic complexity, expression trees}
}
Document
A Lower Bound of the Number of Rewrite Rules Obtained by Homological Methods

Authors: Mirai Ikebuchi

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)


Abstract
It is well-known that some equational theories such as groups or boolean algebras can be defined by fewer equational axioms than the original axioms. However, it is not easy to determine if a given set of axioms is the smallest or not. Malbos and Mimram investigated a general method to find a lower bound of the cardinality of the set of equational axioms (or rewrite rules) that is equivalent to a given equational theory (or term rewriting systems), using homological algebra. Their method is an analog of Squier’s homology theory on string rewriting systems. In this paper, we develop the homology theory for term rewriting systems more and provide a better lower bound under a stronger notion of equivalence than their equivalence. The author also implemented a program to compute the lower bounds.

Cite as

Mirai Ikebuchi. A Lower Bound of the Number of Rewrite Rules Obtained by Homological Methods. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 24:1-24:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{ikebuchi:LIPIcs.FSCD.2019.24,
  author =	{Ikebuchi, Mirai},
  title =	{{A Lower Bound of the Number of Rewrite Rules Obtained by Homological Methods}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{24:1--24:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.24},
  URN =		{urn:nbn:de:0030-drops-105312},
  doi =		{10.4230/LIPIcs.FSCD.2019.24},
  annote =	{Keywords: Term rewriting systems, Equational logic, Homological algebra}
}
Document
On Repetitive Right Application of B-Terms

Authors: Mirai Ikebuchi and Keisuke Nakano

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)


Abstract
B-terms are built from the B combinator alone defined by B == lambda f.lambda g.lambda x. f~(g~x), which is well-known as a function composition operator. This paper investigates an interesting property of B-terms, that is, whether repetitive right applications of a B-term cycles or not. We discuss conditions for B-terms to have and not to have the property through a sound and complete equational axiomatization. Specifically, we give examples of B-terms which have the property and show that there are infinitely many B-terms which do not have the property. Also, we introduce a canonical representation of B-terms that is useful to detect cycles, or equivalently, to prove the property, with an efficient algorithm.

Cite as

Mirai Ikebuchi and Keisuke Nakano. On Repetitive Right Application of B-Terms. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 18:1-18:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{ikebuchi_et_al:LIPIcs.FSCD.2018.18,
  author =	{Ikebuchi, Mirai and Nakano, Keisuke},
  title =	{{On Repetitive Right Application of B-Terms}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{18:1--18:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.18},
  URN =		{urn:nbn:de:0030-drops-91882},
  doi =		{10.4230/LIPIcs.FSCD.2018.18},
  annote =	{Keywords: Combinatory logic, B combinator, Lambda calculus}
}
  • Refine by Author
  • 3 Ikebuchi, Mirai
  • 2 Nakano, Keisuke
  • 1 Alcock, Leo
  • 1 Asif, Sualeh
  • 1 Bosboom, Jeffrey
  • Show More...

  • Refine by Classification
  • 2 Theory of computation → Rewrite systems
  • 1 Theory of computation → Equational logic and rewriting
  • 1 Theory of computation → Problems, reductions and completeness
  • 1 Theory of computation → Turing machines

  • Refine by Keyword
  • 2 Homological algebra
  • 1 B combinator
  • 1 Combinatory logic
  • 1 Computable functions
  • 1 Computation model
  • Show More...

  • Refine by Type
  • 5 document

  • Refine by Publication Year
  • 2 2021
  • 1 2018
  • 1 2019
  • 1 2020

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