# Binary combinatory logic

Jump to navigation Jump to search

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

## Definition

### Syntax

``` <term> ::= 00 | 01 | 1 <term> <term>
```

### Semantics

The denotational semantics of BCL may be specified as follows:

• `[ 00 ] == K`
• `[ 01 ] == S`
• `[ 1 <term1> <term2> ] == ( [<term1>] [<term2>] ) `

where "`[...]`" abbreviates "the meaning of `...`". Here `K` and `S` are the KS-basis combinators, and `( )` is the application operation, of combinatory logic. (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). These are `(00, 01, 1)` (as in the present version), `(01, 00, 1)`, `(10, 11, 0)`, and `(11, 10, 0)`.

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:

• `  1100xy  → x `
• ` 11101xyz → 11xz1yz `

where `x`, `y`, and `z` are arbitrary subterms. (Note, for example, that because parsing is from the left, `10000` is not a subterm of `11010000`.)