What is a Free Name in a Process Algebra?

This is the question addressed by a short paper by Flemming Nielson, Hanne Riis Nielson and Henrik Pilegaard that appears in Information Processing Letters 103 (2007), pp. 188-194. In the paper, the authors show that the standard definition of free name is not preserved under the structural congruence, which is one of the sanity properties one would expect to have.

The traditional definition of the set of free names of a process term stipulates that the set of free names of a parameterized constant A(x₁,...,x_n) is {x₁,...,x_n}. Moreover, a term of the form A(y₁,...,y_n) is structurally congruent to P[y₁,...y_n/x₁,...,x_n] if the body of A(x₁,...,x_n) is the term P.

Consider now, for instance, the constant A(x) with body 0. The A(x) has x as its only free name. But this term is structurally congruent to 0, whose set of free names is empty! This is an example showing that the traditional definition of free names is not preserved by structural congruence, and we certainly want a process constant to be congruent to its body.

Why didn't anybody notice this before? As the authors write in their paper "Unfortunately the notion of free names is usually considered so simple that a formal definition is dispensed with and this occasionally shows up as problems in proofs."

In that paper, the authors develop a fixed point approach to the set of free names, argue that the set of free names can be computed efficiently and show that it is invariant under structural congruence.

I strongly recommend reading the paper.