Earlier today, I demonstrated how to work with coinduction in the theorem provers Isabelle, Coq and Agda, with a very simple example. This reminded me of a discussion I had in Karlsruhe with my then colleague Denis Lohner: If coinduction is the dual of induction, why do the induction principles look so different? I like what we observed there, so I d like to share this. The following is mostly based on my naive understanding of coinduction based on what I observe in the implementation in Isabelle. I am sure that a different, more categorial presentation of datatypes (as initial resp. terminal objects in some category of algebras) makes the duality more obvious, but that does not necessarily help the working Isabelle user who wants to make sense of coninduction.

Inductive lists I will use the usual polymorphic list data type as an example. So on the one hand, we have normal, finite inductive lists:

datatype 'a list = nil   cons (hd : 'a) (tl : "'a list")

with the well-known induction principle that many of my readers know by heart (syntax slightly un-isabellized):

P nil   ( x xs. P xs   P (cons x xs))     xs. P xs

Coinductive lists In contrast, if we define our lists coinductively to get possibly infinite, Haskell-style lists, by writing

codatatype 'a llist = lnil   lcons (hd : 'a)  (tl : "'a llist")

we get the following coinduction principle:

(  xs ys.
    R xs ys'   (xs = lnil) = (ys = lnil)  
               (xs   lnil   ys'   lnil  
	         hd xs = hd ys   R (tl xs) (tl ys)))  
  (  xs ys. R xs ys   xs = ys)

This is less scary that it looks at first. It tell you if you give me a relation R between lists which implies that either both lists are empty or both lists are nonempty, and furthermore if both are non-empty, that they have the same head and tails related by R, then any two lists related by R are actually equal. If you think of the infinte list as a series of states of a computer program, then this is nothing else than a bisimulation. So we have two proof principles, both of which make intuitive sense. But how are they related? They look very different! In one, we have a predicate P, in the other a relation R, to point out just one difference.

Relation induction To see how they are dual to each other, we have to recognize that both these theorems are actually specializations of a more general (co)induction principle. The datatype declaration automatically creates a relator:

rel_list :: ('a   'b   bool)   'a list   'b list   bool

The definition of rel_list R xs ys is that xs and ys have the same shape (i.e. length), and that the corresponding elements are pairwise related by R. You might have defined this relation yourself at some time, and if so, you probably introduced it as an inductive predicate. So it is not surprising that the following induction principle characterizes this relation:

Q nil nil  
( x xs y ys. R x y   Q xs ys   Q (cons x xs) (cons y ys))  
( xs ys   rel_list R xs ys   Q xs ys)

Note how how similar this lemma is in shape to the normal induction for lists above! And indeed, if we choose Q xs ys (P xs xs = ys) and R x y (x = y), then we obtain exactly that. In that sense, the relation induction is a generalization of the normal induction.

Relation coinduction The same observation can be made in the coinductive world. Here, as well, the codatatype declaration introduces a function

rel_llist :: ('a   'b   bool)   'a llist   'b llist   bool

which relates lists of the same shape with related elements only that this one also relates infinite lists, and therefore is a coinductive relation. The corresponding rule for proof by coinduction is not surprising and should remind you of bisimulation, too:

( xs ys.
    R xs ys   (xs = lnil) = (ys = lnil)  
              (xs   lnil   ys   lnil  
	        Q (hd xs) (hd ys)   R (tl xs) (tl ys)))  
(  xs ys   R xs ys   rel_llist Q xs ys)

It is even more obvious that this is a generalization of the standard coinduction principle shown above: Just instantiate Q with equality, which turns rel_llist Q into equality on the lists, and you have the theorem above.

The duality With our induction and coinduction principle generalized to relations, suddenly a duality emerges: If you turn around the implication in the conclusion of one you get the conclusion of the other one. This is an example of cosomething is something with arrows reversed . But what about the premise(s) of the rules? What happens if we turn around the arrow here? Although slighty less immediate, it turns out that they are the same as well. To see that, we start with the premise of the coinduction rule, reverse the implication and then show that to be equivalent to the two premises of the induction rule:

( xs ys.
    R xs ys   (xs = lnil) = (ys = lnil)  
              (xs   lnil   ys   lnil  
	        Q (hd xs) (hd ys)   R (tl xs) (tl ys)))
