Binary combinatory logic


Binary combinatory logic is a formulation of combinatory logic using only the symbols 0 and 1. BCL has applications in the theory of program-size complexity.

Definition

Syntax

::= 00 | 01 | 1

Semantics

The denotational semantics of BCL may be specified as follows:
where "" abbreviates "the meaning of ...". Here K and S are the KS-basis combinators, and is the application operation, of combinatory logic.
Thus there are four equivalent formulations of BCL, depending on the manner of encoding the triplet. These are , , , and .
The operational semantics of BCL, apart from eta-reduction, 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.