<p>At the request of Andrej and PhD, I am turning my comment into an answer, with apologies for self-advertising.</p>

<p>I recently wrote a <a href="http://www-lipn.univ-paris13.fr/~mazza/papers/ChurchCookLevin.pdf" rel="nofollow noreferrer">paper</a> in which I look at how to prove the Cook-Levin theorem ($\mathsf{NP}$-completeness of SAT) using a functional language (a variant of the λ-calculus) instead of Turing machines. A summary:</p>

<ul>
<li>the key notion is that of affine approximations, i.e., approximating arbitrary programs by affine ones (which may use their inputs at most once); the intuition is that
$$\frac{\text{Boolean circuits}}{\text{Turing machines}}=\frac{\text{affine $\lambda$-terms}}{\text{$\lambda$-terms}}$$
so affine $\lambda$-terms approximate arbitrary computations arbitrary well just like Boolean circuits;</li>
<li>the upshot is that, in the $\lambda$-calculus world, the proof is much "higher-level", it uses order theory, Scott-continuity, etc. instead of hacking Boolean circuits; in particular, the slogan "computation is local" (which is given by many as the message underlying the Cook-Levin theorem) becomes "computation is continuous", as expected;</li>
<li>however, the "natural" $\mathsf{NP}$-complete problem is not CIRCUIT SAT but HO CIRCUIT SAT, a kind of "solvability" of linear λ-terms or, more precisely, linear logic proof nets (which are like higher-order Boolean circuits);</li>
<li>of course, one may then reduce HO CIRCUIT SAT to CIRCUIT SAT, thus proving the usual Cook-Levin theorem, and the gory, low-level details are all moved to building such a reduction.</li>
</ul>

<p>So the only thing that would change "on this side of the planet" is, perhaps, that we would have considered a λ-calculus-related problem, instead of Boolean-circuit-related problem, to be the "primordial" $\mathsf{NP}$-complete problem.</p>

<p>A side note: the above-mentioned proof could be reformulated in a variant of Accattoli's $\lambda$-calculus with linear explicit substitutions mentioned in Andrej's answer, which is perhaps more standard than the $\lambda$-calculus I use in my paper.</p>

<hr>

<p><strong>Later edit:</strong> my answer was just a bit more than a cut-and-paste from my comment and I realize that something more should be said concerning the heart of the question which, as I understand it, is: <em>would it be possible to develop the theory of $\mathsf{NP}$-completeness without Turing machines?</em></p>

<p>I agree with Kaveh's comment: the answer is <em>yes</em>, but perhaps only restrospectively.  That is, when it comes to complexity (counting time and space), Turing machines are unbeatable in simplicity, the cost model is self-evident for time and almost self-evident for space.  In the $\lambda$-calculus, things are far less evident: time cost models as those mentioned by Andrej and given in Harper's book are from the mid-90s, space cost models are still almost non-existing (I am aware of essentially one work <a href="http://www.cs.cmu.edu/~spoons/papers/parallel/icfp08.pdf" rel="nofollow noreferrer">published in 2008</a>).</p>

<p>So, of course we can do everything using the purely functional perspective, but it is hard to imagine an alternative universe in which Hartmanis and Stearns define complexity classes using $\lambda$-terms and, 30 to 50 years later, people start adapting their work to Turing machines.</p>

