Contrôle dynamique.

Une procédure dans un programme est représentée par un ensemble fini de points de contrôle. Dans un programme multithread, chaque fil d´exécution (thread) se trouve à un moment donné dans un point de contrôle précis. Avec ces considérations, on peut modéliser la création dynamique des threads et la récursion comme un système de réécriture comprenant des règles de forme :

$$\begin{eqnarray*} X \Rightarrow Y \parallel Z \end{eqnarray*}$$

ou $X$, $Y$ et $Z$ sont des termes, et $\parallel$ est un opérateur de composition parallèle. Les termes dans ce cas sont des arbres binaires. La récursion à une expression similaire, utilisant des règles de forme :

$$\begin{eqnarray*} X \Rightarrow Y . Z \end{eqnarray*}$$

ou la sémantique est l´appel d´une procédure avec $Y$ comme point de contrôle initial et $Z$ comme continuation, après la retour. Dans ce cas on peut représenter les termes comme des tuples de mots finis, chaque mot étant en effet la pile d´un thread.