View source for Binary lambda calculus

{{Article for deletion/dated|page=Binary lambda calculus|timestamp=20161229224849|year=2016|month=December|day=29|substed=yes}}
<!-- Once discussion is closed, please place on talk page: {{Old AfD multi|page=Binary lambda calculus|date=29 December 2016|result='''keep'''}} -->
<!-- End of AfD message, feel free to edit beyond this point --> {{⚠️🚨COPIED from en.EverybodyWiki ❗❕⚠️😡😤Please respect Licence CC-BY-SA ❗}}
{{Multiple issues|
{{Original research|date=September 2010}}
{{COI|date=November 2015}}
{{tone|date=February 2016}}
{{Notability|date=June 2016}}
}}

'''Binary lambda calculus''' ('''BLC''') is a minimal, [[purely functional programming language]] invented by John Tromp in 2004,<ref name="RAC">John Tromp, Binary Lambda Calculus and Combinatory Logic, in ''Randomness And Complexity, from Leibniz To Chaitin'', ed. Cristian S. Calude, World Scientific Publishing Company, October 2008. (The last reference, to an initial Haskell implementation, is dated 2004) [http://tromp.github.io/cl/LC.pdf (pdf version)] {{webarchive |url=https://web.archive.org/web/20160304083208/http://tromp.github.io/cl/LC.pdf |date=March 4, 2016 }}</ref>
based on a [[binary encoding]] of the [[untyped lambda calculus]] in [[De Bruijn index]] notation.

==Background==
BLC is designed to provide a very simple and elegant concrete definition of descriptional complexity ([[Kolmogorov complexity]]),
where the complexity of an object is the length of its shortest description.

This is made precise by identifying a description method with a computable function
that transforms bitstrings (descriptions) into objects.
Objects are usually also just bitstrings, but can have additional structure as well, e.g., pairs of strings.

Originally, [[Turing machine]]s, the most well known formalism for computation,
were used for this purpose. But they are somewhat lacking in ease of
construction and composability. Another classical computational formalism,
the [[Lambda calculus]], offers distinct advantages in ease of use.
BLC is the result of incorporating a notion of binary I/O into lambda calculus,
so as to turn it into an effective description method.

==Binary strings in BLC==

BLC represents bits 0 and 1 as the standard lambda booleans
''B''<sub>0</sub> = True and ''B''<sub>1</sub> = False:
:True  = <math>\lambda x\, \lambda y.\, x</math>
:False = <math>\lambda x\, \lambda y.\, y</math>
which can be seen to directly implement the [[if-then-else]] operator.

The standard pairing function
:<math>\langle,\rangle = \lambda x \,\lambda y \,\lambda z.\, z x y</math>
applied to two terms ''M'' and ''N''
:<math>\langle M, N \rangle = \lambda z.\, z M N</math>
can be applied to a boolean to yield the desired component of choice.

BLC represents a string ''s'' = ''b''<sub>0</sub>''b''<sub>1</sub>…''b''<sub>n&minus;1</sub> by repeated pairing as
:<math>\langle B_{b_0}, \langle B_{b_1} \ldots \langle B_{b_{n-1}}, z\rangle \ldots \rangle \rangle </math> which is denoted as <math>s:z\ </math>.

The ''z'' works as a list continuation, that could be a nil list (to end the string) or another string (that would be appended to the original string).

==Delimited versus undelimited==
Descriptional complexity comes in two distinct flavors,
depending on whether the input is considered to be delimited.

Knowing the end of your input makes it easier to describe objects.
For instance, you can just copy the whole input to output.
This flavor is called ''plain'' or ''simple'' complexity.

But in a sense it is additional information. A file system for instance needs to separately
store the length of files. The [[C (programming language)|C language]]
uses the [[null character]] to denote the end of a string,
but this comes at the cost of not having that character available within strings.

The other flavor is called ''prefix'' complexity, named after [[prefix code]]s,
where the machine needs to figure out, from the input read so far, whether it needs
to read more bits. We say that the input is self-delimiting.
This works better for communication channels, since one can send
multiple descriptions, one after the other, and still tell them apart.

In the I/O model of BLC, the flavor is dictated by the choice of ''z''.
When kept as a free variable, and required to appear as part of the output,
then the machine must be working in a self-delimiting manner.
If on the other hand z is a lambda term specifically designed to be easy
to distinguish from any pairing, then the input becomes delimited.
BLC chooses ''False'' for this purpose but gives it the more descriptive alternative name of ''Nil''.
Dealing with lists that may be Nil is straightforward: since
:<math>\langle x, y \rangle\ M\ N = M\ x\ y\ N</math>, and
:<math>Nil\ M\ N = N</math>
one can write functions ''M'' and ''N'' to deal with the two cases, the only caveat being that
''N'' will be passed to ''M'' as its third argument.

==Universality==
One can find a description method ''U'' such that for any other description method ''D'',
there is a constant ''c'' (depending only on ''D'') such that no object takes more than ''c'' extra
bits to describe with method ''U'' than with method ''D''.
BLC is designed to make these constants relatively small.
In fact the constant will be the length of a binary encoding of a ''D''-interpreter written in BLC,
and ''U'' will be a lambda term that parses this encoding and runs this decoded interpreter on the
rest of the input. ''U'' won't even have to know whether the description is delimited or not;
it works the same either way.

BLC not only represents bitstrings as lambda calculus terms, but the other way
around as well.

==Lambda encoding==
First, lambda terms are written in a particular notation using what is known as
[[De Bruijn indices]]. The encoding is then defined recursively as follows
:<math>\widehat{\lambda M}= 00\widehat{M}</math>
:<math>\widehat{M\ N}=01\widehat{M}\widehat{N}</math>
:<math>\widehat{i}=1^i0</math>

For instance, the pairing function <math>\lambda x \lambda y \lambda z. x z y</math>
is written <math>\lambda \lambda \lambda. 1 3 2</math> in De Bruijn format, which has encoding <math>00\ 00\ 00\ 01\ 01\ 10\ 1110\ 110</math>.

A '''closed''' lambda term is one in which all variables are bound, i.e. without any free variables.
In De Bruijn format, this means that an index ''i'' can only appear
within at least ''i'' nested lambdas.
The number of closed terms of size ''n'' bits is given by sequence {{OEIS2C|A114852}}
of the [[On-Line Encyclopedia of Integer Sequences]].

The shortest possible closed term is the identity function <math>\widehat{\lambda 1} = 0010</math>.
In delimited mode, this machine just copies its input to its output.

The [[universal machine]] ''U'' in BLC is then, in De Bruijn format (all indices are single digit):
:<math>(\lambda 1 1) (\lambda \lambda \lambda 1 (\lambda \lambda \lambda \lambda 3 (\lambda 5 (3 (\lambda 2 (3 (\lambda \lambda 3 (\lambda 1 2 3))) (4 (\lambda 4 (\lambda 3 1 (2 1))))))</math>
:<math>(1 (2 (\lambda 1 2)) (\lambda 4 (\lambda 4 (\lambda 2 (1 4))) 5)))) (3 3) 2) (\lambda 1 ((\lambda 1 1) (\lambda 1 1)))</math>

This is in binary:

:0101000110100000000101011000000000011110000101111110011110
:000101110011110000001111000010110110111001111100001111100
:0011100110111101111100111101110110000110010001101000011010
:(only 232 bits (29 bytes) long)

A detailed analysis of machine ''U'' may be found in.<ref name="RAC" />

==BLC Complexity==
In general, complexity of an object can be conditional on several other objects
that are provided as additional argument to the universal machine.
BLC defines Plain (or simple) complexity ''KS'' and prefix complexity ''KP'' by

:<math>\begin{align}
KS(x|y_1,\ldots,y_{k}) &= \min \{ \ell(p)\ |\ U\ (p:Nil)\ y_1\ \ldots\ y_{k} = \ \,x\ \ \ \  \}\\
KP(x|y_1,\ldots,y_{k}) &= \min \{ \ell(p)\ |\ U\ (p:\ z\ \ )\   y_1\ \ldots\ y_{k} = \langle x,z \rangle \}
\end{align}</math>

==Basic Theorems==
The identity program <math>\lambda 1</math> proves that
:<math>KS(x) \leq \ell(x) + 4</math>

The program <math>\lambda \lambda 1 ((\lambda 1 1) (\lambda \lambda \lambda \lambda 2 (4 4) (\lambda \lambda 3 2 (3 2 (2 (5 1 (2 1))))))) (\lambda \lambda \lambda 1 (3 ((\lambda 1 1)</math> <math>(\lambda \lambda \lambda \lambda 1 (\lambda 5 5 (\lambda \lambda 3 5 6 (\lambda 1 (\lambda \lambda 6 1 2) 3)) (\lambda \lambda 5 (\lambda 1 4 3))) (3 1)) (\lambda \lambda 1 (\lambda \lambda 2) 2) (\lambda 1)) (\lambda \lambda 1)) 2)</math>

proves that
:<math>KP(x|\ell(x)) \leq \ell(x)+188</math>

The program
:<math>(\lambda 1 1) (\lambda \lambda \lambda 1 (\lambda 1 (3 (\lambda \lambda 1)) (4 4 (\lambda 1 (\lambda \lambda \lambda 1 (\lambda 4 (\lambda \lambda 5 2 (5 2 (3 1 (2 1)))))) 4 (\lambda 1))))) (\lambda \lambda \lambda 1 (3 ((\lambda 1 1)</math> <math>(\lambda \lambda \lambda \lambda 1 (\lambda 5 5 (\lambda \lambda 3 5 6 (\lambda 1 (\lambda \lambda 6 1 2) 3)) (\lambda \lambda 5 (\lambda 1 4 3))) (3 1)) (\lambda \lambda 1 (\lambda \lambda 2) 2) (\lambda 1)) (\lambda \lambda 1)) 2)</math>

proves that
:<math>KP(x) \leq \ell(\overline{x})+338</math>
where <math>\overline{x}</math> is the [[Levenstein coding|Levenstein code]] for ''x'' defined by
:<math>\begin{array}{ll}
\overline{0} & = 0 \\
\overline{n+1} & = 1\ \overline{\ell(n)}\ n\\
\end{array}</math>
in which we identify numbers and bitstrings according to lexicographic order.
This code has the nice property that for all ''k'',
:<math>\ell(\overline{n}) \leq \ell(n)+\ell(\ell(n))+\cdots+ \ell^{k-1}(n) + O(\ell^k(n))</math>
Furthermore, it makes lexicographic order of delimited numbers coincide with numeric order.

{| class="wikitable" border="1"
|-
! Number !! String !! Delimited
|-
| 0 ||  || 0
|-
| 1 || 0 || 10
|-
| 2 || 1 || 110 0
|-
| 3 || 00 || 110 1
|-
| 4 || 01 || 1110 0 00
|-
| 5 || 10 || 1110 0 01
|-
| 6 || 11 || 1110 0 10
|-
| 7 || 000 || 1110 0 11
|-
| 8 || 001 || 1110 1 000
|-
| 9 || 010 || 1110 1 001
|}

==Halting probability==
The [[halting probability]] of the prefix universal machine is defined as the probability it will output any term that has a closed normal form (this includes all translated strings):
:<math>\Omega_{\lambda} = \sum_{\stackrel{U (p:z) = \langle x,z \rangle}{x\in NF}} 2^{-\ell(p)}</math>

With some effort, we can determine the first 4 bits of this particular number of wisdom:
:<math>\Omega_{\lambda} = .0001\ldots_2</math>
where probability {{math|1=.0001<sub>2</sub>&nbsp;= 2<sup>&minus;4</sup>}} is already contributed by programs {{mono|00100}} and {{mono|00101}} for terms True and False.

==BLC8: byte sized I/O==

While bit streams are nice in theory, they fare poorly in interfacing with the real world.
The language BLC8 is a more practical variation on BLC in which programs operate on a stream of bytes,
where each byte is represented as a delimited list of 8 bits in [[big-endian]] order.

==BLC in the IOCCC 2012==

An implementation of both BLC and BLC8 in the [[C programming language]] won the "Most Functional" award in the 2012 edition of the [[International Obfuscated C Code Contest]].

==References==
<references/>

==External links==
* [http://tromp.github.io/cl/cl.html John's Lambda Calculus and Combinatory Logic Playground]
* [http://www.ioccc.org/2012/tromp/hint.html A Binary Lambda Calculus interpreter in C for the IOCCC]
* [http://arxiv.org/abs/1401.0379 Counting Terms in the Binary Lambda Calculus]

{{DEFAULTSORT:Binary Lambda Calculus}}
[[Category:Algorithmic information theory]]
[[Category:Lambda calculus]]
[[Category:Esoteric programming languages]]
[[Category:Functional languages]] {{Source Wikipedia}}