<p>Then, as Kaveh points out, there is the "social" aspect: people were convinced that $\mathsf{NP}$-completeness is important because Cook proved that a problem considered to be central in a widely studied field (theorem proving) is $\mathsf{NP}$-complete (or, in more modern terminology, using Karp reductions, $\mathsf{coNP}$-complete). Although the above shows that this may be done in the $\lambda$-calculus, maybe it would not be the most immediate thing to do (I have my reserves on this point but let's not make this post too long).</p>

<p>Last but not least, it is worth observing that, even in my work mentioned above, when I show that HO CIRCUIT SAT may be reduced to CIRCUIT SAT, I do not explicitly show a $\lambda$-term computing the reduction and prove that it always normalizes in a polynomial number of leftmost reduction steps; I just show that there is an algorithm which, intuitively, may be implemented in polynomial time, just like any complexity theorist would not explicitly build a Turing machine and prove it polytime (which, let me say it, would be even crazier than writing down a $\lambda$-term, let alone check for mistakes).</p>

<p>This phenomenon is pervasive in logic and computability theory, complexity theory just inherits it: formal systems and models of computation are often used only to know that one <em>can</em> formalize intuitions; after that, intuition alone is almost always enough (as long as used carefully).  So reasoning about the difficulty of solving problems like SAT, TAUT, SUBSET SUM, GI etc., and thus developing the theory of $\mathsf{NP}$-completeness, may largely be done independently of the underlying computational model, as long as a reasonable cost model is found. The $\lambda$-calculus, Turing machines or <a href="https://en.wikipedia.org/wiki/Brainfuck" rel="nofollow noreferrer">Brainfuck programs</a>, it doesn't really matter if you know that your intuitions are sound. Turing machines gave an immediate, workable answer, and people didn't (and still do not) feel the need to go further.</p>

CC BY-SA 3.0
2016-12-05T18:51:03.590Z
Just a clarification many miss: Steve proved NP-completeness for TAUT, the proof for SAT is implicit there in there. The notion of Karp reduction did not exist at the time. It is also important to note that TAUT was the reason why Steve got interested in the topic and is central to automatic theorem proving, would people be as interested in solvability of linear lambda terms? The alternative development is possible, but would it happen without the foreknowledge of NP-completeness? I find that unlikely considering that the alternative development is rather recent. :)
Kaveh
CC BY-SA 3.0
2016-12-06T03:19:57.197Z
I remember reading somewhere that part of Levin's motivation to develop NP-completeness was the inability to solve Graph Isomorphism and Minimum Circuit Size Problem (MCSP), and the hope to show that they were (what we would now call) NP-hard. At least GI would've still existed in a world of lambdas...
Joshua Grochow
CC BY-SA 3.0
2016-12-06T10:25:19.990Z
@Kaveh, thanks for your comment, I added some paragraphs to complete the answer.
Damiano Mazza
CC BY-SA 3.0
2016-12-07T09:26:27.343Z
@Josh, so would TAUT and SAT.
Kaveh
CC BY-SA 3.0
2016-12-05T12:15:03.643Z
2016-12-07T12:37:23.247Z
2016-12-07T12:37:23.247Z
Damiano Mazza
<p>Yes, via Ordinary Differential Equations.</p>
<p><a href="https://dl.acm.org/doi/abs/10.1145/3127496" rel="nofollow noreferrer">Bournez et al.</a> described a connection between Turing Machines and <a href="https://%20From%20their%20abstractIn%202017,%20%5BBournez%20et%20al.%5D%5B1%5D%20gave%20an%20implicit%20characterization%20of%20%5Bpolynomial%20time%20computation%5D%5B2%5D%20in%20terms%20of%20%5Bordinary%20differential%20equations%5D%5B3%5D%20and%20proved%20that%20the%201941%20General%20Purpose%20Analog%20Computer%20(GPAC)%20of%20Claude%20Shannon%20is%20provably%20equivalent%20to%20Turing%20machines%20both%20in%20terms%20of%20computability%20and%20complexity." rel="nofollow noreferrer">Ordinary Differential Equations (ODE)</a>. Such connection preserves the notion of <a href="https://en.wikipedia.org/wiki/P_(complexity)" rel="nofollow noreferrer">polynomiality</a> by looking at the length of the function that solves the ODE. This means that the notion of polynomiality of a problem can be linked directly to properties of ODE independently of any machine or whatever.</p>

