Theory and Practice

Squaregraphs

2011-11-16T22:52:00.001Z

On Tuesday, Donald Knuth gave a talk about squaregraphs. I'm summarizing here what I learned, and I'm including the open problems that Knuth mentioned.

Squaregraphs are plannar graphs. When you draw a graph in a plane, each of its cycles partition the plane into two regions, one bounded and one unbounded. When the bounded region is empty (that is, no edge and no vertex is drawn in it), the cycle is called a bounded face; when the unbounded region is empty, the cycle is called an unbounded face. By definition, all bounded faces of a squaregraph are 4-cycles. There is one more condition. A vertex is interior if it does not belong to the unbounded face. All interior vertices must have degree $\ge4$. Here is an example, a gear graph.

Knuth told us about many properties that are implied by this definition, usually without proof. I enjoy such talks. First, they give you a hawk's eye view of a subject; second, they make you think about the proofs. Some proofs are easy and some escape you during the talk and even days afterwards, but at least you get an idea of what is easy and what is not. What bothers me is that at no point did I feel the need to invoke the last property, that interior vertices have at least 4 neighbours.

But let's focus on what I did learn, rather than what I did not understand.

While on the bus, before the talk, Rasmus and I looked at the Wikipedia article on squaregraphs, which is very dense, and tried to make sense of it. I think it helped both of us to follow the presentation better. One of the last things Rasmus said was: "Squaregraphs ought to have an inductive definition." And, lo and behold, we found out what that definition is during the talk. Every squaregraph can be built by starting with a 4-cycle and repeatedly adding new faces, subject to the degree constraint: take a simple path of length 1, 2, or 3 that is part of the unbounded face and make a new 4-cycle by adding, respectively, 3, 2, or 1 new edges (drawn in the former unbounded face, that is, towards the outside).

Open problem: Is it possible, using this inductive definition, to construct squaregraphs that look like Mona Lisa when viewed from afar?

By the way, a frog can jump from an edge to an opposite edge across a bounded face, obviously. Here is a picture with all possible frog expeditions on an 8-gear.

Each expedition, depicted above with a curved green line, is a set of edges that cut the graph into two disconnected parts. We give vertices on one side a bit $0$ and vertices on the other side a bit $1$. If we do this for each expedition then each vertex gets as many bits as there are expeditions. To put some order on these bits we name the expeditions $0$, $1$, $\ldots\,$, $n-1$, so each vertex gets an $n$-bit string. In our example, there are 8 green lines so each vertex will get an 8-bit string.

These bitstrings are interesting because the shortest distance between two vertices equals the Hamming distance between the bitstrings of the vertices. We say that we found an isometric embedding of squaregraphs into an $n$-dimensional hypercube. In $n$ dimensions, squaregraphs look squarish.

Another interesting property of squaregraphs is that they are median graphs. A median graph is one in which all three vertices $x$, $y$, and $z$ have a median vertex $\langle xyz\rangle$ that is on some shortest path between $x$ and $y$, on some shortest path between $y$ and $z$, and on some shortest path between $z$ and $x$. An example is the integer grid, with vertices $(m_x,m_y)$ for all integers $m_x$ and $m_y$, and edges between vertices $m$ and $n$ when $|m_x-n_x|+|m_y-n_y|=1$. The $x$-coordinate of $\langle mnp\rangle$ is the median of the array $[m_x,n_x,p_x]$, hence the name (I guess). It turns out that you can also isometrically embed median graphs in $n$-dimensional hypercubes. That is, you can label vertices with bitstrings such that travelling an edge flips exactly one bit.

A subset of the $n$-dimensional hypercube is a median graph exactly when the selected coordinates are the models of a 2-CNF formula. Knuth said that an open problem would be to find a nice condition to impose on 2-CNF formulas such that their models correspond to squaregraphs.

Notice that on squaregraphs we have a notion of a line (the green equivalence classes above) and also of turning left or right. This means that we can define a knight's move on the bounded faces of a squaregraph. How can we generalize various problems that are usually done on chessboards to squaregraphs? For example, can one define something like rook polynomials for squaregraphs?

Finally, is there a 3D generalization of squaregraphs?

For more information, Knuth recommended a paper by Bandelt, Chepoi, and Eppstein, which is also recommended by Wikipedia. It's quite long, though. Knuth also showed us some nice pictures of squaregraphs on Eppstein's blog. Of this blog he said: "It is one of the best blogs in computer science. I do not read it, for otherwise I would not do anything else."

[Thanks to Rasmus for finding several mistakes in a previous version.]

Automata on Infinite Alphabets

2011-11-10T17:26:00.000Z

There are several ways of extending the standard definitions of automata to infinite alphabets. Here I try to explain why the trivial extension (just use the same definitions) is not satisfactory and present a couple of alternatives.

The usual definitions go like this. Given is a finite set $\Sigma$. We say that $\Sigma$ is an alphabet and its elements are letters. Words are strings of letters, languages are sets of words. A finite automaton is a finite digraph whose arcs are labelled by letters, has a distinguished initial vertex, and has some vertices marked as being accepting. Each (finite) automaton determines a language, namely the set of those words obtained by concatenating the labels of a walk from the initial vertex to some accepting vertex. A language that can be described by a finite automaton is said to be regular.

Why restrict $\Sigma$ to be finite? What could possibly cause problems if we allow it to be bigger? Isn't the generalization straightforward?

Yes and no.

Yes, we could simply remove the restriction on $\Sigma$ and keep the same definitions. However, that would lead to situations that intuitively just don't feel right. For example, is the language $L=\{\,abc \mid c\in\{a,b\}\,\}$ regular? With the definitions above $L$ is regular exactly when $\Sigma$ is finite. There is something unpleasant about a language suddenly becoming non-regular, although its (declarative) definition does not change.

