# Would a proof that the traveling salesman algorithm can't be encoded on LAL also prove P!=NP?

An answer to the traveling salesman (and similar) problems can be easily verified on light lambda-calculi. Also, if I understand correctly, the light lambda-calculi can compute every polinomial-time computable function. That way, if one can prove that the traveling salesman problem can't be encoded on the light lambda-calculi, that would also prove the problem can't be solved in poly-time, which would also prove P!=NP. Is that correct, or am I confusing some concepts?

• "traveling salesman algorithm" $\: \mapsto \:$ "traveling salesman problem" $\;\;\;$ ? $\hspace{1.98 in}$ – user6973 Jul 29 '15 at 11:54
• Can you please confirm that the article Light types for polynomial time computation in lambda calculus by R. Baillot and K. Terui refers to the same LAL or light lambda calculi as your question. Alternatively, you may also provide a better reference. Based on the comment by Sasho Nikolov, the details of the reduction will be important for answering the question, i.e. which type of encoding you would have to rule out for proving P!=NP. – Thomas Klimpel Jul 31 '15 at 5:55
• Sorry for not answering earlier. Yes, I can confirm that is the calculi I refer. – MaiaVictor Aug 1 '15 at 9:50
• I don't understand what the proposed edit changed. – MaiaVictor Aug 1 '15 at 9:51
• It changed "algorithm" to "problem". $\;$ – user6973 Aug 2 '15 at 16:01

• N!=NP $\mapsto$ P!=NP $\;$ – user6973 Jul 29 '15 at 11:55
• People keep making this mistake: P-hard and P-complete problems are totally irrelevant to P vs NP. They are useful for L vs P or NC vs P. In fact P $\neq$ NP if and only if there exists an NP-hard problem which is not polytime reducible to the language $\{0, 1\}$ (or any non-trivial language). The latter is of course not P-hard unless L=P. – Sasho Nikolov Jul 29 '15 at 14:05