CC BY-SA 4.0
2024-04-12T11:54:22.413Z
Are you sure you are pointing at the right article? From the abstract of the article you point at, the authors prove "an implicit characterization of polynomial time computation in terms of ordinary differential equations", which seem to imply a definition of P rather than NP?
J.y B.y
CC BY-SA 4.0
2024-04-11T11:41:50.590Z
2024-04-12T11:52:38.800Z
2024-04-12T11:52:38.800Z
HeMath
<p>You may wish to look at <strong>cost semantics for functional languages</strong>. These are various computational complexity measures for functional languages that do <em>not</em> pass through any kind of Turing machine, RAM machine, etc. A good place to start looking is <a href="http://lambda-the-ultimate.org/node/5021" rel="noreferrer">this Lambda the Ultimate post</a>, which has some good further references.</p>

<p>Section 7.4 of Bob Harper's <a href="http://www.cs.cmu.edu/~rwh/pfpl.html" rel="noreferrer">Practical Foundations for Programming Languages</a> explains the costs semantics.</p>

<p>The paper <a href="https://arxiv.org/abs/1505.03791" rel="noreferrer">On the relative usefulness of fireballs</a> by Accattoli and Coen shows that $\lambda$-calculus has at most linear blowup with respect to RAM machine model.</p>

<p>In summary, on this other planet things would be pretty much the same with regards to NP, but there would be fewer buffer overflows, and there wouldn't be as much garbage lying around.</p>

CC BY-SA 3.0
2016-11-28T22:00:46.523Z
I suppose the untyped $\lambda$-calculus people would still invent (pure) scheme. Oh well.
Andrej Bauer
CC BY-SA 3.0
2016-11-28T22:16:52.953Z
That's a nice link on the LtU post. But any links to concrete examples of proving this class of "NP" with problems like 3Sat? Curios to see a "proof" in lambda calculus
PhD
CC BY-SA 3.0
2016-12-01T18:30:09.127Z
Damiano, you could post your comments as a proper answer which demonstrates that one *can* do NP-related theory directly in $\lambda$-calculus.
Andrej Bauer
CC BY-SA 3.0
2016-12-05T01:25:31.397Z
@DamianoMazza - I agree with Andrej and believe your comment should be an answer
PhD
CC BY-SA 3.0
2016-12-05T12:16:08.700Z
@Andrej: Done!  I removed my previous comments.
Damiano Mazza
CC BY-SA 3.0
2016-11-28T21:59:40.357Z
2016-11-28T21:59:40.357Z
Andrej Bauer
<p>From a purely abstract math/computational reasoning point of view, (how) could one even discover or reason about problems like 3-SAT, Subset Sum, Traveling Salesman etc.,? Would we be even able to reason about them in any meaningful way with just the <em>functional</em> point of view? Would it even be possible?</p>

<p>I've been mulling on this question purely from a point of self inquiry as part of learning the lambda calculus model of computation. I understand that it's "non-intuitive" and that's why Godel favored the Turing model. However, I just wish to know what are the known theoretical limitations of this <em>functional</em> style of computation and how much of a hindrance would it be for analyzing the NP class of problems?</p>

