7
$\begingroup$

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)?

$\endgroup$
5
  • 2
    $\begingroup$ 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? $\endgroup$
    – cody
    Aug 18, 2015 at 14:32
  • $\begingroup$ @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. $\endgroup$ Aug 18, 2015 at 14:37
  • 1
    $\begingroup$ With this weaker condition, I believe that Iota, Jot and Zot are examples of a): semarch.linguistics.fas.nyu.edu/barker/Iota/zot.html $\endgroup$ Aug 18, 2015 at 14:38
  • $\begingroup$ You should turn your comment into an answer. $\endgroup$
    – cody
    Aug 18, 2015 at 14:40
  • 1
    $\begingroup$ This is a related post. cstheory.stackexchange.com/questions/31883/… $\endgroup$ Aug 19, 2015 at 0:11

2 Answers 2

1
$\begingroup$

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].

[1] https://github.com/tromp/AIT/blob/master/ait/zot.lam

[2] https://web.archive.org/web/20160312050150/http://semarch.linguistics.fas.nyu.edu/barker/Iota/zot.html

[3] https://github.com/tromp/AIT/blob/master/ait/blc.lam

[4] https://github.com/tromp/AIT/blob/master/ait/allA.lam

$\endgroup$
0
$\begingroup$

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)...

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.