Binary lambda calculus

Binary lambda calculus (BLC) is a version of lambda calculus with provisions for binary I/O, a standard binary encoding of lambda terms, and a designated universal machine.

The program is as a sequence of bits. The following commands are defined:

• 00x = Lambda function with body x
• 01xy = Apply function x of y
• 1x0 = Where x is zero or more "1" bits, make the de Bruijn index of the lambda, for example 10 is the innermost argument, 110 the second most, 1110 the third most, etc

I/O

A program is a lambda calculus term that transforms an input to an output. Standard input is represented as a list of boolean values, and standard output has the same format. A set bit is 0000110 (True), and an unset bit is 000010 (False). The empty list, called nil, is 000010 (False). A list with multiple elements is represented by the pairing or cons function 00010110xy, where x is the head of the list and y is the tail.

See also

• Binary combinatory logic

External resources

• Binary lambda calculus at Wikipedia (from the Wayback Machine; retrieved on 19 October 2016)
• Wikipedia:Binary combinatory logic
• John's Lambda Calculus and Combinatory Logic Playground