Binary combinatory logic

Binary combinatory logic (BCL) is a computer programming language that uses binary terms 0 and 1 to create a complete formulation of combinatory logic using only the symbols 0 and 1.

[1][2] Utilizing K and S combinators of the Combinatory logic, logical functions can be represented in as functions of combinators: Backus–Naur form: The denotational semantics of BCL may be specified as follows: where "[...]" abbreviates "the meaning of ...".

(The prefix 1 corresponds to a left parenthesis, right parentheses being unnecessary for disambiguation.)

Thus there are four equivalent formulations of BCL, depending on the manner of encoding the triplet (K, S, left parenthesis).

The operational semantics of BCL, apart from eta-reduction (which is not required for Turing completeness), may be very compactly specified by the following rewriting rules for subterms of a given term, parsing from the left: where x, y, and z are arbitrary subterms.