2.4 Closure under Importation

Importation is a kind of tight coupling between models.

Strictly speaking, DCharts are not closed under importation. I.e., it may not be possible to find such a model $M'$ so that it has exactly the same behavior as the original model $M$ but it has no importation state. A counter-example can be easily found. Suppose $\exists s\in S\ \cdot\ \Delta_M(s)=M$, which means model $M$ imports itself in state $s$. This creates an infinite structure. It is impossible to find a non-recursive model $M'$ with the same behavior.

If recursive importation is not considered, closure under importation can be proved with the algorithm described in section 4.2.9.

Theorem 1   Non-recursive DCharts models are closed under importation. I.e., models with importation states can be replaced by models without importation states, which have exactly the same behavior.

Proof The expanded model $M'$ of non-recursive DCharts model $M$ is found by the following algorithm:

function expand($M$)
$M'$=$M$
for $s$ in $S$ of $M'$
if $\Delta_{M'}$ is defined at $s$ then
${M'}_s$=expand( $\Delta_{M'}(s)$)
import ${M'}_s$ into $M'$ according to the algorithm in section 4.2.9
return $M'$

Since $M$ is non-recursive, this algorithm always terminates in a finite number of steps. The model $M'$ returned does not contain any importation state.

Obviously, $M'$ is still a DCharts model. According to the semantics of dynamic importation (section 4.2.9), it has exactly the same behavior as $M$. $\Box$