📑 Table of Contents▼

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

edit

S-K Basis

edit

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

edit

Backus–Naur form: 

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

Semantics

edit

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

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

edit

References

edit
  1. ^ a b Tromp, John (2007), "Binary lambda calculus and combinatory logic", Randomness and complexity (PDF), World Sci. Publ., Hackensack, NJ, pp. 237–260, CiteSeerX 10.1.1.695.3142, doi:10.1142/9789812770837_0014, ISBN 978-981-277-082-0, MR 2427553.
  2. ^ Devine, Sean (2009), "The insights of algorithmic entropy", Entropy, 11 (1): 85–110, Bibcode:2009Entrp..11...85D, doi:10.3390/e11010085, MR 2534819
  3. ^ a b c Wolfram, Stephen (2021-12-06). "Combinators: A Centennial View". writings.stephenwolfram.com. arXiv:2103.12811. Archived from the original on 2020-12-06. Retrieved 2021-02-17.

Further reading

edit
edit

📚 Artikel Terkait di Wikipedia

Combinatory logic

Combinatory logic is a notation to eliminate the need for quantified variables in mathematical logic. It was introduced by Moses Schönfinkel and Haskell

John Tromp

"the logical rules of Go". He is also known for his work in binary combinatory logic (binary lambda calculus) [citation needed] and lambda diagrams that

Iota and Jot

continuing through the continuation w. Lambda calculus Combinatory logic Binary combinatory logic SKI combinator calculus Barker, Chris. "Zot". The Esoteric

Moses Schönfinkel

1942 (1943)) was a logician and mathematician, known for the invention of combinatory logic. Moses Schönfinkel was born on (1888-09-29)29 September 1888 in Ekaterinoslav

SKI combinator calculus

The SKI combinator calculus is a combinatory logic system and a computational system. It can be thought of as a computer programming language, though

BCL

1066, used by approximately one third of the global population. Binary combinatory logic Bunga Citra Lestari, Indonesian actress and singer Members of the

Mathematical logic

proof theory, especially intuitionistic logic. Formal calculi such as the lambda calculus and combinatory logic are now studied as idealized programming

Outline of logic

Classical logic Computability logic Deontic logic Dependence logic Description logic Deviant logic Doxastic logic Epistemic logic First-order logic Formal