This post is devoted to the fourth, and last, interview with the colleagues who were selected for the first edition of the CONCUR
Test-of-Time Award. (See here for the interview with Davide Sangiorgi, here for the interview with Nancy Lynch and Roberto Segala, and here for the interview with Rob van Glabbeek.) In keeping with my previous interviews, I asked
Hans Hüttel (Aalborg University, Denmak) a few questions via email and you can find his answers below.
Hans receives the award for his paper "Bisimulation Equivalence is Decidable for all Context-Free Processes", which he wrote with Søren Christensen and Colin Stirling. Søren moved to industry after finishing his PhD. Colin is now retired.
Hans receives the award for his paper "Bisimulation Equivalence is Decidable for all Context-Free Processes", which he wrote with Søren Christensen and Colin Stirling. Søren moved to industry after finishing his PhD. Colin is now retired.
Luca:
You receive one of the two CONCUR ToT Awards for the period 1990-1993
for the paper
"Bisimulation Equivalence is Decidable for all Context-Free Processes" you
published with Søren
Christensen and Colin Stirling at CONCUR 1992. Could you tell us
briefly what the context for that work was and how it came about?
Hans: I
was working on my PhD which was on the topic of decidability of
behavioural equivalences for process calculi that allow processes to
have infinite state spaces. Baeten, Bergstra and Klop had proved that
strong bisimilarity is in fact decidable for the BPA calculus even
though the class of trace languages for BPA is exactly the class of
context-free languages. The result only held for normed BPA
processes, that is, processes that could always terminate. Colin was
my supervisor in Edinburgh, and he suggested that I try to find a
simpler proof of that result (much can be said about the original
proof, but simple it was not!). This turned out to be really
interesting; I met Didier Caucal from IRISA who had found a nice,
much shorter proof that relied on finite characterizations and I was
able to use his notion of self-bisimilarity to prove that a tableau
system for bisimilarity was sound and complete wrt. bisimilary. Jan
Friso Groote, who was a PhD student at the CWI at the time, and
myself proved that all other known equivalences are undecidable for
normed BPA (and therefore a
fortiori
also for full, unnormed BPA). But one problem that Colin and I were
never able to solve was if the decidability result also held for the
full BPA calculus.
Søren
arrived in Edinburgh in 1990 and we shared a flat there, in St
Leonards Bank just across from Holyrood Park. We hung out with the
same people in the LFCS, many of whom were clever Italians such as
Davide Sangiorgi and clever quasi-Italians such as Marcelo Fiore. It
is no surprise that Søren and I often discussed our work or that he,
given that Colin was also his supervisor, moved on to study
decidability problems as well, the only difference being that Søren
was mostly interested in the BPP calculus that has parallel
composition instead of sequential composition.
When
I left Edinburgh at the end of August of 1991, Colin and I had
managed to make some progress on the decidability problem for
unnormed BPA. We realised that a finite characterization of the
maximal bisimulation á
la
Caucal was the way ahead but the actual characterization escaped us.
When I returned for my viva in December, Søren had found an
important lemma on finite characterizations and everything fell into
place. The decidability result relied on proving that bisimilarity is
semi-decidable using the finite characterization; non-bisimilarity
was already known to be semi-decidable.
Luca:
Both Søren
Christensen and you wrote the award-winning paper as PhD students in
Edinburgh. Could you tell us about the research environment in
Edinburgh at that time, and the influence it had on you then and in
the rest of your career?
Hans: The
LFCS in Edinburgh was a great place to be at the time. Robin Milner
was still around and busy working on the pi-calculus together with
Davide Sangiorgi, who was his student at the time. Watching them at
the blackboard was interesting, even though the rest of us often
could not follow their discussions! Gordon Plotkin was there (and
still is, fortunately). Rod Burstall was still active, and so was
Mike Fourman. Plus many, many others. There was always someone to
talk to, and it was perfectly legitimate to have an interest in basic
research. Unlike the other professors, Colin had no background in
maths – he was originally a philosopher! – and maybe that was why
he was trying to avoid heavy mathematical lingo, trying to be simple
and precise in his writing at the same time. I learned a lot from
him, also in that respect.
After
Søren returned to Denmark, he left academia and got a job in the
private sector. He still lives near Aarhus. Sadly we lost touch with
each other, in all likelihood because our lives turned out so
different. We got back in touch recently, when we were told about the
reward and we look forward to finally meeting each other again. Colin
retired recently, and I really hope to see him again, when I am able
to travel to Scotland again some day.
Luca:
How much of your later work has built on your award-winning paper?
What follow-up results of yours are you most proud of and why?
Hans: I
worked on decidability issues for another few years after that but
there was no-one to talk to in Aalborg, or rather, there was no-one
there that shared my interest in the area at the time. What is more,
the open problems that remained were major challenges. Some were only
solved much later (such as the decidability of bisimilarity for
pushdown automata, a result due to Sénizergues, the proof later
greatly simplified by Colin) or remain open (such as the decidability
of weak bisimilarity for BPA). Eventually I drifted down the slippery
slope and became interested in other, related topics, and focused
somewhat more directly on program properties. The follow-up result
that most directly relates to my paper with Søren and Colin is the
result from 1994 that bisimilarity is also the only equivalence that
is decidable for BPP. This is a result that I am also quite proud of.
It grew out of discussions with Javier Esparza and Yoram Hirshfeld,
when I was back in Edinburgh for a while in 1993. Ironically, there
was a subtle flaw in the proof that Naoki Kobayashi discovered many
years later. Naoki and one of his student found out how to repair the
proof, and the three of us co-authored the journal version that came
out many years later. The reason why Naoki became interested in BPP
was that he was trying to use the calculus as a behavioural type
system for a pi-calculus. As it happened, this was also the route
that I had taken.
Those
of my later results that I am most proud of have to do with this
area: My work on type systems for psi-calculus (CONCUR 2011 and
later) and a session type system for bounded name use in the
pi-calculus (Acta Informatica 2019). The latter paper also has a
CONCUR connection; it grew out of attending a talk by Roland Meyer at
CONCUR 2013 and wondering why they were not trying to characterize
notions of name-boundedness in the pi-calculus by means of a type
system. It turned out that Meyer et al. were not familiar with type
systems at all. It took me an awful long time to work out a
type-based characterization (using session types), as you can
probably tell.
As
you can tell, I have not worked on bisimulation for quite some time.
Not that there is anything wrong with bisimulation, of course, but if
one wants results that are applicable for automated reasoning about
program behaviour, decidability is important. One can then either
choose to go for a less expressive model of computation (which is
what researchers in the model checking community do) or keep the
model of computation and go for sound, but incomplete
characterizations of program properties (which is what researchers
interested in type systems and related static analysis methods do). I
ended up in the latter camp.
Luca:
To your mind, what are the most interesting or unexpected uses in the
literature of the notions and techniques you developed in
"Bisimulation Equivalence is Decidable for all Context-Free
Processes"?
Hans: BPA,
BPP and similar process calculi can be used as the basis of
behavioural type systems, and I am thrilled that my old research
interests and my current research interests are so directly related.
In
2018 I discovered that Vasco Vasconcelos and Peter Thiemann had
devised a session type system for a functional programming language
in which session types were not regular expressions (which is
essentially what they are in the original work by Honda, Kubo and
Vasconcelos) but BPA processes. Vasco and Peter knew that type
equivalence should be decidable but they were not so familiar with
our results from the early 1990s. At POPL 2019 I attended a talk by
Andreia Mordido, one of Vasco’s collaborators, and she mentioned
our paper from CONCUR 1992! Later that day, I ended up talking to
Andreia and Vasco about my work on BPA from all those years ago.
Luca:
The last forty years have seen a huge amount of work on process
algebra and process calculi. However, the emphasis on that field of
research within concurrency theory seems to have diminished over the
last few years, even in Europe. What advice would you give to a young
researcher interested in working on process calculi today?
Hans: That
they should still work on process calculi! There remains a lot of
interesting work to be done. One reason why research topics drift in
and out of focus is simply that researchers lose interest; it is
hardly ever the case that a topic runs out of interesting research
questions. Another reason is rather grim: Basic research is nowhere
near as well-respected as it used to be. If you look at the funding
schemes that we have today, only the very successful few can get
funding for basic research; I am not among them and it does get
frustrating quite often. Most topics these days deal with applied
research. There is nothing wrong with applied research per se; some
of what I do is on that side of things, but there has to be more to
research than that.
Luca:
What are the research topics that currently excite you the most?
Hans: I
have slowly become more and more interested in programming language
theory, and some of my current collaborators have taken a similar
route, beginning in concurrency theory, drifting into the world of
behavioural type systems and finally wanting to apply all of their
skills to actual programming languages. Right now Mario Bravetti,
Adrian Francalanza, António Ravara and myself are involved in
working on a behavioural type system related to the Mungo tool for a
subset of Java. I am fortunately enough to have had three
exceptionally clever and productive MSc students involved as well,
and this has been extremely helpful. Mungo is in many ways the work
of Simon Gay and Ornela Dardha at Glasgow University, and they, too,
began their careers working on process calculi.
Luca:
You have a keen interest in teaching at university level. Is there
anything you think we should do better in conveying the beauty and
usefulness of theoretical computer science in general, and
concurrency theory in particular, to our students today? Do you have
any thoughts you'd like to share with us on how to combine digital
resources and in-person meetings in the teaching of subjects in the
theory of computing?
Hans: Personally
I think there is a tendency to present any academic topic – and
in particular topics in the mathematical sciences, broadly speaking
– in such a way that the definitions and theorems appear as if
they fell from the heavens, fully formed. As any researcher will
know, that is certainly not
how
they came about. In this way, we focus a lot on what Imre Lakatos and
Karl Popper called the context
of justification. A
well-honed presentation of a theory may appear to be beautiful, but
in my opinion the actual beauty is the one that one experiences when
one has finally understood the theory and understands why the
definitions and theorem turned out the way they did – that is, one
must understand the context
of discovery.
I think problem-based learning (which is something that we talk about
a lot at Aalborg University and at Roskilde University) is the key
here, because it puts the focus on student-centered active learning.
I
have lectured a lot over the years but since 2013 I have drifted away
from traditional lectures towards flipped teaching in which I use
pre-recorded podcasts (of my own making) that students can watch
whenever they want; I then use the plenary sessions for activities
that focus on active learning. I by far prefer having a dialogue with
students that focuses on the problems that they encounter to the
monologue style of a lecture. All my teaching activities are now
flipped and I am happy to say that some of my colleagues are now
thinking along similar lines. It is always good to have someone to
talk to.
