Reasoning about recursive processes: 
Expansion is not always fair. 

Stephen Brookes 
Department of Computer Science 
Carnegie Mel lon University 
Pittsburgh, PA 15213, USA 

Abstract 
When reasoning about parallel programs we would like to combine ﬁxed-point laws 
for unrolling recursion with expansion laws for parallel composition. Algebraic 
manipulation using this combination is dangerous, because of the need to stay 
faithful to the assumption that parallel processes are executed fairly. We give an 
example of a ﬁnite-state parallel system in which the combination of ﬁxed-point laws 
with a Milner-style expansion law causes a mismatch with fair parallel composition. 
Similar diﬃculties are well known in the literature, and it is traditional to conclude 
that the problem is caused by the unbounded non-determinism and inherent lack 
of continuity associated with fairness. Rather than laying the blame on fairness, we 
propose a new form of fair expansion for processes. Every ﬁnite-state process has 
a fair expansion, which characterizes its behavior when run for an arbitrary ﬁnite 
number of steps. We show that fair expansion interacts smoothly with recursion 
and with parallel composition. We provide a fair expansion rule for obtaining a 
valid expansion for a parallel system from fair expansions for its components. We 
establish a theorem on the recursive characterization of parallel compositions of 
recursive processes, in what amounts to a fair parallel generalization of Bekic’s 
theorem concerning simultaneous recursive deﬁnitions. We also discuss how to 
incorporate local variables.