Recall the standard model for (finite) automata: a transition function $\delta:X\times\Sigma\to X$, where $X=V$ is the (finite) set of vertices, an accepting function $\alpha:V\to2$, and the initial function $\iota:1\to X$. There are at least three ways of extending the standard model: finite-memory automata aka register automata (Francez and Kaminski, 1994), pebble automata, and data automata. All three are surveyed by Segoufin (2006). Thinking back of the language $L$, the intuitive reason why it cannot be recognized by a finite automaton is that we cannot easily remember the letters we saw. So the natural thing to try is to add a (finite) memory to the automaton. This suggests distinguishing between the (not necessarily finite) set of states $X$ and the finite set of vertices $V$. For example, we could take $X=V\times\Sigma^k$ for some $k$. The automaton has $k$ registers. However, now the automaton is too powerful. For example, take $V$ to be the singleton set $1$, and $\Sigma$ to be the set of natural numbers $\mathbb{N}$, and $k$ to be $1$. Then $\delta$ could be essentially any function $\mathbb{N}\times\mathbb{N}\to\mathbb{N}$. We did not even require it to be computable! The class of languages recognized by such a device is clearly too big to be called "regular". This is why extra restrictions on $\delta$ are needed. Francez and Kaminski (1994) essentially required that all that $\delta$ can do with letters is (1) store them in registers and (2) compare them for equality.

Finally, Bojanczyk et al (2011) give what I think is a very cute extension of the standard model of (finite) automata.

Their model is still a triple $(\delta, \alpha, \iota)$ of functions with the types as given above. However, the extra restrictions are much more principled. Now $X$ and $\Sigma$ are required to be $G$-Sets (for some group $G$), and all the three functions are required to be invariant. (These concepts are explained in my previous post on group actions.) A language is now $G$-regular when it is recognized by an automaton for which both $X$ and $\Sigma$ have a finite number of orbits.

Group Actions

2011-11-07T19:29:00.000Z

The theory of finite automata works with finite alphabets. The article Automata with Group Actions by Bojanczyk et al. is one recent attempt to extend the theory to infinite alphabets. To do so, the authors use a basic notion from group theory, namely group action. Here I review the facts about group actions that are necessary to understand Bojanczyk's article.

Recall that a group is a set $G$ together with a binary operation that has an identity, is associative, and each element has an inverse:

$1 \pi=\pi 1$, for all $\pi \in G$
$(\pi\sigma)\tau=\pi(\sigma\tau)$, for all $\pi,\sigma,\tau\in G$, and
there exist a $\pi^{-1}\in G$ such that $\pi\pi^{-1}=\pi^{-1}\pi=1$, for all $\pi\in G$

The typical example of a group is the set of permutations of some set $X$. Its elements have the type $X \to X$. The identity is the identity function. The binary operation is function composition, which is always associative. Each permutation has an inverse almost by definition. (Permutations are those functions that have inverses.) This group is sometimes denoted $\mathrm{Sym}(X)$ and is called the symmetric group of $X$.

Recall also that a function $f : G \to H$ is called a homomorphism when $f(\pi\sigma)=f(\pi)f(\sigma)$ for all $\pi,\sigma \in G$. We say that $f$ preserves the group operation. In particular, $f(1)=1$ or, more precisely, $f(1_G)=1_H$. In words, homomorphisms map the identity of one group to the identity of the other. This is easy to prove, and makes a nice exercise.

A group action is a homomorphism from $G$ to $\mathrm{Sym}(X)$. The set $X$ is called a $G$-Set.

The simplest group action is the trivial action, which maps all elements of $G$ to the identity permutation of $X$,

I know of two reasons why group actions are an interesting concept. First, they let you think of elements of a group $G$ as symmetries of a set $X$ and therefore they partition the set $X$ into equivalence classes. You change the group $G$, you change which elements of $X$ are "essentially the same." Second, once you have group actions for $X$ and $Y$ you also have group actions for $X \times Y$ and $X+Y$ and $X^*$. So group actions build up nicely.

The picture I have in my mind when I talk about G-Sets is a bunch of points (the elements of $X$) with a bunch of arcs between them. Each arc is labelled by an element of $G$. When we look at all arcs labelled by $\pi$ (where $\pi \in G$) we get the picture of a permutation on $X$. That is, a bunch of (disjoint) cycles. When we look at the arcs labelled by $1_G$ we see a loop on each point. In general, we see $|G|$ arcs getting out of each point. This picture has a few more properties. If there is an arc from $x$ to $y$ and one from $y$ to $z$, then there is an arc from $x$ to $z$. In other words, the digraph I'm describing is transitively closed. Proving this property makes another nice exercise. In yet other words, for all $x$ and $y$ either there is an arc from $x$ to $y$ or there is no path from $x$ to $y$. The (strongly) connected components of this graph are the equivalence classes that $G$ determines on $X$. The equivalence class of an element $x \in X$ is called its orbit. Another property of this graph (the Burnside lemma) is that the points in each orbit have exactly $|G|$ loops in total. (Well, I admit: This is not quite the standard formulation.)

To discuss how group actions build up it's useful to finally introduce some (common) notation. We write $x \cdot \pi = y$ when the permutation associated with $\pi \in G$ maps $x \in X$ to $y \in Y$. So, in a way, the dot $\cdot$ represents the (still nameless) group action. Typically, we use the following.

$(x,y) \cdot \pi = (x \cdot \pi, y \cdot \pi)$
$[x_0,\ldots,x_{n-1}]\cdot \pi = [x_0\cdot\pi,\ldots,x_{n-1}\cdot\pi]$

A subset $Z$ of $X$ is said to be invariant (or equivariant) when it is a union of orbits. Equivalently, $Z$ is said to be invariant when each $\pi \in G$ permutes its elements, that is $Z \cdot \pi = Z$. (The graph picture is very handy to figure out why these two definitions are equivalent.)

Now suppose that the $G$-Set is $X \times Y$ and we are given a function $f : X \to Y$. We say that $f$ is invariant when the subset $\{\,(x,f(x))\mid x\in X\,\}$ is invariant. In other words, when $$f(x \cdot \pi) = f(x) \cdot \pi$$ for all $x \in X$ and $\pi \in G$. Invariant functions are closed under composition. $G$-Set is the category of $G$-Sets with the arrows being invariant functions.

How is this at all relevant to finite automata over infinite alphabets? Well, very roughly, a finite automaton over infinite alphabets is one that cannot distinguish between symmetric traces. For example, an automaton might say that "given two iterators $\alpha$ and $\beta$ on a collection $\gamma$, it is illegal to use $\alpha$ to modify $\gamma$ and then continue to use $\beta$." The exact values $\alpha$, $\beta$, and $\gamma$ are irrelevant, so if a trace with some values is accepted, then so are all traces obtained by pointwise permuting the values in the trace. I realize this is rather unclear, but I plan to talk about it in a future post.

