4 ms·

The theory of concatenative combinators (2007)

104 points by rrampage 3y ago

deleted 3y ago
[deleted]
lkuty 3y ago
"Composition Intuition by Conor Hoekstra | Lambda Days 2023" (https://www.youtube.com/watch?v=Mj8jxYS-hi4 https://www.youtube.com/watch?v=Mj8jxYS-hi4) is all about combinators.
dang 3y ago
Related: The Theory of Concatenative Combinators (2007) - https://news.ycombinator.com/item?id=20849180 https://news.ycombinator.com/item?id=20849180 - Aug 2019 (3 comments) The Theory of Concatenative Combinators (2007) - https://news.ycombinator.com/item?id=12328870 https://news.ycombinator.com/item?id=12328870 - Aug 2016 (2 comments) The Theory of Concatenative Combinators - https://news.ycombinator.com/item?id=11490051 https://news.ycombinator.com/item?id=11490051 - April 2016 (5 comments)
tromp 3y ago
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?
- pohl 3y ago
  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?
  - tromp 3y ago
    That is indeed not the case here, as both systems I discuss are Turing complete.
- js8 3y ago
  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.
  - tromp 3y ago
    A typed combinatory logic is introduced in [1]. [1] https://staff.fnwi.uva.nl/b.vandenberg3/Onderwijs/Proof_Theory_2016/handout_7.pdf https://staff.fnwi.uva.nl/b.vandenberg3/Onderwijs/Proof_Theo...
    - js8 3y ago
      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.
andoando 3y ago
I am very interested in this. Is there any good beginner resources for learning?

104 points by rrampage 3y ago

deleted 3y ago

[deleted]

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

dang 3y ago

Related: The Theory of Concatenative Combinators (2007) - https://news.ycombinator.com/item?id=20849180 https://news.ycombinator.com/item?id=20849180 - Aug 2019 (3 comments) The Theory of Concatenative Combinators (2007) - https://news.ycombinator.com/item?id=12328870 https://news.ycombinator.com/item?id=12328870 - Aug 2016 (2 comments) The Theory of Concatenative Combinators - https://news.ycombinator.com/item?id=11490051 https://news.ycombinator.com/item?id=11490051 - April 2016 (5 comments)

tromp 3y ago

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?

pohl 3y ago
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?
- tromp 3y ago
  That is indeed not the case here, as both systems I discuss are Turing complete.
js8 3y ago
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.
- tromp 3y ago
  A typed combinatory logic is introduced in [1]. [1] https://staff.fnwi.uva.nl/b.vandenberg3/Onderwijs/Proof_Theory_2016/handout_7.pdf https://staff.fnwi.uva.nl/b.vandenberg3/Onderwijs/Proof_Theo...
  - js8 3y ago
    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.

andoando 3y ago

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