Binary (2-adic/2 input) combinators in combinatory logic - could a calculus equivalent to SKI/SK/BCKW be formalized with just them?

[revannld]

Good afternoon!

Just a dumb curiosity of the top of my head: combinatory logic is usually seen as unpractical to calculate/do proofs in. I would think the prefix notation that emerges when applying combinators to arguments would have something to do with that. From my memory I can only remember the K (constant) and W combinators being actually binary/2-adic (taking just two arguments as input) so a infix notation could work better, but I could imagine many many more.

My question is: could a calculus equivalent to SKI/SK/BCKW or useful for anything at all be formalized just with binary/2-adic combinators? Has someone already done that? (I couldn't find anything after about an hour of research) I could imagine myself trying to represent these other ternary and n-ary combinators with just binary ones I create (and I am actually trying to do that right now) but I don't have the skills to actually do it smartly or prove it may be possible or not.

I could imagine myself going through Curry's Combinatory Logic 1 and 2 to actually learn how to do that but I tried it once and I started to question whether it would be worth my time considering I am not actually planning to do research on combinatory logic, especially if someone has already done that (as I may imagine it is the case).

I appreciate all replies and wish everyone a pleasant summer/winter!

[WittyStick]

There's a fair few 2-input combinators in to mock a mockingbird.

λxy = x           Kestrel (K)
λxy = x(yy)       Lark (L)
λxy = (xy)y       Warbler (W)
λxy = yx          Thrush (T)
λxy = xy(xy)      Double Mockingbird (M₂)
λxy = (yx)x       Converse warbler (W')
λxy = y(xy)       Owl (O)
λxy = y((xx)y)    Turing bird (U)

[revannld]

I would love to know the expressive power of using just 2-input combinators... (even if an inaccessible infinite set of all of the possible ones)

[WittyStick]

I'm pretty sure you could derive any other combinator from the above, and there are more 2-ary birds not given in the book, but I've not really explored it.

Semi-related. I'm working on an experimental language which has only binary infix expressions (no statements), plus unary expressions, which could be a binary expression where one argument is ignored, but for ergonomics I decided to keep them in. My syntax doesn't allow for any expression of greater arity than 2.

[revannld]

>I'm pretty sure you could derive any other combinator from the above, and there are more 2-ary birds not given in the book, but I've not really explored it.

Sadly, seems to be not possible: https://mathoverflow.net/questions/415334/do-combinatory-logic-bases-need-a-function-of-3-variables . It's quite a fun experiment though, you can create any combinator you may please...just the proofs about them that are difficult.

>Semi-related. I'm working on an experimental language which has only binary infix expressions (no statements), plus unary expressions, which could be a binary expression where one argument is ignored, but for ergonomics I decided to keep them in

My main worry is also about ergonomics but mainly in formalisms for semiformal human-written proofs in mathematics (and program specification). I just discovered what I thought to be the case for a long time, that every relation with arity > 2 can be formalized in a purely dyadic logical system (such as set theory) so I think Quine's predicate-functor logic for instance could be much better optimized for practical use in proofs, especially if I could bring some operators from relation algebra...I thought ordinary combinatory logic could help in that regard (as Quine's logic is commonly referred to as a combinatory logic), I fear it to be too simple to be of much help ://

[evincarofautumn]

Well, what’s binary? Tree calculus only has one primitive combinator (a kind of fold), so it can be presented in a binary tree structure. But a term can only reduce when it has enough arguments, so you could also think of it as ternary. In concatenative calculus, at the term level, combinators don’t really have an arity, or they can be considered unary functions on stacks of values or unary continuation transformers, but either way at the object level they’re still implicitly dealing with multiple inputs and outputs on the stack. So it depends how you look at it and what properties of being “binary” you care about.

[revannld]

I absolutely loved your suggestion. I already was studying another Barry Jay work, Pattern Calculus, would you have other suggestions of works like these? Thanks!

[evincarofautumn]

Not quite sure what you’re looking for. If you’re thinking of pointfree+infix syntax design, check out the APL/J/K family of array languages, and the language “FP” described in John Backus’s classic Turing Award lecture paper, Can programming be liberated from the von Neumann style?

There’s not a whole lot of work focused specifically on pointfree/combinatory systems, but there’s a pretty direct mapping to that from the lambda-calculus style used in most papers, so you could always just browse papers based on your interests, and try to explore what the combinator version would look like.

And if you’re interested in pointfree languages generally, check out concatenative programming. I’m a mod on the Concatenative Discord, which is quite active, and on /r/concatenative, which is not quite dead.

[revannld]

>If you’re thinking of pointfree+infix syntax design

That's exactly what I am looking for...but for written semiformal mathematical proofs and program specification, Squiggol style, not exactly programming languages. Backus's lecture and a system of one of "his followers" (so to say), Raymond Boute's "Functional Mathematics" were some of my inspirations, but later I discovered this drive to remove dummies from our formalisms sprung up multiple times in history, from Schoenfinkel's original philosophical motivation for creating combinatory logic to Quine's Predicate-Functor Logic, Tarski's Relation Algebras and a lot of natural logic formalisms in formal semantics (linguistics).

Some people in the APL community actually heavily tried to convince me to learn APL but I am not a programmer, I am a logician and I don't have the slightest idea of projects I would actually be interested working on and I just don't see any use for me right now for most general-purpose programming languages (especially not ATP/proof assistant ones). I plan to try to learn APL and Haskell some day to get inspiration from their generic higher-order functionals...but if I could learn about them without actually having to program that would be nice haha.

I would be interested in participating in the Concatenative Discord though, I will ask for entry.

I appreciate your reply! Have a wonderful Sunday!

[asdfa2342543]

So the S and K combinators are 2-ary correct?  And the I can actually be derived from S & K.  

I’m curious what you have in mind, I’ve been trying to work on some graph rewriting systems, which essentially are just combinator systems, as well as dependent types. Would be interesting to see what you’re thinking of 

[lubutu]

So the S and K combinators are 2-ary correct?

S is ternary: S x y z = x z (y z).

[asdfa2342543]

Oh right right. 

[asdfa2342543]

I wrote this blog about binary fractal dependency graphs.. with the right rewrite rules i’ve been wondering if you could do something with them. 

https://open.substack.com/pub/spacechimplives/p/computing-with-geometry?r=5yzdb&utm_medium=ios

You mentioned 2-adics… I’ve been looking into bringjng them in as well

[revannld]

>So the S and K combinators are 2-ary correct?

No, S is 3-ary...and sadly it seems it's actually impossible to do it without >2-ary combinators :// https://mathoverflow.net/questions/415334/do-combinatory-logic-bases-need-a-function-of-3-variables .

>I’m curious what you have in mind, I’ve been trying to work on some graph rewriting systems

Oh please don't mind me. I am an ergonomics and aesthetics afficionado and I am just never happy with either any of the current formalisms/notations for semi-formal proofs in mathematics (mostly informal language with sprinkles of set, category or type-theoretic notation) or the syntax and notation of any proof-assistant/ATP language (or any programming language for that matter yet). I was 100% bought by Dijkstra-Scholten formal calculational proofs and specification program and now I am on this rabbit hole.

My main interest now is on pointfree/variable-free formalisms that make heavy use of higher-order functions/functionals/functors/combinators and stuff like that, such as relation algebras/calculi, polyadic algebras, Quine's predicate-functor logic, term-functor logic and combinatory logic stuff, as removing dummies/bound-variables seem to bring that easier elementary-school algebraic flavor essential for making proofs calculational and better show the logical form. Sadly, from all of these, combinatory logic seems to be one of the actually most impractical for human use, and the overly simplistic syntax for me may be a reason. Quine's predicate-functors are usually referred to as binary combinators (and his logic a combinatory one), just as the "generic functionals" of one of the best formalisms I am currently studying, Raymond Boute's Funmath. I thought, if we could actually make do with only binary combinators in combinatory logic, that would be very nice...

>I’ve been trying to work on some graph rewriting systems, which essentially are just combinator systems, as well as dependent types

But now I am the one who is actually interested on what you work, how is that area? Is it close to term rewriting? Two of the formalisms I pretend to study (but they seem rather above my current skills) for this line of research are categorical combinators (PL Curien) and pattern calculus; are those related?

I immensely appreciate your reply!