=   case analysis (the other two cases are vacuously true)  
  ( xs ys.
    xs = lnil   ys = lnil  
    R xs ys   (xs = lnil) = (ys = lnil)  
              (xs   lnil   ys   lnil  
	        Q (hd xs) (hd ys)   R (tl xs) (tl ys)))
  ( xs ys.
    xs   lnil   ys   lnil
    R xs ys   (xs = lnil) = (ys = lnil)  
              (xs   lnil   ys   lnil  
	        Q (hd xs) (hd ys)   R (tl xs) (tl ys)))
=   simplification  
  ( xs ys.  xs = lnil   ys = lnil   R xs ys
  ( x xs y ys.  R (cons x xs) (cons y ys)   (Q x y   R xs ys))
=   more rewriting  
  R nil nil
  ( x xs y ys. Q x y   R xs ys   R (cons x xs) (cons y ys))

Conclusion The coinduction rule is not the direct dual of the induction rule, but both are specializations of more general, relational proof methods, where the duality is clearly present. More generally, this little excursion shows that it is often beneficial to think of types less as sets, and more as relations this way of thinking is surprisingly fruitful, and led to proofs of parametricity and free theorems and other nice things.

The blog Math with Bad Drawings recently featured an article about Ultimate Tic Tac Toe, a variant of Tic Tac Toe where each of the nine fields is a separate game of Tic Tac Toe. To mark a field of the large game as your, you have to win the small game therein. If you chose a field in the small game, this position determines the small field that the other play may play next. See the linked article for a full explanation. As far as I know, the question of who wins this game was open; at least nothing definite was known on Hacker News or on the Board Games StackExchange site. We discussed this a bit in our office, and my coworker Denis Lohner came up with what seems to be a winning strategy. Update: Not surprising, but with these variants of the rule, the winning strategy was already known.
Strategy Assume Denis ( ) plays against me ( ). Like most suggestions for a winning strategy for the first player, Denis (X) starts with the middle:

Now I have to put my in the center field of the center game. No matter where I place it, Denis will send me back ot the middle, until one field of the center game is free. Doing this eight times inevitably puts us in a position like this:

The only way I can influence the game is by chosing which I place last; this determines where Denis goes now. But (and please verify that carefully) it will not matter: The only thing required from that field is that there is a second field that, together with the center, forms a row (or column or diagonal); all fields satisfy that. Assume I placed the top-left last, and Denis has to go there. He will send me to that field:

Now the game of the first field is repeated: Whereever I send him, he will send me back. This works great for all fields but the middle field. The middle field is special: When I send him there, he has the free choice. He will pick the bottom-right game.

• If I send him to the center field before I send him to bottom-right, he will put the in the top-left corner of that field, sending me back. Once I send him to bottom-right then, he will put the in the bottom-right corner of that field.
• If I send him to the center field after I sent him to bottom-right, he will put the in the bottom-right corner of that field.

In any case we will end up in this situation: I won the center game; I likely have a few in the top-left game. To be precise: I have a there if and only if the he has a in the top-left corner of the corresponding game. He also has the diagonal of the lower-right game. For example:

I have to put my mark in the lower-right game now. From now on, whereever I go, he will send me to either to the top-left or bottom-right game. I can do nothing about it (I cannot send him to the diagonal any more, and whereever I send him there is at least one of the top-left or bottom-right fields fee), so he wil easily win all the other games by getting the diagonal. Eventually, he wins the whole game with the bottom row or the right column:

This is not a formal proof yet, but hopefully close enough to convince you, or alternatively allow you to precisely describe how you can prevent losing against Denis strategy.

This is a security release fixing privilege escalation and local file overwrite vulnerabilities in all previous versions. All users of my pam-krb5 module should upgrade as soon as possible. Derek Chan discovered and Steven Luo reported a vulnerability that allowed overwrite and chown of arbitrary files via Solaris su. Subsequent investigation revealed another, more general problem that would allow tricking pam-krb5 into thinking that Kerberos authentication succeeded with a password under the control of the attacker. This release fixes both problems (CVE-2009-0360 and CVE-2009-0361). See the security advisory for all the details. I feel particularly bad about the more general vulnerability since there was a BUGTRAQ discussion about the underlying cause (needing to use krb5_init_secure_context with MIT Kerberos instead of krb5_init_context) back in 2007 around sudo. I should have realized the implications at the time. Debian, Ubuntu, and Gentoo are affected. I prepared fixed patches for Debian stable, testing, and unstable for both libpam-krb5 and libpam-heimdal, and the Debian security advisories should follow mine shortly. This release also has some build system and installation path fixes by Peter Breitenlohner and support for another Heimdal error reporting interface, thanks to Chaskiel Grundman. You can get the latest release from the pam-krb5 distribution page.