4
$\begingroup$

In the book by Sangiorgi and Walker ("The $\pi$-calculus: A theory of Mobile Processes"), Subsection 3.2 is devoted to recursion. They state the following constraint (pages 132-133):

"The environment is finitary, in the sense that any process depends on only finitely many constant definitions. (Formally, the transitive closure of the relation that relates two different constants $K$ and $K'$ if an instance of $K$ occurs in the definition of $K'$, is well-founded.)"

I do not understand how the two sentences are related. Right after there is an example with the definitions of $B_0$, $B_1$ and $B_2$: instances of $B_1$ and $B_0$ occur in the definition of $B_0$; instances of $B_2$ and $B_0$ occur in the definition of $B_1$; and an instance of $B_1$ occurs in the definition of $B_2$. Thus the environment is "finitary" in the sense that each one of the constants $B_0$, $B_1$ and $B_2$ only depends on three constant definitions. But how is "the transitive closure of the relation that relates two different constants $K$ and $K'$ if an instance of $K$ occurs in the definition of $K'$" well-founded? This transitive closure should relate any of the three constants $B_0$, $B_1$ and $B_2$ to any of these same constants and thus, if I consider the set $\{ B_0, B_1, B_2 \}$, I cannot find a minimal element.

$\endgroup$
2
$\begingroup$

I am as puzzled as you are. Indeed, that looks wrong, as far as I can see. The mentioned relation can indeed have infinite descending chains, otherwise we could not have "cycles" which are needed for (mutual) recursion.

What should be ruled out is the presence of infinite descending chains involving infinitely many constants $K$. This is however a different requirement from well-foundation.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.