On properties of $B$-terms
$B$-terms are built from the $B$ combinator alone defined by $B\equiv\lambda fgx. 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 cond...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2020-06-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/5156/pdf |
| _version_ | 1827322732310691840 |
|---|---|
| author | Mirai Ikebuchi Keisuke Nakano |
| author_facet | Mirai Ikebuchi Keisuke Nakano |
| author_sort | Mirai Ikebuchi |
| collection | DOAJ |
| description | $B$-terms are built from the $B$ combinator alone defined by $B\equiv\lambda
fgx. 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 cyclic property and show that there are infinitely
many $B$-terms which do not have the property. Also, we introduce another
interesting property about a canonical representation of $B$-terms that is
useful to detect cycles, or equivalently, to prove the cyclic property, with an
efficient algorithm. |
| first_indexed | 2024-04-25T01:34:35Z |
| format | Article |
| id | doaj.art-83290ea49eb64e348dac791e68c32371 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:34:35Z |
| publishDate | 2020-06-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-83290ea49eb64e348dac791e68c323712024-03-08T10:30:29ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742020-06-01Volume 16, Issue 210.23638/LMCS-16(2:8)20205156On properties of $B$-termsMirai IkebuchiKeisuke Nakano$B$-terms are built from the $B$ combinator alone defined by $B\equiv\lambda fgx. 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 cyclic property and show that there are infinitely many $B$-terms which do not have the property. Also, we introduce another interesting property about a canonical representation of $B$-terms that is useful to detect cycles, or equivalently, to prove the cyclic property, with an efficient algorithm.https://lmcs.episciences.org/5156/pdfcomputer science - logic in computer science03b40 (primary) 68q42 (secondary)f.4.1f.4.2 |
| spellingShingle | Mirai Ikebuchi Keisuke Nakano On properties of $B$-terms Logical Methods in Computer Science computer science - logic in computer science 03b40 (primary) 68q42 (secondary) f.4.1 f.4.2 |
| title | On properties of $B$-terms |
| title_full | On properties of $B$-terms |
| title_fullStr | On properties of $B$-terms |
| title_full_unstemmed | On properties of $B$-terms |
| title_short | On properties of $B$-terms |
| title_sort | on properties of b terms |
| topic | computer science - logic in computer science 03b40 (primary) 68q42 (secondary) f.4.1 f.4.2 |
| url | https://lmcs.episciences.org/5156/pdf |
| work_keys_str_mv | AT miraiikebuchi onpropertiesofbterms AT keisukenakano onpropertiesofbterms |