Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Computational complexity via finite types
Asperti A. ACM Transactions on Computational Logic16 (3):1-25,2015.Type:Article
Date Reviewed: Sep 1 2015

Undergraduate-level computer science can feel disjointed at times: for example, at that level, one feels that operating systems and programming languages are entirely separate subdisciplines, whose practitioners have apparently never spoken to one another. The same feeling repeats itself with the more advanced topics of complexity and type theory. Unfortunately, graduate-level computer science does little to dispel that, although with sufficient digging in the research literature, one can see some intersection between operating systems and programming languages.

The intersection between type theory and computational complexity is much harder to see, although it is there. This paper shows beautifully how rich it is. It turns out that there is a direct correspondence between polymorphic functions on finite types and basic complexity classes. In fact, much more is true: higher-order primitive recursive functions precisely capture basic complexity classes. This is an absolutely phenomenal result.

Furthermore, the exposition of these results is a joy to read. The author provides a solid introduction to the necessary concepts, deftly balancing rigor and intuition. All of the most important ideas are illustrated with examples, and the crucial details are spelled out fully (and omitted when reasonably obvious and less important). Going beyond merely proving some rather substantial theoretical results, the author then shows that the machinery he develops is also easily applicable, by showing that Savitch’s algorithm can be (naturally) expressed using a so-called rank-3 term, and thus showing that it recognizes only things in PSPACE.

The combined elegance of the results and the exposition is remarkable. The results also strike me as quite important. I have given this paper some of the highest praise I can: I have actively pointed it out to colleagues as a paper worth reading.

Reviewer:  Jacques Carette Review #: CR143736 (1511-0965)
Bookmark and Share
  Editor Recommended
Featured Reviewer
Complexity Measures And Classes (F.1.3 )
Mathematical Logic (F.4.1 )
Studies Of Program Constructs (F.3.3 )
Would you recommend this review?
Other reviews under "Complexity Measures And Classes": Date
Nonuniform proof systems
Kämper J. Theoretical Computer Science 85(2): 305-331, 1991. Type: Article
Feb 1 1993
Reversal complexity
Chen J., Yap C. SIAM Journal on Computing 20(4): 622-638, 1991. Type: Article
Oct 1 1992
Lower bounds for algebraic computation trees with integer inputs
Yao A. (ed) SIAM Journal on Computing 20(4): 655-668, 1991. Type: Article
Jul 1 1992

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy