14
$\begingroup$

Background:

I'm coming to the end of my masters degree in Mathematics and will be starting a PhD in Logic in August. The more logic I study, the more theoretical computer science I am exposed to, e.g. recursion theory, lambda calculus, but the underlying CS is brushed under the rug. My main areas of interest - set theory and category theory - also have applications in computer science, but so far I've only studied them from the point of view of pure mathematics.

Problem:

My lack of any computer science background sometimes makes it difficult to see the motivation or intuition behind what is going on, or how it could be applied. I get by, but I feel like it would be healthier to branch out a little bit... it occurs to me that, for the benefit of my future research, I should learn some computer science.

Most CS books I've looked at haven't been very suitable for my purposes, either being too basic and untechnical, or presupposing the kind of CS background that I don't have. They seem to be aimed at people who are quite computer-savvy but who have little in the way in mathematical background - my situation is the opposite.

Question:

What books or other resources are there which could help a mathematician-turned-logician in their goal of gaining a working knowledge of (theoretical) computer science?

I'm looking for something more wholesome than a few seminar talks and more in-depth than The New Turing Omnibus, but I don't have the time or resources to do another undergraduate degree. (It may be that I'm asking for something that doesn't exist.)

Sorry if the question is too vague or ill-posed. I felt it was more suitable here than on MSE but I'll be happy to migrate it if needs be.

$\endgroup$
  • 2
    $\begingroup$ Theoretical computer science makes a lot more sense if one is a good, or at least reasonable programmer, because in some sense, all (most) of TCS is a formalisation (and simplification) of what working programmers do. We had a thread about related matters $\endgroup$ – Martin Berger May 17 '13 at 16:44
  • 1
    $\begingroup$ this was answered on mathoverflow computer science for mathematicians but maybe there is room for a TCS.se version $\endgroup$ – vzn May 17 '13 at 17:07
  • 2
    $\begingroup$ For computability and basic complexity theory, how about Sipser's Introduction to the Theory of Computation? I am puzzled you have not found mathematically oriented books, because there is plenty of them. For example, Arora and Barak, and Goldreich have recent complexity theory books available online, and I am sure there are plenty of math-y track-b theory books out there. $\endgroup$ – Sasho Nikolov May 17 '13 at 17:46
  • 2
    $\begingroup$ Computer Science is quite big; can you narrow it down? It sounds like you are mainly interested in computability, type theory/programming languages, and perhaps complexity theory; does that sound right? $\endgroup$ – usul May 18 '13 at 12:42
  • $\begingroup$ You might find the Handbook of Logic in Computer Science useful for reference. $\endgroup$ – Radu GRIGore May 21 '13 at 21:44
11
$\begingroup$

You're essentially asking for resources that will let you turn your existing knowledge of logic, recursion theory, and category theory into knowledge about theoretical computer science.I would suggest looking at realizability theory, especially via its connections to topos theory and categorical proof theory.

Here are a handful of suggestions; my advice is to pick one and go into depth. With the exception of Taylor's book (which explains this), my suggestions assume you have been exposed to enough lambda calculus and category theory to have seen categorical interpretations of the simply-typed lambda calculus.

  • Paul Taylor's book Practical Foundations of Mathematics

    IMO, this is probably the single best technical introduction to the relationship between logic, category theory and computation. It assumes almost no pre-requisites, but it gets into quite deep waters very quickly, and is sure to tax (and greatly improve) your mathematical maturity.

  • Wesley Phoa's notes An Introduction to Fibrations, Topos Theory, the Effective Topos, and Modest Sets

    These are some lecture notes that Wesley Phoa wrote up. If you are categorically fluent, then these notes offer a really fast path into understanding some of the most important constructions in realizability and topos theory (namely, the construction of the effective topos).

  • Bart Jacobs' book Categorical Logic and Type Theory

    This is one of the definitive references on the categorical semantics of type theory. It is also very large.

At the same time you are reading one of these books, I would advise downloading and learn how to use the Agda programming language. This language implements the sophisticated type theories described above, and IMO it is incredibly helpful to see how the often quite subtle semantic constructions cash out in type theory.

Andrej Bauer can probably give you even better advice. Perhaps he can be persuaded to post. :)

$\endgroup$
4
$\begingroup$

The two books that come to mind are

Introduction to the Theory of Computation by Sipser

and

Introduction to Algorithms by Cormen et al.

I agree with usul who said that theoretical computer science is a broad area and we could give better references if you were more specific about what you want to learn.

$\endgroup$
  • 1
    $\begingroup$ I wouldn't recommend the verbose Introduction to Algorithms. If one wishes to be introduced with the basic algorithmic techniques, I would recommend one of Algorithms by Dasgupta, Papadimitriou and Vazirani, Algorithm Design by Kleinberg and Tardos, or The Design and Analysis of Algorithms by Kozen. Introduction to the Theory of Computation by Sipser is an obviously great choice. I would also add some book on Computational Complexity (I find the ones by Papdimitriou, Arora and Barak, and Goldreich all excellent). $\endgroup$ – Bruno May 20 '13 at 9:31
  • 1
    $\begingroup$ My personal preference is for Kozen's Theory of Computation (quite mathematical in style, and with a larger coverage of logic and computability) over Sipser (which is much closer in style to an applied computer science book). $\endgroup$ – András Salamon May 20 '13 at 11:44

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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