Binary combinatory logic
Binary combinatory logic (BCL) is a complete formulation of combinatory logic (CL) using only the symbols 0 and 1, together with two term-rewriting rules. BCL has applications in the theory of program-size complexity (Kolmogorov complexity).
Definition
Syntax
- <term> ::= 00 | 01 | 1 <term> <term>
Semantics
Rewriting rules for subterms of a given term (parsing from the left):
- 1100xy --> x
- 11101xyz --> 11xz1yz
where x, y, and z are arbitrary terms.
(Note, for example, that because parsing is from the left, 10000 is not a subterm of 11010000.)
The terms 00 and 01 correspond, respectively, to the K and S basis combinators of CL, and the "prefix 1" acts as a left parenthesis (which is sufficient for disambiguation in a CL expression).
There are four equivalent formulations of BCL, depending on the manner of encoding the triplet (left-parenthesis, K, S). These are (1, 00, 01) (as above), (1, 01, 00), (0, 10, 11), and (0, 11, 10).
See also
- Binary lambda calculus
- Iota and Jot -- languages that are similar to BCL, but are more complicated due to unstated λ-calculus syntax and semantics.