# Concatenative binary lambda calculus/combinatory logic

John Tromp defines a version of the lambda calculus that is encoded in binary: https://tromp.github.io/cl/cl.html

a) Does there exist a concatenative version of this language (or its combinatory equivalent)?

b) Does there exist a concatenative version restricted to the primitive recursive functions (e.g. as per Combinators for the Primitive Recursive Functions)?

• I'm not sure what you mean by concatenative. Do you mean something like here: en.wikipedia.org/wiki/Concatenative_programming_language or a language in which the concatenation of any two programs is a valid program?
– cody
Aug 18, 2015 at 14:32
• @cody - Actually, it looks like just the condition that the concatenation of any two programs is a valid program suffices. If anyone can say what languages with this weaker condition are called, I'll edit the question/title accordingly. Aug 18, 2015 at 14:37
• With this weaker condition, I believe that Iota, Jot and Zot are examples of a): semarch.linguistics.fas.nyu.edu/barker/Iota/zot.html Aug 18, 2015 at 14:38
– cody
Aug 18, 2015 at 14:40
• This is a related post. cstheory.stackexchange.com/questions/31883/… Aug 19, 2015 at 0:11

Yes, there exists a version of BLC working similarly to Zot.

Consider the zot implementation at [1], which mimics the original definition at [2]. It defines 3 lambda expressions:

zot = \c.c I

0 = \c.c(\f.f S K)

1 = \c\L.L(\l\R.R(\r.c(l r)))

such that applying zot to a sequence of 0s and 1s produces any desired lambda term. For instance, I = \x.x = zot 1 0 0.

But while it's true that the concatenation of 2 bit sequences A and B is another bit sequence C, the resulting program has little to do with the program for B, since B no longer follows the initial zot term.

The lambda terms for 0 and 1 in zot are very much unlike plain bits.

Is there any way we can use the plain bits 0 = \x\y.x and 1 = \x\y.y instead? It turns out that we can! At the cost of moving all complexity into the initial term. This is what I did in the implementation at [3]. The 195 bit term blc serves the same role as zot above. But by applying it to the sequence of (actual plain) bits that are the BLC code of a lambda term T, we obtain that very term T. For instance, I = \x.x = blc 0 0 1 0

blc is in fact a binary tree containing all closed lambda terms at its leaves, and applying 0/1 is taking the left/right subtree.

It's also possible to reduce the 195 bits to a much smaller 100 bits by using the single point combinator basis A = \x\y\z.x z(y(_.z)) [4].

As per @cody's comment above, if we require only that "the concatenation of any two programs is a valid program" then I believe that Iota, Jot and Zot (semarch.linguistics.fas.nyu.edu/barker/Iota/zot.html) are examples of a).

However, IMO the more interesting question part of the question is b)...