CMP.Reference: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.
CMP.15 applies when independently added data variants and operations must work together. It supplies the required combinations, explicit joining implementations, recursive binding and preservation conditions. Use CMP.12 to derive an interpretation that a joining body still needs; use CMP.14 when shared state or changing visible methods introduces interaction. An adequate closed interpreter can remain unchanged when independent extension is unnecessary.
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.
These methods do not form a compulsory sequence. 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.