Universal Lambda

Universal Lambda is a functional esoteric programming language designed by flatigious in 2008, based on binary lambda calculus, in an attempt to make it more suitable for code golf. It's similar to Lazy K, in that the entire program represents a single lambda calculus term that maps standard input (encoded as a list of Church numerals) to standard output.

Syntax

The program file is interpreted as a stream of bits, which is translated into a lambda term as follows:

• 00 introduces a lambda abstraction.
• 01 represents an application of two subsequent terms; like Unlambda's `.
• 111..10, with n repetitions of the bit 1, refers to the variable of the nth parent lambda; i.e. it is a 1-indexed De Bruijn index in unary.

For example, the S combinator:

λx.λy.λz.xz(yz)

would be represented as:

00 00 00 01 01 1110 10 01 110 10
λ  λ  λ  `  `  x    z  `  y   z

or, packed into bytes,

00000001 01111010 01110100

(Note the trailing zero: after a full program is parsed, the remainder of the program is ignored.)

I/O

After a program is read as a lambda term, it must be applied to standard input. To do so, we need an encoding of strings. We can encode a byte as a Church numeral, and a list by nesting Church pairs:

cons = λa.λb.λx.x a b
nil  = λa.λb.b

Then the input string hello is encoded as:

cons 104 (cons 101 (cons 108 (cons 108 (cons 111 nil))))

Output uses the very same encoding.

Complexity

The lambda calculus is Turing complete, so Universal Lambda obviously also is.

Sample programs

The identity function (λx.x, encoded as 0010) doesn't affect standard input at all, and it's therefore a cat program. Of course, we can pad this four-bit program to a single byte whichever way we want. This means all single-byte programs from space to ? are cat programs.

Let's try to do something more interesting: suppose we want to chop off the first byte of input. In the encoding given above, this is just cdr, or λp.p(λa.λb.b):

  (λp.p(λa.λb.b)) (cons K (cons L (...)))
= (cons K (cons L (...))) (λa.λb.b)
= (λx. x K (cons L (...))) (λa.λb.b)
= (λa.λb.b) K (cons L (...))
= (cons L (...))

So let's encode it:

λ  `  1  λ  λ  1
00 01 10 00 00 10

Which corresponds to the 2-byte program:

00011000 00100000

which we can pad whichever way we want.

External resources

• The original site by flatigious, which also includes some tools that facilitate writing Universal Lambda programs.
• Interpreter which is being maintained on GitHub