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 Logic 16 (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
A complexity trichotomy for approximately counting list H-colorings
Galanis A., Goldberg L., Jerrum M.  ACM Transactions on Computation Theory 9(2): 1-22, 2017. Type: Article
Jan 11 2018
Controlling loosely cooperating processes
Muscholl A., Schewe S.  Theoretical Computer Science 611(C): 136-141, 2016. Type: Article
Apr 27 2016
Networks of networks: the last frontier of complexity
D’Agostino G., Scala A.,  Springer Publishing Company, Incorporated, Cham, Switzerland, 2014. 355 pp. Type: Book (978-3-319035-17-8), Reviews: (2 of 2)
Mar 11 2015

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright © 2000-2020 ThinkLoud, Inc.
Terms of Use
| Privacy Policy