next up previous contents
Next: Flow graphs and semantics Up: Foundational models and abstract Previous: The tile model

Correct Transformations of Nondeterministic Programs

Computing systems have two parts: a computational part and a descriptive part. The descriptive part specifies the environment in which the computational part is to execute, and it may be nondeterministic (e.g. asynchrony in a system with communicating processes). The computational part is most often deterministic and can be implemented in various ways, which gives opportunities for optimisations.

Traditional program transformations, like fold/unfold-transformations, are however not always correct in the presence of nondeterminism. Yet, there is a need to perform optimising transformations on programs containing an environmental part, especially if the language concepts are very high level (and thus expensive to implement). The motivation for this work is to provide a theory to support the design and implementation of languages where the computational part can be optimised as freely as possible while preserving the (possibly nondeterministic) semantics for the full system. The results are general, but the intended target is recursive languages with process constructs.

If the computational and descriptive parts (both described as rewrite rules) commute, it is however possible to prove the validity of unfold/fold program tranformations. This earlier work within Confer-1 has been completed during this year [Lisp98]. These results hold under the classical condition of ``restricted folding-unfolding'' [Cou90], which is quite restrictive with respect to the formation of new recursive definitions. We have made some initial investigations towards extending the results to the particular formation of new recursive definitions that typically occur during program specialization. [[Lisp98]] B. Lisper.
Computing in unpredictable environments: Semantics, reduction strategies, and program transformations.
Theoretical Comput. Sci., 190(1):61-85, Jan. 1998.


next up previous contents
Next: Flow graphs and semantics Up: Foundational models and abstract Previous: The tile model

1/10/1998