CC BY-SA 3.0
2016-11-28T22:02:16.467Z
This is not a research-level question for someone who does programming language theory professionally, but I still don't think the qustion deserves all the downvotes. Could the downvoters tell us what bothers them? Perhaps the question can be improved.
Andrej Bauer
CC BY-SA 3.0
2016-11-28T22:07:58.500Z
@AndrejBauer: I downvoted because (1) I think that the (polynomial) equivalence between Turing machines and the lambda calculus is fairly well-known, and (2) the post has a lot of fluff which masks that as the core question. However, your answer shows that there is more going on than I thought, so I may reverse my vote.
Huck Bennett
CC BY-SA 3.0
2016-11-28T22:09:28.450Z
I agree that the fluff belongs to Discovery Channel.
Andrej Bauer
CC BY-SA 3.0
2016-11-28T22:13:47.247Z
@AndrejBauer, HuckBennet: I initially was deciding to post this on the computer science portal but I couldn't find the relevant tags and hence posted it here. I removed the fluff to help be direct with what it is that I want to know. I've left my "reason" for asking the question and hence tagged it as a soft question. I'm genuinely interested in knowing how one could analyze NP problems purely from a functional perspective and if there is indeed any value in doing that - with the hope that I understand something more deeply about lambda calculus
PhD
CC BY-SA 3.0
2016-11-29T03:36:15.203Z
I think the core of your question is if complexity could be developed using lambda calculus. The answer is yes, and there is an old question asking that on the site iirc.
Kaveh
CC BY-SA 3.0
2016-11-29T03:38:39.797Z
Btw, you are confusing computational problems with computational models to some extend. SAT, etc. after computational problems and they would and would still exist without complexity theory.
Kaveh
<soft-question><lambda-calculus><turing-machines><functional-programming><np>
(How) Could we discover/analyze NP problems in the absence of the Turing model of computation?
PhD
# (How) Could we discover/analyze NP problems in the absence of the Turing model of computation?

(Asked by: username_0 on 2016-11-28)

From a purely abstract math/computational reasoning point of view, (how) could one even discover or reason about problems like 3-SAT, Subset Sum, Traveling Salesman etc.,? Would we be even able to reason about them in any meaningful way with just the *functional* point of view? Would it even be possible?

I've been mulling on this question purely from a point of self inquiry as part of learning the lambda calculus model of computation. I understand that it's "non-intuitive" and that's why Godel favored the Turing model. However, I just wish to know what are the known theoretical limitations of this *functional* style of computation and how much of a hindrance would it be for analyzing the NP class of problems?

**Tags:** soft-question, lambda-calculus, turing-machines, functional-programming, np
> **Comments:**
> **username_1**: This is not a research-level question for someone who does programming language theory professionally, but I still don't think the qustion deserves all the downvotes. Could the downvoters tell us what bothers them? Perhaps the question can be improved.  
> **username_2**: @AndrejBauer: I downvoted because (1) I think that the (polynomial) equivalence between Turing machines and the lambda calculus is fairly well-known, and (2) the post has a lot of fluff which masks that as the core question. However, your answer shows that there is more going on than I thought, so I may reverse my vote.  
> **username_1**: I agree that the fluff belongs to Discovery Channel.  
> **username_0**: @AndrejBauer, HuckBennet: I initially was deciding to post this on the computer science portal but I couldn't find the relevant tags and hence posted it here. I removed the fluff to help be direct with what it is that I want to know. I've left my "reason" for asking the question and hence tagged it as a soft question. I'm genuinely interested in knowing how one could analyze NP problems purely from a functional perspective and if there is indeed any value in doing that - with the hope that I understand something more deeply about lambda calculus  
> **username_3**: I think the core of your question is if complexity could be developed using lambda calculus. The answer is yes, and there is an old question asking that on the site iirc.  
> **username_3**: Btw, you are confusing computational problems with computational models to some extend. SAT, etc. after computational problems and they would and would still exist without complexity theory.  

---

## 3 answers

### Answer by username_1 on 2016-11-28. Score: 18 | Accepted answer

