NVTI 11

The Netherlands Theory Day took place on Friday. After a brief puzzling moment (the projector showed mirror image of the slides and I had to tweak knobs, one of which turned out to be the joystick for the menu).

Jos Baeten motivated his talk with a few observations: in reactive systems, input is not a string with an endmarker; world is nondeterministic, such as google results from one moment to another; Turing m/c's can't fly an airplane but computers can; etc. Then he embarked on describing a theory for interactivity. He emphasized the lack of distributivity in presence of interaction (a.b + a.c \not= a. (b+c); a is open door and after that have b or c revealed is different from opening the door and having the choice of b vs c), and develop an algebra. The talk went from processes similar to finite automata to pushdown processes with new concepts along the way (new Kleene closure, unbounded branching of automata, nonstandard cfg, use of contra simulation, etc) and eventually to reactive Turing machines with executability playing the role of computability. The audience had questions about quantum versions, analogs of halting problems or Universality, and so on, and technical discussions about nonlinear recursion. Jos ended the talk saying this material was good for teaching 1st year theory course because this can lead to later courses on both computability and to process algebra.

I spoke second on data stream algorithms. I had a new puzzle for this talk and was energized. Mark de Berg asked about classes of problems solvable not only in polylog space like typical streaming, but also in say \sqrt{n} space, etc. Yvette Tuin talked about Dutch govt funding for theory but despite best efforts, the picture is dismal for core theory. Observations: Grants were called "subsidies". There were interesting programs like Games for Healthcare, and things like vici, vidi, veni on slides that I am trying to still figure out. Over lunch, I got tutored on how to say Vermeer and Van Gogh.

Hans Bodlaender spoke after lunch about kernelization: preprocessing the input in polytime with what looks like simple rules to reduce the problem to its polysize kernel in some parameter k. The first example was Vertex Cover, for which O(K^2) kernel exists (one can remove any vertex of degree >= k+1 and include it). The second example was about transforming a string into one in which all symbols occur only in runs, and this too had quadratic sized kernel. Hans then related this to FPT (fixed parameter tractability): a prob is FPT iff there exists a kernel. Questions were about complete/hard problems (ex: W(1) hard), role of choice of parameters (in SAT, you can set k variables or satisfy k clauses), and other problems (set cover is hard, linear algebraic problems?). Hans talk altogether was very interesting and I think "kernelization" is a nice combinatorial way to bring one into the FPT world.

The final talk was by Tobias Nipkow. In introducing him, Femke van Raamsdonk talked about success of his group in checking complex proofs (like proof of Kepler's Conjecture or compiled Java programs). Tobias stated that students find it challenging to prove things formally. (Scott Aaronson who has a gift for phrasing, made a cameo: he was quoted comparing some proofs to LSD trips). So, Tobias started breezily, with setting out the goal of teaching students to do proofs with a proof assistant using the Isabelle system, and the image he invoked was thought of bloody video game (qed or die). Rest of his talk was about his experiment of teaching a class on semantics with HWs using a proof assistant with 15 or so MS students. Fascinating, the kind of observations one can make with such experiments. Questions: are there proof "styles"? does Isabelle find counterexamples? can this be extended to algorithms (challenges: probability, approx, running times?) can one detect plagiarism? etc. Some of the technical discussions were around whether this only applied to constructionist logic or if this was too old fashioned by omitting pointers, etc.

After the talks, the NVTI organization (Jaco van de Pol led) discussed their business --- newsletter, thesis awards --- and I was a fly on the wall. They discussed more technical activities, and Femke brought up the idea of connecting with activities for the Turing year (didn't know about that!) in 2012.

ps: The day ended with the dinner at the traditional place (for 15+ years). It was great to see Han La Poutre whose early work on data structures and dynamic graph problems I know and liked, who now seems to have ambled onto bidding/bargaining/auctions/strategies. Han is a fellow city dweller, and Amsterdam is one of the great art cities of the world.