my-server
← Wiki Redirected from Binary lambda calculus

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. Using the S and K combinators, complex Boolean algebra functions can be made. BCL has applications in the theory of program-size complexity (Kolmogorov complexity).

Definition

S-K Basis

Utilizing K and S combinators of the Combinatory logic, logical functions can be represented in as functions of combinators:

Syntax

Backus–Naur form:

Semantics

The denotational semantics of BCL may be specified as follows:

  • <code>[ 00 ] == K</code>
  • <code>[ 01 ] == S</code>
  • <code>[ 1 &lt;term1> &lt;term2> ] == ( [&lt;term1>] [&lt;term2>] ) </code>

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

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:

  • <code> &nbsp;1100xy&nbsp;&nbsp;&rarr; x </code>
  • <code> 11101xyz&nbsp;&rarr;&nbsp;11xz1yz </code>

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

BCL can be used to replicate algorithms like Turing machines and Cellular automata, BCL is Turing complete.

See also

References

Further reading

External links