eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2018-07-04
18:1
18:15
10.4230/LIPIcs.FSCD.2018.18
article
On Repetitive Right Application of B-Terms
Ikebuchi, Mirai
1
Nakano, Keisuke
2
Massachusetts Institute of Technology, Cambridge, MA, USA , https://mir-ikbch.github.io/
Tohoku University, Sendai, Miyagi, Japan, http://www.riec.tohoku.ac.jp/~ksk/
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol108-fscd2018/LIPIcs.FSCD.2018.18/LIPIcs.FSCD.2018.18.pdf
Combinatory logic
B combinator
Lambda calculus