Document Open Access Logo

On Repetitive Right Application of B-Terms

Authors Mirai Ikebuchi, Keisuke Nakano

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2018.18.pdf
  • Filesize: 456 kB
  • 15 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Rewrite systems
Keywords
  • Combinatory logic
  • B combinator
  • Lambda calculus

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

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 Get BibTex

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) https://doi.org/10.4230/LIPIcs.FSCD.2018.18

Author Details

Mirai Ikebuchi
  • Massachusetts Institute of Technology, Cambridge, MA, USA , https://mir-ikbch.github.io/
Keisuke Nakano
  • Tohoku University, Sendai, Miyagi, Japan, http://www.riec.tohoku.ac.jp/~ksk/

Funding

  • Nakano, Keisuke: This work was partially supported by JSPS KAKENHI Grant Number JP25730002 and JP17K00007.

References

  1. Hendrik P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics. Elsevier Science, 1984. Google Scholar
  2. Michael Beeler, Ralph W. Gosper, and Richard C. Schroeppel. HAKMEM. Technical report, Massachusetts Institute of Technology, Cambridge, MA, USA, 1972. Google Scholar
  3. Richard P. Brent. An improved Monte Carlo factorization algorithm. BIT, 20(2):176-184, 1980. Google Scholar
  4. Haskell B. Curry. Grundlagen der Kombinatorischen Logik (Teil II). American Journal of Mathematics, 52(4):789-834, 1930. Google Scholar
  5. Sachio Hirokawa. Principal types of BCK-lambda-terms. Theoretical Computer Science, 107(2):253-276, Jan 1993. Google Scholar
  6. Donald E. Knuth. The Art of Computer Programming, Volume 2 (3rd Ed.): Seminumerical Algorithms. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 1997. Google Scholar
  7. Evgeny S. Ljapin. Semigroups. Translations of Mathematical Monographs. American Mathematical Society, 1968. Google Scholar
  8. Keisuke Nakano. ρ-property of combinators. 29th TRS Meeting in Tokyo, 2008. URL: http://www.jaist.ac.jp/~hirokawa/trs-meeting/original/29.html.
  9. Chris Okasaki. Flattening combinators: surviving without parentheses. Journal of Functional Programming, 13(4):815-822, July 2003. Google Scholar
  10. Raymond M. Smullyan. To Mock a Mockingbird. Knopf Doubleday Publishing Group, 2012. Google Scholar
  11. Rick Statman. The Word Problem for Smullyan’s Lark Combinator is Decidable. Journal of Symbolic Computation, 7(2):103-112, 1989. Google Scholar
  12. Rick Statman. To Type A Mockingbird. Draft paper available from http://tlca.di.unito.it/PAPER/TypeMock.pdf, December 2011.
  13. Johannes Waldmann. Personal communication, March 2013. Google Scholar
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact