Binary combinatory logic
Encyclopedia
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
).
of BCL may be specified as follows:
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:
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.)
External links
Combinatory logic
Combinatory logic is a notation introduced by Moses Schönfinkel and Haskell Curry to eliminate the need for variables in mathematical logic. It has more recently been used in computer science as a theoretical model of computation and also as a basis for the design of functional programming...
using only the symbols 0 and 1. BCL has applications in the theory of program-size complexity (Kolmogorov complexity
Kolmogorov complexity
In algorithmic information theory , the Kolmogorov complexity of an object, such as a piece of text, is a measure of the computational resources needed to specify the object...
).
Syntax
Backus–Naur form:-
::= 00 | 01 | 1
Semantics
The denotational semanticsDenotational semantics
In computer science, denotational semantics is an approach to formalizing the meanings of programming languages by constructing mathematical objects which describe the meanings of expressions from the languages...
of BCL may be specified as follows:
- [ 00 ]
K
- [ 01 ] S
- [ 1
] ( [ ] [ ] )
where "[...]" abbreviates "the meaning of ...". Here K and S are the KS-basis combinators, and is the application operation, of combinatory logic
Combinatory logic
Combinatory logic is a notation introduced by Moses Schönfinkel and Haskell Curry to eliminate the need for variables in mathematical logic. It has more recently been used in computer science as a theoretical model of computation and also as a basis for the design of functional programming...
. (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
Operational semantics
In computer science, operational semantics is a way to give meaning to computer programs in a mathematically rigorous way. Operational semantics are classified into two categories: structural operational semantics formally describe how the individual steps of a computation take place in a...
of BCL, apart from eta-reduction (which is not required for Turing completeness), may be very compactly specified by the following rewriting
Rewriting
In mathematics, computer science, and logic, rewriting covers a wide range of methods of replacing subterms of a formula with other terms. What is considered are rewriting systems...
rules for subterms of a given term, parsing
Parsing
In computer science and linguistics, parsing, or, more formally, syntactic analysis, is the process of analyzing a text, made of a sequence of tokens , to determine its grammatical structure with respect to a given formal grammar...
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.)
External links