Binary combinatory logic

From Esolang
Jump to: navigation, search

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

External resources