Binary combinatory logic
This article may meet Wikipedia's criteria for speedy deletion because: Original research; see Reasons for deletion on Talk page of Binary lambda calculus. For valid criteria, see CSD.
If this article does not meet the criteria for speedy deletion, or you intend to fix it, please remove this notice, but do not remove this notice from pages that you have created yourself. If you created this page and you disagree with the given reason for deletion, you can click the button below and leave a message explaining why you believe it should not be deleted. You can also visit the talk page to check if you have received a response to your message. Note that this article may be deleted at any time if it unquestionably meets the speedy deletion criteria, or if an explanation posted to the talk page is found to be insufficient.
Note to administrators: this article has content on its talk page which should be checked before deletion. Administrators: check links, talk, history (last), and logs before deletion. Consider checking Google.This page was last edited by Toploftical (contribs | logs) at 16:13, 3 June 2016 (UTC) (9 years ago) |
Binary combinatory logic (BCL) is a formulation of combinatory logic using only the symbols 0 and 1.[1] BCL has applications in the theory of program-size complexity (Kolmogorov complexity).[1][2]
Definition
Syntax
- <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.)
See also
References
- ^ a b Tromp, John (2007), "Binary lambda calculus and combinatory logic", Randomness and complexity (PDF), World Sci. Publ., Hackensack, NJ, pp. 237–260, doi:10.1142/9789812770837_0014, MR 2427553.
- ^ Devine, Sean (2009), "The insights of algorithmic entropy", Entropy, 11 (1): 85–110, doi:10.3390/e11010085, MR 2534819
{{citation}}: CS1 maint: unflagged free DOI (link).