You may wish to look at **cost semantics for functional languages**. These are various computational complexity measures for functional languages that do *not* pass through any kind of Turing machine, RAM machine, etc. A good place to start looking is [this Lambda the Ultimate post](http://lambda-the-ultimate.org/node/5021), which has some good further references.

Section 7.4 of Bob Harper's [Practical Foundations for Programming Languages](http://www.cs.cmu.edu/~rwh/pfpl.html) explains the costs semantics.

The paper [On the relative usefulness of fireballs](https://arxiv.org/abs/1505.03791) by Accattoli and Coen shows that $\lambda$-calculus has at most linear blowup with respect to RAM machine model.

In summary, on this other planet things would be pretty much the same with regards to NP, but there would be fewer buffer overflows, and there wouldn't be as much garbage lying around.

> **Comments:**
> **username_1**: I suppose the untyped $\lambda$-calculus people would still invent (pure) scheme. Oh well.  
> **username_0**: That's a nice link on the LtU post. But any links to concrete examples of proving this class of "NP" with problems like 3Sat? Curios to see a "proof" in lambda calculus  
> **username_1**: Damiano, you could post your comments as a proper answer which demonstrates that one *can* do NP-related theory directly in $\lambda$-calculus.  
> **username_0**: @DamianoMazza - I agree with Andrej and believe your comment should be an answer  
> **username_4**: @Andrej: Done!  I removed my previous comments.  

---

### Answer by username_4 on 2016-12-05. Score: 15

At the request of Andrej and PhD, I am turning my comment into an answer, with apologies for self-advertising.

I recently wrote a [paper](http://www-lipn.univ-paris13.fr/~mazza/papers/ChurchCookLevin.pdf) in which I look at how to prove the Cook-Levin theorem ($\mathsf{NP}$-completeness of SAT) using a functional language (a variant of the λ-calculus) instead of Turing machines. A summary:

* the key notion is that of affine approximations, i.e., approximating arbitrary programs by affine ones (which may use their inputs at most once); the intuition is that
  $$\frac{\text{Boolean circuits}}{\text{Turing machines}}=\frac{\text{affine $\lambda$-terms}}{\text{$\lambda$-terms}}$$
  so affine $\lambda$-terms approximate arbitrary computations arbitrary well just like Boolean circuits;
* the upshot is that, in the $\lambda$-calculus world, the proof is much "higher-level", it uses order theory, Scott-continuity, etc. instead of hacking Boolean circuits; in particular, the slogan "computation is local" (which is given by many as the message underlying the Cook-Levin theorem) becomes "computation is continuous", as expected;
* however, the "natural" $\mathsf{NP}$-complete problem is not CIRCUIT SAT but HO CIRCUIT SAT, a kind of "solvability" of linear λ-terms or, more precisely, linear logic proof nets (which are like higher-order Boolean circuits);
* of course, one may then reduce HO CIRCUIT SAT to CIRCUIT SAT, thus proving the usual Cook-Levin theorem, and the gory, low-level details are all moved to building such a reduction.

So the only thing that would change "on this side of the planet" is, perhaps, that we would have considered a λ-calculus-related problem, instead of Boolean-circuit-related problem, to be the "primordial" $\mathsf{NP}$-complete problem.

A side note: the above-mentioned proof could be reformulated in a variant of Accattoli's $\lambda$-calculus with linear explicit substitutions mentioned in Andrej's answer, which is perhaps more standard than the $\lambda$-calculus I use in my paper.

---

**Later edit:** my answer was just a bit more than a cut-and-paste from my comment and I realize that something more should be said concerning the heart of the question which, as I understand it, is: *would it be possible to develop the theory of $\mathsf{NP}$-completeness without Turing machines?*

I agree with Kaveh's comment: the answer is *yes*, but perhaps only restrospectively. That is, when it comes to complexity (counting time and space), Turing machines are unbeatable in simplicity, the cost model is self-evident for time and almost self-evident for space. In the $\lambda$-calculus, things are far less evident: time cost models as those mentioned by Andrej and given in Harper's book are from the mid-90s, space cost models are still almost non-existing (I am aware of essentially one work [published in 2008](http://www.cs.cmu.edu/~spoons/papers/parallel/icfp08.pdf)).

So, of course we can do everything using the purely functional perspective, but it is hard to imagine an alternative universe in which Hartmanis and Stearns define complexity classes using $\lambda$-terms and, 30 to 50 years later, people start adapting their work to Turing machines.

Then, as Kaveh points out, there is the "social" aspect: people were convinced that $\mathsf{NP}$-completeness is important because Cook proved that a problem considered to be central in a widely studied field (theorem proving) is $\mathsf{NP}$-complete (or, in more modern terminology, using Karp reductions, $\mathsf{coNP}$-complete). Although the above shows that this may be done in the $\lambda$-calculus, maybe it would not be the most immediate thing to do (I have my reserves on this point but let's not make this post too long).

Last but not least, it is worth observing that, even in my work mentioned above, when I show that HO CIRCUIT SAT may be reduced to CIRCUIT SAT, I do not explicitly show a $\lambda$-term computing the reduction and prove that it always normalizes in a polynomial number of leftmost reduction steps; I just show that there is an algorithm which, intuitively, may be implemented in polynomial time, just like any complexity theorist would not explicitly build a Turing machine and prove it polytime (which, let me say it, would be even crazier than writing down a $\lambda$-term, let alone check for mistakes).

This phenomenon is pervasive in logic and computability theory, complexity theory just inherits it: formal systems and models of computation are often used only to know that one *can* formalize intuitions; after that, intuition alone is almost always enough (as long as used carefully). So reasoning about the difficulty of solving problems like SAT, TAUT, SUBSET SUM, GI etc., and thus developing the theory of $\mathsf{NP}$-completeness, may largely be done independently of the underlying computational model, as long as a reasonable cost model is found. The $\lambda$-calculus, Turing machines or [Brainfuck programs](https://en.wikipedia.org/wiki/Brainfuck), it doesn't really matter if you know that your intuitions are sound. Turing machines gave an immediate, workable answer, and people didn't (and still do not) feel the need to go further.

> **Comments:**
> **username_3**: Just a clarification many miss: Steve proved NP-completeness for TAUT, the proof for SAT is implicit there in there. The notion of Karp reduction did not exist at the time. It is also important to note that TAUT was the reason why Steve got interested in the topic and is central to automatic theorem proving, would people be as interested in solvability of linear lambda terms? The alternative development is possible, but would it happen without the foreknowledge of NP-completeness? I find that unlikely considering that the alternative development is rather recent. :)  
> **username_5**: I remember reading somewhere that part of Levin's motivation to develop NP-completeness was the inability to solve Graph Isomorphism and Minimum Circuit Size Problem (MCSP), and the hope to show that they were (what we would now call) NP-hard. At least GI would've still existed in a world of lambdas...  
> **username_4**: @Kaveh, thanks for your comment, I added some paragraphs to complete the answer.  
> **username_3**: @Josh, so would TAUT and SAT.  

---

### Answer by username_6 on 2024-04-11. Score: 2

Yes, via Ordinary Differential Equations.

[Bournez et al.](https://dl.acm.org/doi/abs/10.1145/3127496) described a connection between Turing Machines and [Ordinary Differential Equations (ODE)](https://%20From%20their%20abstractIn%202017,%20%5BBournez%20et%20al.%5D%5B1%5D%20gave%20an%20implicit%20characterization%20of%20%5Bpolynomial%20time%20computation%5D%5B2%5D%20in%20terms%20of%20%5Bordinary%20differential%20equations%5D%5B3%5D%20and%20proved%20that%20the%201941%20General%20Purpose%20Analog%20Computer%20(GPAC)%20of%20Claude%20Shannon%20is%20provably%20equivalent%20to%20Turing%20machines%20both%20in%20terms%20of%20computability%20and%20complexity.). Such connection preserves the notion of [polynomiality](https://en.wikipedia.org/wiki/P_(complexity)) by looking at the length of the function that solves the ODE. This means that the notion of polynomiality of a problem can be linked directly to properties of ODE independently of any machine or whatever.

> **Comments:**
> **username_7**: Are you sure you are pointing at the right article? From the abstract of the article you point at, the authors prove "an implicit characterization of polynomial time computation in terms of ordinary differential equations", which seem to imply a definition of P rather than NP?  

---

