I am pleased to post Davide Sangiorgi's interview with CONCUR 2022 Test-of-Time Award recipient James Leifer, who will receive the award for the paper
"Deriving Bisimulation Congruences for Reactive Systems" co-authored with the late Robin Milner.
Thanks to James for painting a rich picture of the scientific and social context within which the work on that paper was done and to Davide for conducting the interview. I trust that readers of this blog will enjoy reading it as much as I did.
Davide: How did the work presented in your CONCUR ToT paper come about?
James: I
was introduced to Robin Milner by my undergraduate advisor Bernard
Sufrin around 1994. Thanks to that meeting, I started with Robin at
Cambridge in 1995 as a fresh Ph.D. student. Robin had recently moved
from Edinburgh and had a wonderful research group, including, at various
times, Peter Sewell, Adriana Compagnoni, Benjamin Pierce, and Philippa
Gardner. There were also many colleagues working or visiting Cambridge
interested in process calculi: Davide Sangiorgi, Andy Gordon, Luca
Cardelli, Martín Abadi,... It was an exciting atmosphere! I was
particularly close to Peter Sewell, with whom I discussed the ideas here
extensively and who was generous with his guidance.
There
was a trend in the community at the time of building complex process
calculi (for encryption, Ambients, etc.) where the free syntax would be
quotiented by a structural congruence to "stir the soup" and allow
different parts of a tree to float together; reaction rules (unlabelled
transitions) then would permit those agglomerated bits to react, to
transform into something new.
Robin wanted to
come up with a generalised framework, which he called Action Calculi,
for modelling this style of process calculi. His framework would
describe graph-like "soups" of atoms linked together by arcs
representing binding and sharing; moreover the atoms could contain
subgraphs inside of them for freezing activity (as in prefixing in the pi-calculus), with the possibility of boundary crossing arcs
(similarly to how nu-bound names in pi-calculus can be used in
deeply nested subterms).
Robin had an amazing
talent for drawing beautiful graphs! He would "move" the nodes around
on the chalkboard and reveal how a subgraph was in fact a reactum (the
LHS of an unlabelled transition). In the initial phases of my Ph.D. I
just tried to understand these graphs: they were so natural to draw on
the blackboard! And yet, they were also so uncomfortable to use when
written out in linear tree- and list-like syntax, with so many distinct
concrete representations for the same graph.
Putting
aside the beauty of these graphs, what was the benefit of this
framework? If one could manage to embed a process calculus in
Action Calculi, using the graph structure and fancy binding and nesting
to represent the quotiented syntax, what then? We dreamt about a
proposition along the following lines: if you represent your syntax
(quotiented by your structural congruence) in Action Calculi graphs, and
you represent your reaction rules as Action Calculi graph rewrites,
then we will give you a congruential bisimulation for free!
Compared
to CCS for example, many of the rich new process calculi lacked
labelled transitions systems. In CCS, there was a clean, simple notion
of labelled transitions and, moreover, bisimulation over those labelled
transitions yielded a congruence: for all processes P and Q, and all
process contexts C[-], if P ~ Q, then C[P] ~ C[Q]. This is a
key quality for a bisimulation to possess, since it allows modular
reasoning about pieces of a process, something that's so much harder in a
concurrent world than in a sequential one.
Returning
to Action Calculi, we set out to make good on the dream that everyone
gets a congruential bisimulation for free! Our idea was to find a
general method to derive labelled transitions systems from the
unlabelled transitions and then to prove that bisimulation built from
those labelled transitions would be a congruence.
The
idea was often discussed at that time that there was a duality whereby a
process undergoing a labelled transition could be thought of as the
environment providing a complementary context inducing the process to
react. In the early labelled transition system in pi-calculus for
example, I recall hearing that P undergoing the input labelled
transition xy could be thought of as the environment outputting
payload y on channel x to enable a tau transition with P.
So
I tried to formalise this notion that labelled transitions are
environmental contexts enabling reaction, i.e. defining P ---C[-]---> P' to mean C[P] ------> P' provided that C[-] was somehow "minimal", i.e. contained nothing superfluous beyond
what was necessary to trigger the reaction. We wanted to get a rigorous
definition of that intuitive idea. There was a long and difficult period
(about 12 months) wandering through the weeds trying to define minimal
contexts for Action Calculi graphs (in terms of minimal nodes and
minimal arcs), but it was hugely complex, frustrating, and ugly and we
seemed no closer to the original goal of achieving congruential
bisimulation with these labelled transitions systems.
Eventually
I stepped back from Action Calculi and started to work on a more
theoretical definition of "minimal context" and we took inspiration from
category theory. Robin had always viewed Action Calculi graphs as
categorical arrows between objects (where the objects represented
interfaces for plugging together arcs). At the time, there was much
discussion of category theory in the air (for game theory); I certainly
didn't understand most of it but found it interesting and inspiring.
If
we imagine that processes and process-contexts are just categorical
arrows (where the objects are arities) then context composition is arrow
composition. Now, assuming we have a reaction rule R ------> R',
we can define labelled transitions P ---C[-]---> P' as follows:
there exists a context D such that C[P] = D[R] and P' = D[R'].
The first equality is a commuting diagram and Robin and I thought that
we could formalise minimality by something like a categorical pushout!
But that wasn't quite right as C and D are not the minimum
pair (compared to all other candidates), but a minimal pair:
there may be many incomparable minimal pairs all of which are witnesses
of legitimate labelled transitions. There was again a long period of
frustration eventually resolved when I reinvented "relative pushouts"
(in place of pushouts). They are a simple notion in slice categories but
I didn't know that until later...
Having found
a reasonable definition of "minimal", I worked excitedly on
bisimulation, trying to get a proof of congruence: P ~ Q implies E[P] ~ E[Q]. For weeks, I was considering the labelled transitions
of E[P] ---F[-]---> and all the ways that could arise. The most
interesting case is when a part of P, a part of E, and F all
"conspire" together to generate a reaction. From that I was able to
derive a labelled transition of P by manipulating relative pushouts,
which by hypothesis yielded a labelled transition of Q, and then, via a
sort of "pushout pasting", a labelled transition E[Q] ---F[-]--->. It was a wonderful moment of elation when I pasted
all the diagrams together on Robin's board and we realised that we had
the congruence property for our synthesised labels!
We
looked back again at Action Calculi, using the notion of relative
pushouts to guide us (instead of the arbitrary approach we had
considered before) and we further looked at other kinds of process
calculi syntax to see how relative pushouts could work there...
Returning to the original motivation to make Action Calculi a universal
framework with congruential bisimulation for free, I'm not convinced of
its utility. But it was the challenge that led us to the journey of the
relative pushout work, which I think is beautiful.
Davide: What influence did this work have in the rest of your career? How much of your subsequent work built on it?
James: It
was thanks to this work that I visited INRIA Rocquencourt to discuss
process calculi with Jean-Jacques Lévy and Georges Gonthier. They kindly
invited me to spend a year as postdoc in 2001 after I finished my
thesis with Robin, and I ended up staying in INRIA ever since. I didn't
work on bisimulation again as a research topic, but stayed interested in
concurrency and distribution for a long time, working with Peter Sewell
et al on distributed language design with module migration and
rebinding, and with Cédric Fournet et al on compiler design for
automatically synthesising cryptographic protocols for high level
sessions specifications.
Davide: Could you tell
us about your interactions with Robin Milner? What was it like to work
with him? What lessons did you learn from him?
James: I was tremendously inspired by Robin.
He
would stand at his huge blackboard, his large hands covered in chalk,
his bicycle clips glinting on his trousers, and he would stalk up and
down the blackboard --- thinking and moving. There was something
theatrical and artistic about it: his thinking was done in physical
movement and his drawings were dynamic as the representations of his
ideas evolved across the board.
I loved his
drawings. They would start simple, a circle for a node, a box for a
subgraph, etc. and then develop more and more detail corresponding to
his intuition. (It reminded me of descriptions I had read of Richard
Feynman drawing quantum interactions.)
Sometimes
I recall being frustrated because I couldn't read into his formulas
everything that he wanted to convey (and we would then switch back to
drawings) or I would be worried that there was an inconsistency creeping
in or I just couldn't keep up, so the board sessions could be a roller
coaster ride at times!
Robin worked
tremendously hard and consistently. He would write out and rewrite out
his ideas, regularly circulating hand written documents. He would refine
over and over his diagrams. Behind his achievements there was an
impressive consistency of effort.
He had a lot
of confidence to carry on when the sledding was hard. He had such a
strong intuition of what ought to be possible, that he was able to
sustain years of effort to get there.
He was
generous with praise, with credit, with acknowledgement of others'
ideas. He was generous in sharing his own ideas and seemed delighted
when others would pick them up and carry them forward. I've always
admired his openness and lack of jealousy in sharing ideas.
In
his personal life, he seemed to have real compatibility with Lucy (his
wife), who also kept him grounded. I still laugh when I remember once
working with him at his dining room table and Lucy announcing, "Robin,
enough of the mathematics. It's time to mow the lawn!"
I
visited Oxford for Lucy's funeral and recall Robin putting a brave face
on his future plans; I returned a few weeks later when Robin passed
away himself. I miss him greatly.
Davide: What research topics are you most interested in right now? How do you see your work develop in the future?
James: I've
been interested in a totally different area, namely healthcare, for
many years. I'm fascinated by how patients, and information about them,
flows through the complex human and machine interactions in hospital.
When looking at how these flows work, and how they don't, it's possible
to see where errors arise, where blockages happen, where there are
informational and visual deficits that make the job of doctors and
nurses difficult. I like to think visually in terms of graphs
(incrementally adding detail) and physically moving through the space
where the action happens --- all inspired by Robin!
