<p>It is known that <code>K = (λx.(λy.x))</code> and <code>S = (λx.(λy.(λz.((x z) (y z)))))</code> define a turing complete system, and we know procedures to map back and forth from lambda calculus to SK calculus. Now, given two arbitrary combinators, <code>A</code> and <code>B</code> in the set of valid lambda terms, is there an algorithm that will answer whether those combinators define a turing-complete system, and what is the corresponding mapping between a lambda term and those combinators? If not, is there such an algorithm with additional restrictions on the shape of <code>A</code> and <code>B</code> (say, its depth), that could be effectively used to find systems that are similar to SK?</p>

CC BY-SA 3.0
2014-11-13T07:52:25.767Z
Your question is ill-posed, and once it gets fixed it is not research-level. How are the combinators specified, by equations? If so, then there won't be an algorithm because a special case of what you're asking for will be the undecidable semigroup word problem.
Andrej Bauer
CC BY-SA 3.0
2014-11-13T09:14:04.560Z
@AndrejBauer I wonder if it helpful to be so aggressively negative towards the question. I think your comment could be turned into a nice answer.
Martin Berger
CC BY-SA 3.0
2014-11-13T09:40:15.813Z
As we say in Slovenia, I probably got up on my left leg.
Andrej Bauer
CC BY-SA 3.0
2014-11-13T09:52:14.083Z
It's probably undecidable even with one combinator, because you could encode an problem to a combinator such that you can't decide if it's halts or it reduces to some constant basis that is known to generate all combinators.
Zsbán Ambrus
CC BY-SA 3.0
2014-11-13T12:20:37.397Z
How the hell I am supposed to know it is or it is not research level? The fact I don't know the answer kinda implies I don't know the complexity. And getting up from your left leg is not an excuse to being aggressive against a questioner. This is a community. Fix your manners.
MaiaVictor
CC BY-SA 3.0
2014-11-13T18:33:11.130Z
@Viclib: I think you need to fix your manners too.
Dave Clarke
CC BY-SA 3.0
2014-11-14T08:53:04.940Z
It's a perfectly valid question for cstheory. The word problem for (semi-)groups is probably not known in detail to most theoretical computer scientists and is not usually covered in undergraduate texts on group theory. The applicability of word problems to combinators would also be unclear to most CS folk.
Martin Berger
CC BY-SA 3.0
2014-11-14T11:33:34.010Z
Isn't this undecidable simply because of Rice's theorem?
Emil Jeřábek
CC BY-SA 3.0
2014-11-15T13:25:40.467Z
I was completely well mannered until he attacked me, @DaveClarke .
MaiaVictor
CC BY-SA 3.0
2014-11-16T21:59:40.960Z
Whether Andrej is right or not about the question, I don't think he was "agressive". There was no emotion in his comment, just a technical opinion about a question not being well-posed. Viclib, if you don't know enough about your question to know if it is research level, you should ask it at CS.stackexchange.com
Sasho Nikolov
CC BY-SA 3.0
2014-11-16T22:17:35.677Z
Okay, I concede. But is it or is it not research level, after all?
MaiaVictor
CC BY-SA 3.0
2014-11-17T16:59:26.410Z
The problem is definitely research-level, see e.g #6 of http://tlca.di.unito.it/opltlca/, or http://www.win.tue.nl/rtaloop/problems/96.html
cody
CC BY-SA 3.0
2014-11-18T22:14:17.730Z
@cody: They are different problems from the current one.  The current question (after moving the phrase “given two arbitrary combinators A and B” to the appropriate position) is already answered by Emil’s comment, so I do not know what the OP is still waiting for.
Tsuyoshi Ito
CC BY-SA 3.0
2014-11-19T15:23:20.273Z
@TsuyoshiIto: I don't see how they are different; a procedure for verifying whether a finite set of combinators is combinatorially complete seems to be exactly what the OP is asking about. The problem statement specifies that it *is* decidable in the case of linear combinators.
cody
<fl.formal-languages><pl.programming-languages><lambda-calculus>
Is there an algorithm to find whether 2 combinators form a Turing-complete system?
MaiaVictor
# Is there an algorithm to find whether 2 combinators form a Turing-complete system?

(Asked by: username_0 on 2014-11-13)

It is known that `K = (λx.(λy.x))` and `S = (λx.(λy.(λz.((x z) (y z)))))` define a turing complete system, and we know procedures to map back and forth from lambda calculus to SK calculus. Now, given two arbitrary combinators, `A` and `B` in the set of valid lambda terms, is there an algorithm that will answer whether those combinators define a turing-complete system, and what is the corresponding mapping between a lambda term and those combinators? If not, is there such an algorithm with additional restrictions on the shape of `A` and `B` (say, its depth), that could be effectively used to find systems that are similar to SK?

**Tags:** fl.formal-languages, pl.programming-languages, lambda-calculus
> **Comments:**
> **username_1**: Your question is ill-posed, and once it gets fixed it is not research-level. How are the combinators specified, by equations? If so, then there won't be an algorithm because a special case of what you're asking for will be the undecidable semigroup word problem.  
> **username_2**: @AndrejBauer I wonder if it helpful to be so aggressively negative towards the question. I think your comment could be turned into a nice answer.  
> **username_1**: As we say in Slovenia, I probably got up on my left leg.  
> **username_3**: It's probably undecidable even with one combinator, because you could encode an problem to a combinator such that you can't decide if it's halts or it reduces to some constant basis that is known to generate all combinators.  
> **username_0**: How the hell I am supposed to know it is or it is not research level? The fact I don't know the answer kinda implies I don't know the complexity. And getting up from your left leg is not an excuse to being aggressive against a questioner. This is a community. Fix your manners.  
> **username_4**: @Viclib: I think you need to fix your manners too.  
> **username_2**: It's a perfectly valid question for cstheory. The word problem for (semi-)groups is probably not known in detail to most theoretical computer scientists and is not usually covered in undergraduate texts on group theory. The applicability of word problems to combinators would also be unclear to most CS folk.  
> **username_5**: Isn't this undecidable simply because of Rice's theorem?  
> **username_0**: I was completely well mannered until he attacked me, @DaveClarke .  
> **username_6**: Whether Andrej is right or not about the question, I don't think he was "agressive". There was no emotion in his comment, just a technical opinion about a question not being well-posed. Viclib, if you don't know enough about your question to know if it is research level, you should ask it at CS.stackexchange.com  
> **username_0**: Okay, I concede. But is it or is it not research level, after all?  
> **username_7**: The problem is definitely research-level, see e.g #6 of http://tlca.di.unito.it/opltlca/, or http://www.win.tue.nl/rtaloop/problems/96.html  
> **username_8**: @cody: They are different problems from the current one.  The current question (after moving the phrase “given two arbitrary combinators A and B” to the appropriate position) is already answered by Emil’s comment, so I do not know what the OP is still waiting for.  
> **username_7**: @TsuyoshiIto: I don't see how they are different; a procedure for verifying whether a finite set of combinators is combinatorially complete seems to be exactly what the OP is asking about. The problem statement specifies that it *is* decidable in the case of linear combinators.  

---

## 0 answers

