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 complexity theory.
Definition
Syntax
- <term> ::= 00 | 01 | 1 <term> <term>
Semantics
Given any term, the following two rewriting rules are to be applied (in any order) until neither applies:
- 1100xy --> x
- 11101xyz --> 11xz1yz
where x, y, and z are arbitrary terms.
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).
Alternative equivalent formulations may exchange the rôles of 0 and 1 in the syntax and/or in the rewriting rules.
See also
- Iota and Jot -- languages that are similar to BCL, but are more complicated due to unstated λ-calculus syntax and semantics.