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

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,

11000 ``λxx

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

110 0 110101000 ``^ x ``x`x`xxx

``^x ``^y x ``^x 1100 x

``^ x 1100 x 110 10100 1100 10100

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 *C _{n}* of length 2

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!