11
$\begingroup$

In Advanced Topics in Types and Programming Languages it is mentioned, in the chapter on sub-structural type systems, that a "carefully crafted" affine lambda calculus with a recursion combinator for lists can only type terms which have polynomial running time (it does not present the proof due to complexity). This would be super interesting if we could also solve every problem in P. I could try to find a solution to a P-complete problem using the calculus presented by I'm not sure this would actually prove anything. It doesn't seem to me to mean that it can preform all the reductions necessary to use a solution to a P-complete problem (although it sure does seem likely).

If an affine lambda calculus is not known to be able to solve exactly the problems in P, is there any known calculus that can solve exactly the problems in P?

$\endgroup$
5
  • 1
    $\begingroup$ Excuse my ignorance, but what's an example of a $P$-complete problem, and more importantly, what notion of reduction are you using? $\endgroup$ Aug 3, 2014 at 18:39
  • $\begingroup$ I found some on wikipedia: en.wikipedia.org/wiki/P-complete#P-complete_problems. Of interest is the circuit value problem and horn-SAT. Linear programming is also apparently $P$-complete. These slides describe the circuit value problem preety well cs.cornell.edu/courses/CS6820/2012sp/Handouts/cvp.pdf. It seems that either $L$ reductions or $NC$ are used, $L$ reductions being weaker than $NC$ reductions. I would be satisfied with either; I am not sure what the consequences are of using the $L$ vs $NC$ are exactly. $\endgroup$
    – Jake
    Aug 3, 2014 at 19:03
  • 6
    $\begingroup$ There are linear languages which are complete for P. Interestingly, they are generally complete for problems, but not for algorithms. That is, you can write a poly time program for every problem in P, but not every polytime algorithm is expressible. $\endgroup$ Aug 3, 2014 at 19:28
  • $\begingroup$ Would that statement be roughly equivalent to "they are generally complete for P but not for FP"? Also if you could provide some examples this would be an amazing answer. $\endgroup$
    – Jake
    Aug 3, 2014 at 19:32
  • 3
    $\begingroup$ Neel Krishnaswami, can you provide a reference? This sounds interesting. $\endgroup$ Aug 3, 2014 at 20:53

1 Answer 1

12
$\begingroup$

Edit: my guess in the first paragraph below is wrong! Ugo Dal Lago pointed out to me a later paper by Martin Hofmann (appeared in POPL 2002), of which I was unaware, showing (as a corollary of more general results) that the system from the ATTPL book is in fact complete for $\mathsf P$ (in spite of not being able to compute every function in $\mathsf{FP}$). So, to my surprise, the answer to the main question is yes.


Concerning the system you are referring to (from the ATTPL book), I am pretty sure it cannot decide every language in $\mathsf P$. It certainly cannot compute every function in $\mathsf{FP}$: as mentioned in the notes of that chapter, that system is taken from Martin Hofmann's LICS 1999 paper ("Linear types and non-size-increasing polynomial time computation"), in which it is shown that the representable functions are polytime and non-size-increasing, which excludes lots of polytime functions. It also seems to give a serious limitation on the size of the tape of the Turing machines you can simulate in that language. In the paper, Hofmann shows that you can encode linear space computation; my guess is that you will not be able to do much more, i.e., the class corresponding to that system is roughly the problems solvable simultaneously in polytime and linear space.

Concerning your second question, there are several $\lambda$-calculi that can solve exactly the problems in $\mathsf P$. Some of them are mentioned in the notes of the ATTPL chapter you are referring to (Sect. 1.6): Leivant's tiered $\lambda$-calculus (see his POPL 1993 paper, or the paper with Jean-Yves Marion "Lambda Calculus Characterizations of Poly-Time", Fundamenta Informaticae 19(1/2):167-184, 1993), which is related to Bellantoni and Cook's characterization of $\mathsf{FP}$; and the $\lambda$-calculi derived from Girard's light linear logic (Information and Computation, 143:175–204, 1998) or from Lafont's soft linear logic (Theoretical Computer Science 318(1-2):163-180, 2004). Type systems arising from these latter two logical systems and ensuring polytime termination (while still enjoying completeness) may be found in:

Patrick Baillot, Kazushige Terui. Light types for polynomial time computation in lambda calculus. Information and Computation 207(1):41-62, 2009.

Marco Gaboardi, Simona Ronchi Della Rocca. From light logics to type assignments: a case study. Logic Journal of the IGPL 17(5):499-530, 2009.

You'll find lots of other references in those two papers.

To conclude, let me expand on Neel Krishnaswami's remark. The situation is a bit subtle. All of the above $\lambda$-calculi may be seen as restrictions of more general calculi, in which you can compute much more than just the polytime functions, say for example system F. In other words, you define a property $\Phi$ of system F programs $P:\texttt{string}\rightarrow\texttt{bool}$ such that:

soundness: $\Phi(P)$ implies that the language decided by $P$ is in $\mathsf P$;

completeness: for every $L\in\mathsf P$, there is a system F program $P$ deciding $L$ such that $\Phi(P)$.

The interest is that the property expressed by $\Phi$ is purely syntactic and, in particular, decidable. Therefore, completeness can only hold in an extensional sense: if $L$ is your favorite language in $\mathsf P$ and if $P$ is your favorite algorithm for deciding $L$ expressed in system F, it may be that $\Phi(P)$ does not hold. All you know is that there is some other system F program $P'$ deciding $L$ and such that $\Phi(P')$ holds. Unfortunately, it may happen that $P'$ is much more contrived than your $P$. Indeed, completeness is proved by encoding polynomially-clocked Turing machines as system F terms satisfying $\Phi$. Therefore, the only guaranteed way of solving $L$ using your favorite algorithm is implementing that algorithm on a Turing machine and then translating it in system F using the encoding given in the completeness proof (your own encoding may not work!). Not exactly the most elegant solution in terms of programming... Of course, in many cases the "natural" program $P$ does satisfy $\Phi$. However, in many other cases it does not: in the LICS 1999 paper mentioned above, Hofmann gives insertion sort as an example.

Intentionally complete type systems, which are able to type exactly the polytime programs of the wider language (system F in my example above) do exist. Of course, they are undecidable in general. See

Ugo Dal Lago, Marco Gaboardi. Linear Dependent Types and Relative Completeness. Logical Methods in Computer Science 8(4), 2011.

$\endgroup$
4
  • 1
    $\begingroup$ I don’t understand what you are trying to say in the second half. Based on your description, there is a syntactic tranformation of poly-time clocked Turing machines to F-programs solving the same problem. As far as I can see, this is the best one can hope for when translating from one model of computation to another. $\endgroup$ Aug 4, 2014 at 12:28
  • 3
    $\begingroup$ @EmilJeřábek: I'm trying to say that $\Phi$ is quite restrictive and that it rejects many "natural" polytime F-programs. If there were such a thing as a system F programmer and you were one, and if I asked you to write down a program for multiplying unary integers (of type $Nat:=\forall X.(X\rightarrow X)\rightarrow X\rightarrow X$), you'd probably write $\lambda m^{Nat}.\lambda n^{Nat}.\Lambda X.\lambda s^{X\rightarrow X}.mX(nXs)$. Then, you might be disappointed in finding that your term is rejected and, instead, you must program multiplication by iterating addition. (Continued) $\endgroup$ Aug 4, 2014 at 15:43
  • 3
    $\begingroup$ (The above example is real: in all linear-logic derived type systems for polytime, the usual term for multiplication is not typable). You may be even more disappointed if I told you that you cannot program, say, insertion sort as such (which is certainly polytime) but you must write down the Turing machine implementing it and then encode that into system F. And I'd say you'd be right to be disappointed: what programmer in what high-level programming language would be happy with a type checker saying "I can't type-check your nested $\mathtt{for}$ loops, please code this in assembly"? :-) $\endgroup$ Aug 4, 2014 at 15:51
  • $\begingroup$ I think this is ok. I'm mainly interested in function search (finding functions that maximize a certain property) so I don't have to be the programmer, the computer does. Tonight I will have sometime to look though these references. Thanks! $\endgroup$
    – Jake
    Aug 4, 2014 at 16:42

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.