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 so that it has exactly the same behavior as the original model but it has no importation state. A counter-example can be easily found. Suppose , which means model imports itself in state . This creates an infinite structure. It is impossible to find a non-recursive model 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.

** Proof** The

*function expand()
=
for in of
if is defined at then
=expand(
)
import into according to the algorithm in section 4.2.9
return *

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

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