22
$\begingroup$

It is not uncommon to see students starting their PhDs with only a limited background in mathematics and the formal aspects of computer science. Obviously it will be very difficult for such students to become theoretical computer scientists, but it would be good if they could become savvy with using formal methods and reading papers that contain formal methods.

What is a good short term path that starting PhD students could follow to gain the expose required to get them reading papers involving formal methods and eventually writing papers that use such formal methods?

In terms of context, I'm thinking more in terms of Theory B and formal verification as the kinds of things that they should learn, but also classical TCS topics such as automata theory.

Improve this question
$\endgroup$
5
  • 10
    $\begingroup$ “Young man, in mathematics you don't understand things. You just get used to them.” – John von Neumann Unfortunately getting used to it takes years, at least in my case :) $\endgroup$
    – uli
    Mar 14, 2012 at 17:00
  • 2
    $\begingroup$ I wonder why some people (not necessarily you, Dave) think that a comprehensive Bachelor/Master education in CS (about five years) can be replaced by a couple of course credits. $\endgroup$
    – Raphael ♦
    Mar 14, 2012 at 21:29
  • $\begingroup$ By "Theory B", are you referring to the "B Method"? en.wikipedia.org/wiki/B-Method $\endgroup$
    – Steven Shaw
    Sep 20, 2016 at 10:30
  • $\begingroup$ @StevenShaw: No. Theory B covers semantics and so forth, in contrast to automata/complexity. $\endgroup$
    – Dave Clarke
    Sep 21, 2016 at 8:27
  • $\begingroup$ I hadn't heard of "Theory B" before. I was able to find this helpful answer over on cstheory cstheory.stackexchange.com/a/1523/9552 $\endgroup$
    – Steven Shaw
    Sep 21, 2016 at 9:50

3 Answers 3

Reset to default
15
$\begingroup$

In the preface of his book “Mathematical Discovery, On Understanding, Learning, and Teaching Problems Solving” George Pólya writes:

Solving problems is a practical art, like swimming, or skiing, or playing the piano: you can learn it only be imitation and practice. This book cannot offer you a magic key that opens all the doors and solves all the problems, but it offers you good examples for imitation and many opportunities for practice: if you wish to learn swimming you have to go into the water, and if you wish to become a problem solver you have to solve problems.

I think there is no short path, especially for reaching the state of writing papers. It requires practice, a lot of it.

Some pointers:

If “limited background in mathematics and the formal aspects” means “has never conceived a proof and written it down” then something like this might be a start.

If something on the Theoretical Computer Science Cheat Sheet makes the student feel uneasy, then a refresher course of the according branch of mathematics would be advisable.

There are many sources for mathematical writing: The lecture notes of the 1978 Stanford University CS209 course perhaps. Or this article by Paul Halmos.

Improve this answer
$\endgroup$
2
  • 3
    $\begingroup$ I'm not asking for a shortcut; rather a path (which is short). $\endgroup$
    – Dave Clarke
    Mar 14, 2012 at 17:17
  • 1
    $\begingroup$ @J.D. The OP’s question says “a limited background in mathematics and the formal aspects of computer science” and “become savvy with using formal methods and reading papers”. If a student has only limited exposure to the formalisms used in maths and tcs it’s no good to work on a theoretical topic. He has to work on the basics first before doing the next step. I was just pointing at start of the path. $\endgroup$
    – uli
    Mar 15, 2012 at 8:47
10
$\begingroup$

Formal methods such as Z, B, TLA, CafeObj heavily rely on set theory, logic, category theory, lambda calculus, and automata for modelling the concepts of types, data, and computation.

You can either jump into a comprehensive monograph such as Logics of Specification Languages, by Dines Bjørner and Martin C. Henson eds., Monographs in Theoretical Computer Science, Springer Verlag, 2008 and learn as you need from, and use references cited there. Or learn one topic a a time:

  1. Set theory
  2. Mathematical logic
  3. Temporal logic
  4. Universal algebra
  5. Lambda calculus
  6. Category theory
Improve this answer
$\endgroup$
1
  • $\begingroup$ Good suggestion, though I worry whether whether that monograph is a little to dense to start with. It's certainly heavy. $\endgroup$
    – Dave Clarke
    Mar 14, 2012 at 19:00
6
$\begingroup$

I really think "formal" methods are not a very good idea for educational purposes. For that matter, programming a computer is a "formal" method. Does it succeed as an educational tool?

What is needed is understanding, intuition, and the ability to deal with abstraction. Formal methods hinder all that. Rather, they promote trial and error, hacking, pattern matching, imitation, focusing on syntax. The list goes on and on.

Any piece of rigorous mathematics will teach people how to reason correctly. The simpler the domain, the better it is. All I learnt about reasoning I learnt in high school when I did Euclidean Geometry seriously. Calculus and linear algebra in the University did the rest.

Another attractive alternative is philosophical logic, where they teach people how to think about statements and understand what is the information content and what is a consequence of what. They do that without drowning the students in symbols.

If you take stock of all the top Computer Scientists, you would be amazed how many of them have formal training in philosophy. We are losing all that now because philosophy students now think of Computer Science as a mundane subject. Getting our students to learn some philosophy could counter that to some extent. Get them to work through Bertrand Russell's History of Western Philosophy. That will do wonders.

If they work in programming language theory, you can also have them read Quine, whom I regard as the "god father" of denotational semantics. (Quine was essentially doing denotational semantics of natural language in Word and Object, which was a huge source of inspiration for Christopher Strachey. But this book is quite hard going.) The edited collection Quintessence is a nice source of Quine's ideas for a beginner.

[Note added: One advantage of philosophy over mathematics is that the students get to see debate, i.e., they get to see the "right" argument and the "wrong" argument and see the experts demolish the wrong ones. In mathematics, one never gets to see a wrong argument, which limits its educational value.]

Improve this answer
$\endgroup$
1
  • $\begingroup$ I had some clever, tongue-in-cheek response to this involving the Duration Calculus and a pun on Quine's name ... but unfortunately I forget it.... $\endgroup$
    – Dave Clarke
    Apr 25, 2012 at 9:30

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.