Church Meets Cook and Levin

The Cook-Levin theorem (the statement that SAT is NP-complete) is a central result in structural complexity theory. Is it possible to prove it using the lambda-calculus instead of Turing machines? We address this question via the notion of affine approximation, which offers the possibility of using order-theoretic arguments, in contrast to the machine-level arguments employed in standard proofs. However, due to the size explosion problem in the lambda-calculus (a linear number of reduction steps may generate exponentially big terms), a naive transliteration of the proof of the Cook-Levin theorem fails. We propose to fix this mismatch using the author's recently introduced parsimonious lambda-calculus, reproving the Cook-Levin theorem and several related results in this higher-order framework. We also present an interesting relationship between approximations and intersection types, and discuss potential applications.