In the meantime, there are two other nice references on group actions that I know of: Wikipedia and a recent post on Gower's blog.

Education, Sport, Entertainment

2011-09-16T11:47:00.001+01:00

The summer Olympic Games are less than a year away. In those Games, athletes compete in numerous events, all physical. I saw the term Olympiad used also for non-physical contests, like the International Olympiad in Informatics. I wondered when did people start to refer to intellectual contests as Olympiads, so I tried Wikipedia and … did not find an answer. Instead, I did find out that 'Olympiad' means 'a period of four years.' Strictly speaking, it is erroneous to say 'Olympiad' for the event itself, especially if the event is annual.

Let's move on from etymology to a more interesting issue: What do these events have in common? Both are contests whose participants demonstrate skill levels that seem super-human. For a normal person, just watching the performances can be inspiring and motivating. I believe that this last similarity is key, because it is what makes the events good.

Let me explain.

If two people say that 'X is good,' they may, nevertheless,disagree. For example, if two people say that Natalie Portman is good, they may mean different things. One may mean she is a good actress but not a particularly good scientist; another may mean she is a good scientist but not a particularly good actress. It is therefore important to say what I mean by good. Briefly, something that benefits humankind.

So, what exactly is good about the Games? It can't be the extra pollution caused by hordes of people flying to London. It can't be the overcrowded tubes, which will make my life miserable. Could it be the entertainment it provides to so many people? It could, if only it were less expensive. I'm sure there are cheaper forms of entertainment, such as watching silly videos on YouTube.

So what is it?

Every performance, such as a movie, a dance, or a football game, makes people feel good while watching. More importantly, some performances have a lasting effect. Some movies haunt you for a long time and make you think about certain aspects of life. Beckham and Hagi inspired a whole generation to play football (in UK and Romania, respectively). That is one healthier generation than it could have been. Yes, the effects of one particular performance on one particular individual are small, but the effects add up.

In my mind, by far the most important contributions to society of the Olympic Games are the following.

promoting exercise and hence a healthier life-style
promoting fair-play

Identifying elites? A means to an end. The skills that awe us are not even the skills most useful to society. Schumacher is a good driver, but do we really think it would be good for society if all drivers would have his skills? The bus driver who takes children to school for 40 years without any accident is less awe inspiring, but his skills definitely benefit the lives of the many children he transports. Yes, there is some correlation between the two skills.

And so it is with intellectual contests.

Putting Formulas in Normal Form

2011-08-18T00:17:00.001+01:00

What would be a beautiful description for conversion to DNF?

The problem of converting a formula to DNF is easy to explain: Given a boolean formula, write it as a disjunction of conjunctions. For example, $(x \lor y) \land z$ may be rewritten, by distributivity, as $(x \land z) \lor (y \land z)$. The mechanism is also easy to describe: Push $\lnot$ down by de Morgan, then pull $\lor$ above $\land$ by distributivity.

How to turn this description into an algorithm?

I know a nice algorithm for the first half. Expressed in OCaml, it goes like this: We want a function with the type f1->f2, where

type f1 = [`Var of string | `Not of f1 | `And of f1 list | `Or of f1 list]
type f2 = [`Pos of string | `Neg of string | `And of f2 list | `Or of f2 list]

The trick is to keep around a parity.

let rec pnd (p : bool) : f1 -> f2 = function
  | `Var x -> if p then `Pos x else `Neg x
  | `Not f -> pnd (not p) f
  | `And fs ->
      let fs = List.map (pnd p) fs in
      if p then `And fs else `Or fs
  | `Or fs ->
      let fs = List.map (pnd p) fs in
      if p then `Or fs else `And fs

This algorithm I use when I do boolean manipulations on paper. So I like it. The code is nice, rather than beautiful, because it has some repetition.

What would be a similarly nice solution for the second half—applying distributivity? Expressed in OCaml, we want a function with the type f2->dnf, where

type dnf = [`Pos of string | `Neg of string] list list

Of course, I'm interested in solutions in any language.

Loops and Side-effects

2011-08-16T15:23:00.001+01:00

TeX has a better looping construct.

