Guarded recursion and unique fixed points: A pill of wisdom from a recent ICE-TCS seminar

Last Tuesday, Sergey Goncharov (FAU Erlangen-Nürnberg, Germany) delivered an ICE-TCS seminar entitled Guarded traced categories for recursion and iteration. In his talk, Sergey presented recent results, based on  joint work (in progress) with Lutz Schröder and Paul Blain Levy, on axiomatizing the theory of guarded fixed points with applications to process algebra in monad-based form, where the notion of guardedness originated. 

In the classic theory of process calculi without internal actions, an equation

X = P(X) 

is guarded if each occurrence of the variable X in the expression P(X) occurs within the scope of some prefixing operator. A classic result in the theory of, for instance, Milner's Calculus of Communicating Systems is that guarded equations have unique solutions modulo bisimilarity. For instance, the equation

X = a.X 

denotes the process rec X. a.X that executes action a indefinitely. If one interprets the above equation over the complete lattice of all languages of finite words over some alphabet, then its only solution is the empty language.

I freely admit that I was under the impression that guarded equations always had unique solutions, but I was wrong. There was a point in the talk at which Sergey showed that the above equation has more than one solution over other domains. Consider, for instance, the set of languages of infinite words over the singleton alphabet {a}. There are only two such languages, namely the empty language and {a^ω}, and both are solutions to the above equation. (This is not surprising, since a-prefixing is just the identity function over this family of languages.) The same holds true when we interpret that equation over the set of all languages of finite and infinite words over some alphabet.

This is probably not news to many, but I have learnt a lesson from attending the talk myself: Guardedness does not imply uniqueness of solutions.

To the young researchers of all ages out there: Go to talks and keep an open mind. You will learn a few bits of information that you might need in your future research projects or you might clarify some misconceptions you might have had, like I did last Tuesday.