The theory of concatenative combinators (2007) | Hacker News Reader

The theory of concatenative combinators (2007)

tunes.org

104 pointsrrampage9 comments

The theory of combinatory logic is beautiful. For instance, with basis {S,K}, a term is either S or K or an application of one term to another. S and K satisfy

    S x y z = x z (y z)
    K x y = x

These terms can represent any computable function. This is clean and simple. I don't quite see what the theory of concatenative combinators achieves beyond complicating matters with stacks and quotations to obtain some concatenative property of programs.

Tha analogues of S and K in concatenative combinators are

    [C] [B] [A] s == [[C] B] [C] A
    [B] [A] k == A

which look a bit more complicated, but as the article says this is not even a basis:

> This almost gives us completeness; however, there is no way to form "dip" or "sip" using just "s" and "k" because, roughly speaking, they provide no way to dequote items buried in the stack.

What can you express in concatenative combinators that is not as easily expressed in combinatory logic?

I don’t know anything about combinatory logic, but your question sounds similar to “why study push-down automata if we already know that turning machines are Turning complete?” Maybe I’m way off base in drawing that parallel, and if I am I’m curious why. Aren’t systems like these used to explore the hierarchy of computational power? I’m assuming that studying systems with less power is how those lines are drawn. Is that not the case here?

That is indeed not the case here, as both systems I discuss are Turing complete.

My understanding is that you control evaluation more explicitly in concatenative combinators. Combinatory logic cannot destructure programs, only apply them.

I think this has implications for eta-equivalence of programs. I think there are programs that are equivalent in combinatory logic, but not equivalent under concatenative rules.

I also think it affects type-checking, program in concatenative style can (with additional primitives) express "only evaluate if the program typechecks", while I am not sure combinatory logic can express such a program.

A typed combinatory logic is introduced in [1].

[1] https://staff.fnwi.uva.nl/b.vandenberg3/Onderwijs/Proof_Theo...

Yes, you can do that, but then you can express only well-typed programs in that logic. My point is, I believe, that concatenative language such as Joy doesn't prescribe a specific way to do the evaluation (or type-checking) and as such is less restrictive (or perhaps just different) than combinatory logic. This is despite the fact that they are both Turing-complete in the sense they can emulate each other (there is a subset of combinatory logic programs that correspond to concatenative language and vice versa).

I don't want to hammer on the other analogy, but perhaps your question (why not just use combinatory logic) is kind of like asking why don't we only use natural numbers, if they are set-theoretically equivalent with integers at large, and at the same time a smaller set. The reason is, of course, the integers reveal something about the structure of natural numbers (or do they artificially add this structure, which one is it, really?). I think concatenative combinators can be considered analogous to integers here.

"Composition Intuition by Conor Hoekstra | Lambda Days 2023" (https://www.youtube.com/watch?v=Mj8jxYS-hi4) is all about combinators.

The Theory of Concatenative Combinators (2007) - https://news.ycombinator.com/item?id=20849180 - Aug 2019 (3 comments)

The Theory of Concatenative Combinators (2007) - https://news.ycombinator.com/item?id=12328870 - Aug 2016 (2 comments)

The Theory of Concatenative Combinators - https://news.ycombinator.com/item?id=11490051 - April 2016 (5 comments)

I am very interested in this. Is there any good beginner resources for learning?

Reply on news.ycombinator.com