Keraia

Keraia is a binary encoding of Church's lambda calculus rather in the style of Barker's Zot, and in the spirit of Tromp's Binary Lambda Calculus. Like Zot, programs are preorder traversals of a binary tree, but like BLC, Keraia has a lambda operator with named variables.

Church's lambda operator can be seen as an interpreter. It reads three self-delimiting parameters from the input stream---var, body, and replacement---builds data structures representing the application of the functions and operators that those parameters describe, and performs alpha and beta reduction on the data structures, calling itself recursively. If the process of alpha- and beta-reduction reaches a point where it cannot continue, it decodes the data structure into the normal form of the lambda term and outputs it as a string of symbols.

Since an interpreter is merely a function, we can curry it: the function λ takes an input var and returns a new function λ'; likewise, the function λ' takes a single input body and returns a function λ''; the function λ'' applied to the input replacement yeilds the normal form, if one exists.

Since curried functions take exactly one input, the application operator becomes strictly binary, and the tree of applications is a full binary tree. Programs may be written as preorder traversals of the tree to avoid parentheses.

To explain Keraia in terms of lambda calculus, we adopt the backtick (`) as a prefix application operator; for example, the lambda term S=λ xyz.xz(yz) will be written

``λ x ``λ y ``λ z ``x z `y z
A somewhat easier example is the identity term I=λ x.x:
``λ x x
We can read this as "Apply the interpreter λ to the variable x and the body x." Since the interpreter needs three inputs, the result of the computation above is a function that reads in a replacement y and replaces every x in x with y—clearly the identity function.

Keraia's 1 operator reads in a left tree, a right tree, and pairs them together, producing a data structure. In the implementation on this webpage, the data structure is a string. It uses the function Bit to distinguish 0 from 1 and Cat to create the string. It could just as well have created any other data structure with pure lambda terms; the string just happened to be most convenient in this situation.

Keraia's zero operator reads in three data structures and treats them as a variable, a body, and a replacement, respectively. In order to translate an expression like those above into Keraia, simply send backtick to 1, lambda to zero, and each variable to a preorder traversal of a binary tree. For instance,

I = ``λ x x
becomes 
11000
``λxx
with the variable replacement x → 0, while
S = ``λ x ``λ y ``λ z ``x z `y z
becomes 
110 10100 110 11000 110 0 11 10100 0 1 11000 0
``λ     x ``λ     y ``λ z ``     x z `     y z

Keraia uses a greedy algorithm while marking variables: it traverses body marking occurrences of var, then recursively parses body to mark the rest of the variables. Next, it performs α-reduction and β-reduction until body has reached normal form. Any remaining leaves are replaced by the 0 combinator. Finally, Keraia performs lambda-abstraction and returns a combinator. This means that you have to be careful when choosing traversals to encode the variables. For example, we might expect that this would be an encoding of the K combinator: 

110 0 110 10100 0
``λ x ``λ     y x
However, when Keraia sees that 0 is bound to x it parses the rest of the string as follows: 
110 0 110101000
``^ x ``x`x`xxx
In order to encode a term, start from the innermost varable and work outwards, choosing the smallest tree that is not a substring of what has already been encoded. We choose y → 0: 
``^x ``^y x
``^x 1100 x
At this point, we can't choose 0 for x, since we chose it for y; we can't choose 100, since that appears in 1100; so we choose 10100 for x: 
``^     x 1100     x
110 10100 1100 10100
Thus, we have K = 11010100110010100.

Keraia's encodings of lambda terms are larger than BLC's for small lambda terms, but BLC's variables are encoded in unary, whereas Keraia's terms are binary trees (each variable is a preorder traversal of a binary tree and there are Cn of length 2n+1, where Cn is the nth Catalan number). So for terms of less than 25 variables, BLC will usually give a shorter encoding. Keraia wins on Klop's fixpoint combinator

Yk = LLLLLLLLLLLLLLLLLLLLLLLLLLLL
where
L = λabcdefghijklmnopqstuvwxyzr.r(thisisafixedpointcombinator).

Keraia, because of the continuized combinators, has a very short self-simulator: 111000 (read as, "Apply the identity function to what follows"). Iota and Zot have a smaller one, 1100, read the same way. Tromp conjectured in his BLC paper (page 7) that BLC has the smallest self-interpreter for lambda calculus; if he continuized in this way, he'd have the far smaller self-interpreter 010010.

Give it a try!