CMP.Preface:3.3 - Interpret, transform and compose computations

CMP.12 constructs an evaluator or a translation by specifying expression meaning, binding, primitive operations and control. The preservation relation follows what the receiving computation can observe. CMP.13 constructs a cheaper abstract computation for a selected property, with operations that justify its conclusions and a way to reconstruct or refine an apparent counterexample. CMP.14 constructs the shared-state or communication behavior needed when computations interact, including the assumptions under which progress follows.

The returned operations can themselves become objects of further work: an algorithm can interpret another algorithm’s description, a translator can transform it, and an abstract procedure can inspect its possible behavior. Mathematical Thinking supplies constructions of operations and interpretations. CMP adds effective execution and its consequences under the chosen computational model.

There is no compulsory fourteen-stage process. A reader with an adequate formulation can enter at a missing bound or representation. A representation failure can return to the recurrence; a semantic failure can return to interpretation; a communication failure can return to composition. Keep the required result and the assumptions of these connections visible when different agents supply the contributions.