I designed a small Java-like language for some experiments. I think it is a good idea to be able to say "this piece of code has no side-effects." (If you saw how I write C/++, you'd probably be surprised by what I just said.) There are various ways of isolating side-effects. My requirements were that (1) it must look much like Java and (2) there should be some way to contain side-effects. So I simply banned side-effects from expressions.

Then I proceeded to translate the following Java code.

while (i.hasNext()) {
  Object o = i.next();
  // bla
}

Method calls, however, possibly have side-effects so I could not use them in expressions. A method call is a statement in my toy language.

while (true) {
  boolean c = i.hasNext();
  if (!c) break;
  Object o = i.next();
  // bla
}

This loop reminded me of \loop ... \if ... \repeat in $\TeX$. The keywords loop and repeat, however, are rather un-Java-like-esque. So I decided to say do {...} while (...) {...}. This way, the normal do-loop and the while-loop are special cases obtained by omitting one of the bodies.

do boolean c = i.hasNext()
while (c) {
  Object o = i.next();
  // bla
}

Note that in Java (and C/++) one has the illusion that loops test their condition at the beginning (while) or at the end (do) but never in the middle. This is not true, because expressions may have side-effects.

If languages would have do-while-loops, then I'd probably break far less often.

I decided to write this post after seeing another post about how to write a similar kind of loop in OCaml.

In Praise of Algebra

2011-06-24T01:19:00.000+01:00

Yesterday was Turing's 99th birthday. By coincidence, we had a treat at Queen Mary — a talk by C.A.R. Hoare. This is a very brief summary of what was said.

Consider an algebra whose variables range over (possibly non-deterministic) programs:

$p;q$ denotes the sequential composition of $p$ and $q$
$p*q$ denotes the parallel composition of $p$ and $q$

and

$p \le q$ means that all possible executions of $p$ are also possible executions of $q$

Several obvious properties follow from our intuition of what programs are, so we choose to make them axioms.

$*$ is commutative: $p*q=q*p$
$*$ and $;$ are associative: $(p\circ q)\circ r = p\circ(q\circ r)$, where $\circ$ stands for $*$ or $;$
$\le$ is a partial order
$*$ and $;$ are monotonic: if $p\le p'$ and $q\le q'$, then $p\circ q\le p'\circ q'$
the exchange law: $(p*q);(r*s) \le (p;r)*(q;s)$
the empty program $\varepsilon$ is an identity for both $*$ and $;$

Now it is possible to define Hoare triples as follows. $$\{p\}\,q\,\{r\} \;\;=\;\; p;q \le r$$ The fun begins: Several axioms of Hoare triples follow from the algebra. For example, the rule of consequence $$p'\le p\quad\text{and}\quad\{p\}\,q\,\{r\}\quad\text{and}\quad r\le r'\qquad\text{imply}\qquad \{p'\}\,q\,\{r'\}$$ is true because $$ \begin{align} &\{p'\}\,q\,\{r'\}\\ =& p';q \le r'\\ \Leftarrow& p';q \le r \land r \le r' \\ \Leftarrow& p' \le p \land p;q \le r \land r \le r' \\ =& p' \le p \land \{p\}\,q\,\{r\} \land r \le r' \end{align} $$

By symmetry, there are other triples one might wish to define. $$\begin{align} &p\le q;r \\ &p;q\ge r \\ &p\ge q;r \end{align}$$ It turns out that two of these lead to laws associated with Plotkin triples (reduction in structural operational semantics) and, respectively, Dijkstra triples (`going backwards'). The other triple is new.

In summary, this algebra acts as a meeting point for various approaches to defining semantics for languages.

To see what are the consequences of the exchange law, how weakening the axioms allows various useful models, and a lot more see: C.A.R. Hoare, A. Hussain, B. Moller, P.W. O'Hearn, R.L. Petersen, Struth, On Locality and the Exchange Law for Concurrent Processes.

Some Random Code Metrics

2011-04-01T11:39:00.005+01:00

How compressible is source code? What is the average size of a file? The answers to these and other useless questions are born from too much caffeine.

The projects:

Ant: A build system used by many Java projects, which is itself written in Java.
CPython: The reference Python implementation, written in C.
Frama-C: Analyzers of C programs, written themselves mostly in OCaml.
FreeBoogie: A project of mine written in Java.
GHC: The most used Haskell compiler, written in Haskell.
jEdit: A nice source code editor, written in Java.
Linux: An operating system macro-kernel, written in C.
OCaml: Compiler, standard library, and related tools for the language OCaml, written in OCaml.
SGB: A library for handling graphs and a few example algorithms written by Knuth in CWEB.

Methodology. Get the repo, spend $\le 1$ min choosing a subset of files that look like "the source", run a few quick commands in the shell, don't check the results. That's so you know how much you can trust what follows. Nevertheless, it's likely I got the orders of magnitude right.

Project size contest. The most common measure for a project's size is the number of lines of code. This comes with plenty of caveats. In any case, if we define "lines of code" to be "number of '\n' characters in the files that Radu happened to choose as the 'source'" then here are the results:

Linux: 9.1 million
GHC: 460 thousand
CPython: 450 thousand
OCaml: 260 thousand
Ant: 200 thousand
jEdit: 160 thousand
Frama-C: 126 thousand
SGB: 19 thousand
FreeBoogie: 8 thousand

There's an alternative measure that I like much better and that is not used much: the compressed size of the source code. Why do I like it? Because it should make a good proxy for the information content in the source code. For example, it doesn't matter much if coders use space indentation or tab indentation, long lines or short line, etc. There are plenty of caveats here too. For example, it is likely that the true information content (say, Kolmogorov complexity) is much lower, and that would be apparent if compressers would exploit the structure of the language in which the code is written.

Anyway, here is the bzip2 size of the projects.

Linux: 45 MB
GHC: 4.3 MB
CPython: 2.0 MB
OCaml: 1.2 MB
Ant: 930 kB
Frama-C: 735 kB
jEdit: 690 kB
SGB: 190 kB
FreeBoogie: 50 kB

File size contest. All these projects are broken up into files, which roughly correspond to modules or abstraction boundaries. The idea is that you should be able to focus on the internals of one file at a time without needing to know too much about the other files. And that is true of the compiler too, not only of you. Or, at least, that's one way to look at it.

So, lines per file contest:

CPython: 860
Linux: 680
SGB: 580
OCaml: 330
jEdit: 330
Frama-C. 300
GHC: 280
Ant: 260
FreeBoogie: 140

And compressed bytes per file contest:

SGB: 5900 B
CPython: 3700 B
Linux: 3300 B
GHC: 2600 B
Frama-C: 1700 B
OCaml: 1500 B
jEdit: 1400 B
Ant: 1200 B
FreeBoogie: 780 B

Information density. So, which project should I read if I want to get most per byte? And which one can be read on the bus without missing much? Well, here's information per character (where information is "measured" as earlier: compressed size, so these are basically inverses of compression ratios).

SGB: 0.25
GHC: 0.21
FreeBoogie: 0.19
Linux: 0.18
Frama-C: 0.16
jEdit: 0.16
CPython: 0.15
OCaml: 0.14
Ant: 0.14

Looks like GHC is almost as incompressible as the code Knuth writes.

People and Conferences ≥2000

2011-02-18T16:05:00.001Z

A Small jStar Demo

2010-12-13T16:51:00.000Z

Old and New

2010-12-07T01:43:00.000Z

This is an unusual post—imprecise, written late in the night, with no apparent purpose, and no apparent question. As I said, it is unusual. Not for the web, but for this blog.

All else being equal, and sometimes even when all things are not equal, some prefer old over new and others prefer new over old. Suppose you may choose between reusing a piece of code and writing it yourself. Suppose further that you have no objective reason to believe one option is better than the other. It is not clear that reusing old code will ensure you will have fewer bugs to fix in the future, since, obviously, you are an awesome programmer. (After all, you are reading this blog and recommending it to others. Nah. Forget that. I'm drunk. Really.) Back to the subject: You are awesome. I'd like to meet you. No. That was not the subject. Oh, right! So it's not clear that the old code you may reuse has very few bugs. There is also no obvious reason why you should be able to write more efficient code. That may be the case if your problem is a specialization of a general problem solved by the existing code. But that is not the case. Your problem is just as general as the existing library was designed to handle. But, wait! The library is there. Surely it must be quicker to just use it? No, it is not clear. Apparently you must coerce your build system through some hoops in order to accommodate the existing code. And you do need to write a "little" glue code. Just how little is "little" is hard to say. In short, as I said, you really have no idea of what would be better: to reuse or to write from scratch?

Yet, in spite of all I wrote above, I bet you know what is the right thing to do. You feel like telling me, like it is obvious. However, I am willing to bet that all your arguments have a counterfactual or philosophical flavor. Depending on who you are, you may feel like telling me that reusing code is the right thing to do, because it surely cannot be right for humans to keep reinventing wheels. We need to focus on the new stuff, right? "No. No. No." yells the other reader. It is much better to write the code yourself. In the long run, your purpose is to become a better programmer, and not writing the code yourself means giving up a great learning experience.

The point is that most people either prefer the old, or prefer the new—very few are indifferent. I happen to be in the former camp, but this is beside the point. I wonder if psychologists know what I am talking about.

More OCaml Pretty-Printing

2010-12-03T16:10:00.000Z

How to print expressions with binary operators using as few parentheses as possible. In this post, we avoid parentheses that are rendered unnecessary by precedence rules.

Consider the following type.

type op = Plus | Times
type expr = Op of op * expr list | I of int

And here is a value:

let v = Op (Plus, [I 3; Op (Times, [I 5; I 7; Op (Plus, [I 4; I 2])]); I 2])

If we don't care about how many parentheses are printed, we'd write

open Format

let op2s = function Plus -> '+' | Times -> '*'

let rec pp_list sep pp ppf = function
  | [] -> ()
  | [x] -> fprintf ppf "%a" pp x
  | x::xs -> fprintf ppf "%a%c%a" pp x sep (pp_list sep pp) xs

let rec pp ppf = function
  | Op (o, es) -> fprintf ppf "@[(%a)@]@," (pp_list (op2s o) pp) es
  | I x -> fprintf ppf "%d@," x

let _ = pp std_formatter v

The rule for precedence is simple: It's safe to strip parentheses in $(A \circ B) \bullet C$ if and only if $\circ$ has higher precedence than $\bullet$. It would be nice to isolate the code that decides whether parentheses are needed. We begin by removing grouping concerns from pp.

let pp r ppf = function
  | Op (o, es) -> pp_list (op2s o) r ppf es
  | I x -> fprintf ppf "%d" x

We can recover parentheses everywhere with a simple Y-like combinator.

let rec y1 f ppf x = fprintf ppf "@[(%a)@]@," (f (y1 f)) x
let pp1 = y1 pp
let _ = pp1 std_formatter v

Now pp1 does (almost) the same as the initial pp, the big difference being that we isolated the code that handles grouping. Because of this, implementing a policy based on operator precedences is simply a matter of defining another combinator.

let precedence = function 
  | Op (Plus, _::_::_) -> 1
  | Op (Times, _::_::_) -> 2
  | _ -> 0

let rec y2 up f ppf x =
  let down = precedence x in
  let lp, rp = 
    if down <= up && up <> 0 && down <> 0 then ("(", ")") else ("","") in
  fprintf ppf "@[%s%a%s@]@," lp (f (y2 down f)) x rp

let pp2 = y2 0 pp

let _ = pp2 std_formatter v

Mini Me

2010-09-29T15:39:00.000+01:00

Expected Size of a Set

2010-09-29T15:10:00.003+01:00

You insert $a_1$, $a_2$, $\ldots$, $a_n$ into an initially empty set data structure $S$. What is the size $s$ of $S$ at the end?

Say that each $a_k$ is taken from $1.\,.\>m$ and all $m^n$ sequences are equally likely. If $n=0$ then $s=0$; if $n\to\infty$ then $s\to m$; and a quick and dirty simulator shows that if $n=m$ then $s\approx0.63m$. The number $c(n,k,l)$ of sequences of length $n$ that have exactly $k$ unique elements taken from $1.\,.\>l$ satisfies $$c(n,k,l)=c(n,k,l-1)+\sum_{q>0} {n \choose q} c(n-q,k-1,l-1).$$ This gives a way to compute $s$ exactly for $m=n < 100$, and it seems that indeed $s/n$ approaches $\approx0.63$ from above as $n$ grows.

Do you know a formula for $0.63$? For $s(m=n)$? For $s(m,n)$? (I don't.)

A Certain Type of Pretty-Printing in OCAML

2010-09-15T17:41:00.003+01:00

You want to print Node(Leaf, [{ra=1;rb="a"};{ra=2;rb="b"}], Node(Leaf, [{ra=3;rb=["foo";"bar"]}], Leaf)) as "1 * a * 2 * b * 3 * foo * bar". How do you do it?

Let us begin with the simpler problem of printing a star-separated list of integers.

open Format
let simple_print = function ->
  | [] -> ()
  | [x] -> printf "%d" x
  | x :: xs -> printf "%d@ * "; simple_print xs

Since there is one less star than there are integers, the last integer in the list is treated in a special way. Of course, we may want to also print lists of strings in this way; or we may want to use some other separator than a star; or we may want to use a different formatter.

let better_print separator pp ppf = function ->
  | [] -> ()
  | [x] -> fprintf ppf "%a" pp x
  | x::xs -> 
      fprintf ppf "%a@ %s " pp x separator; 
      better_print separator pp ppf xs
let pp_string ppf x = fprintf ppf "%s" x
let pp_int ppf x = fprintf ppf "%d" x
better_print "||" pp_string std_formatter ["foo"; "bar"]

Now comes the interesting part. Suppose that what we really want to print are the primitive values that hang in a complicated tree of nested data structures like lists, variants, records, sets, and so on. For example, the value mentioned in the summary has type t.

type r = { ra : int; rb : string list }
type t = Leaf | Node of t * r list * t
let v =
  Node
    (Leaf,
    [{ra=1;rb=["a"]};{ra=2;rb=["b"]}],
    Node
      (Leaf,
      [{ra=3;rb=["foo";"bar"]}],
      Leaf))

We'll probably have a pretty-printing function pp_r for type r and a pretty-printing function pp_t for type t. Let's think about the latter. For Node(left,data,right) we'd be tempted to say "print left, print star, print data, print star, print right." Of course, left might be a leaf, in which case we should omit the first "print star." Or perhaps, the list data is empty, in which case we should omit one of the two "print star"s. In a more complicated scenario data might be a list of sets and, although the list is not empty, all of its sets may be. In order to figure whether this is the case we'd need to traverse the whole list. Or perhaps we have a record with $n$ fields. After printing the first $k$ fields we should print a star when one of the first $k$ fields is nonempty and one of the last $n-k$ fields is nonempty. So we'd better start by asking once in the beginning each field if it is empty: Otherwise we may end up asking each field $\sim n$ times and we know that checking emptiness may take linear time. (It would be pretty stupid for pretty-printing of a big structure with few leafs to take quadratic time.) Or perhaps, …

OK. That's a nightmare, so let's try to take a step back. We want:

a way to traverse the data structure,
a way to print each possible leaf, and
a way to know when we get to a leaf whether it is the first (or last).

That's easy! It sounds like what we want is a fold. Well, almost, because when we hit a string leaf we need to call one function and when we hit an integer leaf we need to call another. So it is a specialized fold but, nevertheless, our implementation may look very similar to what we'd do for a fold.

let pp_string' ppf first x = 
  if not first then fprintf ppf "@ * "; pp_string ppf x; false
let pp_int' ppf first x =
  if not first then fprintf ppf "@ * "; pp_int ppf x; false
let pp_r ppf first {ra=ra; rb=rb} =
  let first = pp_int' ppf first ra in
  List.fold_left pp_string' first rb
let pp_t ppf first = function
  | Leaf -> first
  | Node (left, data, right) ->
      let first = pp_t ppf first left in
      let first = List.fold_left (pp_r ppf) first data in
      pp_t ppf first right
let pp_r' ppf = pp_r ppf false
let pp_t' ppf = pp_t ppf false

This works and is already much nicer than the previous option. However, There are still problems.

The functions pp_string' and pp_int' are obtained from their unprimed counterparts in a very systematic way, so we shouldn't write the same code once for each leaf type.
Similarly for pp_r' and pp_t'.
Note that for lists we used List.fold_left so for the type t we should be able to do something similar: Implement a generic fold, and then use it.
The star is hardcoded. What if we want a different separator?

So let's see how can we encode the recipe for obtaining pp_string' and pp_int'. We may be tempted to try the following.

let pp_sep separator pp = 
  fun ppf first x -> if not first then fprintf ppf "@ %s " separator; false

Yay: We also solved the problem with the star being hard-coded! What we can do is to add a (first) parameter pp to pp_r and pp_t. Then we redefine the primed versions.

let pp_r' separator ppf = pp_r (pp_primitive separator) ppf false
let pp_r' separator ppf = pp_r (pp_primitive separator) ppf false

We then replace calls to pp_int' by pp pp_int. Everything's sweet, right? Well, … no, this doesn't typecheck. The reason is in OCAML's FAQ. You may want to try these modifications to convince yourself that they indeed do not work. Anyway, the workaround is in OCAML's FAQ. So here's how to do it.

open Format

(* example data structures *)
type r = { ra : int; rb : string list }
type t = Leaf | Node of t * r list * t

(* a value to test with *)
let v =
  Node
    (Leaf,
    [{ra=1;rb=["a"]};{ra=2;rb=["b"]}],
    Node
      (Leaf,
      [{ra=3;rb=["foo";"bar"]}],
      Leaf))

(* how to print 'leafs' *)
let pp_string ppf x = fprintf ppf "%s" x
let pp_int ppf x = fprintf ppf "%d" x

(* a recipe for making leaf printing foldable *)
type sep_wrapper = { 
  primitive : 'a. (formatter->'a->unit)->formatter->bool->'a->bool
}
let pp_sep separator = {
  primitive = fun pp ppf first x -> 
    if not first then fprintf ppf "@ %s " separator; pp ppf x; false
}

(* folds for our homogeous data structures *)
let rec fold_t f s = function
  | Leaf -> s
  | Node (l, xs, r) -> fold_t f (List.fold_left f (fold_t f s l) xs) r

(* pretty printing workers, used mostly internally *)
let pp_r pp ppf first {ra=ra; rb=rb} =
  let first = pp.primitive pp_int ppf first ra in
  List.fold_left (pp.primitive pp_string ppf) first rb
let pp_t pp ppf = 
  fold_t (pp_r pp ppf)

(* pretty printing for the typical user *)
let pp_whole pp = 
  fun separator ppf x -> ignore (pp (pp_sep separator) ppf true x)
let pp_r' = pp_whole pp_r
let pp_t' = pp_whole pp_t

(* a small test *)
let _ =
  printf "@[%a@." (pp_t' "*") v

Note that the strategy of implementing a general fold and then use it does not work for type r because it holds two kinds of leafs (integers and strings). Also note that what I called leafs (or leaves, whatever) do not need to be OCAML primitive types.

Picasaweb Cameras

2010-07-16T21:43:00.002+01:00

Which photo cameras make cool pictures?

I took a sample of 100 featured pictures from Picasa.

59 Canon
23 Nikon
18 others

Out of the Canon pictures, 27 where taken by EOS 5D Mark II, 8 where taken by various flavors of EOS DIGITAL REBEL, and 24 by other Canons.

Solitaire

2010-07-14T16:08:00.003+01:00

Yet another “Is this NP-complete?” question. The problem is of a kind that I discussed before.

In the game Solitaire you sometimes visualize the state you want to achieve and regard the necessary intermediate moves as chore. A friend wondered how to reach the goal with a minimum number of key presses. (He plays on a Blackberry with no mouse.) Let us look at a simplified example.

	□,1,□,□,4,3,□,2,5									(1)
	↝ □,1,□,□,4,23,□,□,5									(2)
	↝ □,1,□,□,234,□,□,□,5									(3)
	↝ □,□,□,□,1234,□,□,□,5									(4)
	↝ □,□,□,□,□,□,□,□,12345									(5)

In this example there are 9 slots into which cards 1–to–5 are placed. In a valid state, each slot contains a contiguous sequence of cards, possibly empty (□). Each move consists of transporting a contiguous sequence of cards from one slot to another. (Take a moment to convince yourself that a valid state is reached only if the whole sequence of a slot is transported.) The cost of a move is the distance between the source and the target slots (and is independent of the size of the transported sequence). In the example above there are 4 moves with a total cost of 2+1+3+4=10. The goal is to put all the cards in one slot.

This problem has a dynamic programming solution, which works on a different representation of the states.

	2,8,6,5,9									(6)
	↝ 2,6,5,9									(7)
	↝ 2,5,9									(8)
	↝ 5,9									(9)
	↝ 9									(10)

The first state tells us that card 1 is in slot 2, card 2 in slot 8, card 3 in slot 6, and so on; the last state tells us that all cards are in slot 9. In general, a state tells us in which slots there are cards, and does so in increasing order of cards’ values. With this representation a move consists of crossing out a number. The cost of a move is the absolute difference between the crossed out number and the following number. (The last number in a state cannot be crossed out.) With n cards there are 2ⁿ⁻¹ possible states. For each state there are <n possible moves. Therefore, if each possible state and each possible move is examined at most once, then this algorithm works in O(n2ⁿ) steps.

Note that there are (n−1)! sequences of moves that attain the goal. A similar reduction (from n! to around n2ⁿ) appears when one moves from a brute force solution to a dynamic programming solution of the Hamiltonian cycle problem. In general, it is often possible to look at all subsets when it seems that looking at all permutations is necessary.

Questions: Can you do better? Is this problem NP-complete?

Mathematical Logic 1

2010-07-12T14:08:00.000+01:00

Motivation by analogy.

Logic studies reasoning. Many people that are not familiar with logic are able to think (reasonably). For example, many children find the explanation “because I say so” less satisfying than “if you do not solve your homework then you will not receive a high grade, therefore you will receive a high grade only if you solve your homework.” A child may not agree that a high grade is a worthy goal, but the point is that the second explanation is somehow more satisfying. Some hidden mechanisms are at work, mechanisms that are transfered to children by training. Children learn how to reason mostly by imitation. I believe it is a very bad idea to teach a child how to reason by exposing him to logic, for that would be akin teaching a child how to walk by exposing him to the laws of mechanics, or teaching a child how to sing by exposing him to music theory, or teaching a child how to speak by exposing him to the rules of grammar. It is preposterous to try to teach a child how to speak by explaining the rules of grammar, because language is necessary in order to communicate the rules of grammar. Such circularity exists in the case of logic too. One cannot learn logic, unless one already knows how to reason.

Are then mechanics, music theory, grammar, and logic useless? Although mechanics does not help people to walk, it does help them to build cars; although grammar does not help people to speak, it does help them to communicate effectively. Mechanics is useful because cars are useful; grammar is useful because the ability to communicate is useful. Note that people built carts before understanding the laws of mechanics and they probably built engines before understanding the laws of thermodynamics. However, cars are better because we understand the laws of mechanics. Similarly, people may communicate without knowing grammar. However, people communicate better if they follow the rules of grammar.

Logic enriches the way people think. A logician immediately parses the sentence “if you do not solve your homework then you will not receive a high grade, therefore you will receive a high grade only if you solve your homework” as “(if (you do not solve your homework) then (you will not receive a high grade), therefore ((you will receive a high grade) only if (you solve your homework))”. Certain logical connectives (like if…then, not, therefore, only if) are emphasized, because logic cares more about how statements are chained together into an argument, rather than what those statements mean. In fact, when being careful about what they say (or hear), logicians will likely translate on the fly that statement into a symbolic form that makes it easier to visualize the structure: “(¬ p ⇒ ¬ q) ⇒ (q ⇒ p), where p stands for ‘you solve your homework’ and q stands for ‘you will receive a high grade’”. Here, logical connectives are represented by some standard symbols (¬ and ⇒) and the rest is hidden behind letters (p and q).

Are these BDDs the same?

2010-06-03T17:30:00.000+01:00

This is exercise 7.1.4-12 in TAoCP. It is easy, but somehow I liked the solution.

A BDD (binary decision diagram) is a data structure that encodes boolean functions. Each node has a variable and two children, low and high. To make it concrete, let's pick a C-language structure.

struct dd_node {
  int V; // variable, at least 1 and at most N
  int L, H; // indexes in nodes
};
struct dd_node nodes[nodes_size];

A valid BDD representation obeys a few constraints.

nodes[k].L!=nodes[k].H for k≥2
nodes[k].L==nodes[k].H==k for k<2
nodes[nodes[k].X].V>nodes[k].V for k≥2 and X either L or R
nodes[k]==nodes[kk] implies k==kk
For all 2≤k<nodes_size there is a kk such that nodes[kk].L==k || nodes[kk].R==k.

Each such node basically encodes a (!v?l:h) expression. For example, if value[V] is the value of variable V then the represented boolean function is evaluated by eval(value, nodes_size-1).

int eval(int* value, int k) {
  if (k < 2) return k;
  return !value[nodes[k].V]? eval(value, nodes[k].L) : eval(value, nodes[k].H);
}

Here comes the problem. Suppose you are given two BDDs, nodes1 of size s1 and nodes2 of size s2. Design an algorithm to decide if they represent the same boolean function. And, by the way, do not use a stack, not even the call stack.

Thesis and Move to London

2010-04-15T15:09:00.002+01:00

I submitted my thesis and I joined Queen Mary, University of London.

On 26th of March I submitted my PhD thesis. I tried to make it easy to understand without much background knowledge. If you read (parts of) it, then please consider sending me feedback, as I can make corrections for the final version.

Now I work in Queen Mary, University of London in the Theory Group, on the jStar project.

Adding is in Nature’s definition

2010-03-19T11:15:00.000Z

Below is one of the funniest and at the same time saddest course descriptions I ever saw.

As an undergrad, I took a course of Tudor Niculiu. I believe the course was supposed to be on OOP, but the lectures gave us some sort of introduction to philosophy. Luckily, there was no exam—we just had to write a small C++ program. Then we had to print the program (poor trees!) and go to an oral examination where the lecturer wanted to see, apparently, if we have any idea about how the program works.

A colleague once told me that "Niculiu used to be normal, but then he had an accident that affected his brain." If that's true, then it is quite sad. In any case, I have trouble understanding how someone who describes his course as follows is allowed to teach in what is supposed to be one of the best colleges in Romania.

Algorithms and Data Structures:

Adding is in Nature’s definition. However, the inverse operation, subtraction, needs negative numbers. We close mathematically the Nature to an integer that opens the physics for recognizing the limits of the Reason - electrons, in the meanwhile, attracting marvelous engineering solutions for different technologies. Electronics is among the most advanced engineering sciences; therefore, it has to be practiced by the most conscient human beings. Recurrent addition is multiplication, a most important parameter for the Nature. Mathematics closes the integers to the multiplication inverse, defining the rational numbers. These are not more than the naturals, but we can do many useful things with the Reason, from strategy to computer. So "what else do we need?" say too many, forgetting that the limits of the, so-called, pure Reason are caused by the fact that it bounds itself to close the Adaptability to discrete/ sequential operations. Thanks God, neither mathematicians, nor physicists accept all-happiness. They discover in three ways - order, algebra, analysis - which assisted all of them to think together, the power of continuum and that of the patience. In this context, “mathematicians and physicists” means the theorem, natural laws, or even new approach discoverers, and more, the engineers that understand the essential of mathematics and of physics.

To his credit, in the first part there's a glimmer of the (nice!) axiomatic way of defining numbers.

Typesetting Inequalities

2010-03-17T20:10:00.001Z

These are two puzzles I arrived at while working on my PhD thesis. I know the answers but not because I derived them. I think both puzzles are quite hard. Have fun!

Typesetting. As you know from a previous post, ViM doesn’t handle paragraph reformatting very well in L^AT_EX, so I wrote a small tool. Given word lengths l₁, l₂, …, l_n we want to insert line breaks such that (1) no line is longer than l and (2) the shortest line is as long as possible. Here’s the challenge: do it in O(n) time.

Inequality. Show that the following inequality has no solution in non-negative reals (or integers if you prefer).

PS: I know the answers because of 11011110 and, respectively, geomblog.

TeX text files

2010-03-02T17:29:00.002Z

Questions for those who use LaTeX by editing text files (as opposed to those who use a WYSIWYG editor like LyX).

Do you use the line wrapping feature in your editor and keep each paragraph on one line or do you usually put paragraphs on multiple lines? If the latter is true then how do you maintain the lines so they aren't too long or too short? Manually or automatically? If automatically, then do you use a program like par, a feature of your editor, or something else? If you use par, then how do you keep it from messing things like \begin {equation}…\end{equation} and \begin {verbatim}…\end{verbatim}? (The latter is in a paragraph of its own, but the former usually not.)

Graph Clustering and Answer Set Programming

2010-02-10T19:35:00.002Z

A short summary of two articles I read on the bus.

Cut-clustering. Flake, Tarjan, and Tsioutsiouliklis published in 2004 an algorithm for clustering graphs. I always enjoy reading articles co-authored by Tarjan because they are so clear and so light on notation. The algorithm acts on undirected graphs. First, a special node is connected to all other nodes thru edges of cost α, a parameter. Initially all nodes are their own cluster, but clusters will be merged as nodes are processed. To heuristically speed up the runtime, nodes are processed in decreasing order of their "connectivity", which is the sum of costs on adjacent edges. Processing one node consists of finding a minimum cut between it and the special node; for all nodes on the same side of the cut as the node being processed (1) we mark them as touched and (2) we merge their clusters. Touched nodes are not processed further. (It doesn't hurt but it's faster not to process them.) That's it.

The article discusses why this works and what properties the resulting clustering has. In short, by making α bigger you get smaller clusters, but there is no fine control on the number and size of clusters. On the bright side, the "quality" of the clusters is good. Also, by varying α the resulting clustering is hierarchical.

The authors present three case studies: the graph of citations for papers in CiteSeer, websites close to dmoz, and something about websites discussing 9/11. The CiteSeer results are interesting. Here are the top level clusters:

61837 paper on image, learning, problem, linear, algorithm
- 36986 papers on learning, image, neural, recognition, knowledge
- 8179 papers on numerical, equations, linear, matrix, nonlinear
- 3650 papers on wavelets, coding, transform
- 2386 papers on constraint satisfaction
- 2377 papers on bayesian, monte carlo, markov
34353 papers on parallel, memory, distributed, execution, processors
20593 papers on network, service, internet, security, traffic
15415 papers on logic programming, software, language, semantics

It would be interesting to compare experimentally this approach with something like k-means.

Answer set programming. In 2002, Lifschitz wrote a nice introduction to answer set programming. I shall summarize only the basics. A program that finds a big clique in a graph looks like this:

const j = 3.
vertex(0..5).  % there are six vertices and here are the edges...
edge(0,1). edge(1,2). edge(2,0). edge(3,4). edge(4.5). edge(5,3). edge(4,0). edge(2,5).

j {in(X) : vertex(X)}. % we want at least 3 vertices ``in'' the clique
joined(X,Y) :- edge(X,Y).
joined(X,Y) :- edge(Y,X).
:- in(X), in(Y), X!=Y, vertex(X), vertex(Y), not joined(X,Y).
  % if X and Y are not joined, then they can't be two distinct selected vertices

SMODELS runs the above program. Beware, you need to change the sources to compile it with a modern GCC.

The theory behind it goes as follow. There is a set S of literals, which come in pairs, the positive literal l and the negative literal -l. Even if above we used some syntactic sugar, the program is essentially a set of rules of the form:

A, not B, :- C, not D

where A, B, C, and D are sets of literals. The set X is an answer set for such a program when

it is consistent (it does not contain both l and -l) and
it is an answer set for the reduct program

The reduct program is obtained by keeping only the rules for which X⊇B and X∩D=∅ and by removing the not parts of the kept rules. The set X is an answer set for a not-free program when

X is closed under the program and
X is a minimal (with respect to set inclusion)

Finally, a set X is closed under a (not-free) program when for each rule

C⊄X or
A⊆X

A nice exercise would be to find an encoding of SAT in answer set programming. (Lifschitz has a solution.) The converse is the subject of a paper by Fangzhen Lin and Yuting Zhao from 2002 (but published in 2004).

update 1: when α is bigger the clusters are smaller.
update 2: fixed the problem pointed out by Mikolas in the first comment.

Green Tree

2009-12-24T17:59:00.002Z