Binary combinatory logic

From Wikipedia, the free encyclopedia
Revision as of 02:38, 24 March 2025 by imported>Citation bot (Altered template type. Added arxiv. | Use this bot. Report bugs. | Suggested by Dominic3203 | Category:Combinatory logic | #UCB_Category 6/9)
(diff) ← Previous revision | Latest revision (diff) | Newer revision → (diff)
Jump to navigation Jump to search

Template:Short description Script error: No such module "Unsubst".

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] 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).[1][2]

Definition

S-K Basis

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

List of Logical Operations as Binary Combinators[3]
Boolean Algebra S-K Basis
True(1) K(KK)
False(0) K(K(SK))
AND SSK
NOT SS(S(S(S(SK))S))(KK)
OR S(SS)S(SK)
NAND S(S(K(S(SS(K(KK)))))))S
NOR S(S(S(SS(K(K(KK)))))(KS))
XOR S(S(S(SS)(S(S(SK)))S))K

Syntax

Backus–Naur form:

 <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.)

File:Rule 110 SK Basis.png
One step of Rule 110 Cellular Automata in SK-Basis(Written in the Wolfram Language).[3]

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

See also

References

Template:Reflist

Further reading

  • Script error: No such module "Citation/CS1".
  • Script error: No such module "citation/CS1".

External links

  1. a b Script error: No such module "citation/CS1"..
  2. Script error: No such module "citation/CS1".
  3. a b c Script error: No such module "Citation/CS1".