Part C - Interpret, transform and compose computations

CMP.12 - Construct an Interpreter or a Meaning-Preserving Translation

Type: Method Status: Stable Normativity: Normative

CMP.12:1 - Problem frame

Use this when a calculation, rule language or program description has an intended meaning, but an effective way to execute it is missing, too costly or must change. You need to construct evaluation rules, translate the description into another executable form, or repair a translation that changes the result or behavior on which its user relies.

The reader can distinguish the admitted expressions and the operations they describe. The task is to turn those distinctions into an algorithm for evaluation or translation. Programs become inputs and outputs of that algorithm: a reader can examine how a rule is executed and change the rule’s representation without silently changing its use.

The result is an interpreter or effective translation, with the correspondence needed to use its output. Depending on the question, the preserved observation may include returned values, state changes, interaction, failure or termination. A compiler for a programming language, an evaluator for symbolic expressions and an interpreter for a decision language are different applications of this method.

Use an existing suitable evaluator or translator when it already provides the needed behavior affordably. Designing the notation’s useful distinctions is a separate question when those distinctions are still unknown. Choosing a physical realization follows the computational construction and its actual resource requirements.

CMP.12:2 - Problem

How can expression meaning be turned into effective evaluation and translation rules, so that the resulting computation preserves the observations needed by its user?

A mathematical interpretation can assign a meaning without providing an algorithm for obtaining it. A text substitution can preserve printed names while changing what they refer to. A translation can return the right value on a simple test while evaluating an unwanted branch, capturing another binding or failing to terminate on a previously terminating input.

CMP.12:3 - Forces

CMP.12:4 - Solution

Recover expression structure and observations → construct evaluation rules → make control and binding effective → construct the translation → establish the needed correspondence → execute and revise the changed rule.

CMP.12:4.1 - Recover the expression structure and the intended observations

Identify the constructors of admitted expressions and how their parts bind and compose. Work with a parsed structure when precedence, grouping or scope matters. A name occurrence must reach the declaration or external input intended by the language. If the supplied text admits different parses that change the answer, resolve that difference before constructing one evaluator.

Specify what evaluation receives and what its user can observe. Inputs can include the expression, name bindings, stored state and external responses. Outputs can include a value, changed state, a sequence of interactions or a failure. Distinguish a language-defined error from the absence of a defined operation; a translator can be required to preserve the former without being required to assign a meaning to the latter.

Choose the required relation between source and target observations. Equal returned values may suffice for a terminating pure expression. An interactive program may require the same ordered events. A source with several permitted behaviors may allow the target to choose among them; retaining every source possibility is a stronger requirement. Timing, memory use or a probability law belongs in this relation only when the receiving question uses it.

CMP.12:4.2 - Derive effective evaluation rules for each constructor

Construct the evaluator by cases on expression structure. For a literal, return its value. For a name, obtain its binding. For an operation, evaluate the required operands in the specified order and apply the available primitive. For a conditional, evaluate its test and then only the selected branch when that is the language’s rule.

Give binding an explicit operation. In an immutable lexically scoped language, evaluating let x=a in b first obtains a’s value in the current environment, then evaluates b in an environment extended with that binding. The extension’s scope ends with b. Nested use of the same printed name need not change the earlier binding.

For a function expression, construct an applicable value containing the parameters, body and the bindings its later execution needs. Such a value is a closure. To apply it under lexical scope, extend its saved environment with the argument bindings and evaluate its body there. If variables can change, distinguish names, storage locations and current contents so that a captured reference continues to designate the intended location.

Expose the primitive’s actual operation. An instruction to select an element satisfying a condition needs a search or other obtaining procedure. An unbounded search must retain its possible nontermination. If the implementation language has different arithmetic, truth values or evaluation order, translate those operations deliberately rather than inheriting its defaults.

CMP.12:4.3 - Make control, progress and resource use executable

Decide what remains to be done after the current subexpression returns. A recursive evaluator can retain that continuation in its own call stack. An explicit evaluator can instead store pending operations, environments and return destinations as data. Construct the transition that resumes the pending work with the obtained result.

Distinguish the termination of translation from the termination of the translated program. A compiler that traverses a finite syntax tree can terminate even when the generated program runs indefinitely. A step limit can return a suspended computation; reaching that limit does not establish divergence. CMP.1 supplies the limit on general termination decision when that question arises.

Count consequential dispatch, environment lookup, retained continuations, arithmetic and storage. Removing repeated syntax analysis may repay compilation for repeated execution. For a rarely used or frequently changing expression, direct interpretation may be the cheaper choice. Retain the existing algorithmic cost and comparison methods rather than assuming compilation always improves the work.

CMP.12:4.4 - Construct translation from the evaluation structure

Choose a target instruction or expression language with defined execution rules. For each source constructor, generate the target operations that perform its required evaluation. Construct the translation of subexpressions and then their combination, retaining temporary results until their consumers use them.

Preserve binding and control at this construction step. Allocate fresh temporary names or use addresses whose scopes cannot capture unrelated bindings. Place conditional branches behind the appropriate control transfer. Pass arguments and return results through agreed locations. An operator with effects requires the relevant order and number of executions; algebraic reassociation alone does not supply that permission.

State how source values, environments and observations correspond to target ones. A target representation may require encoding inputs and decoding outputs. Check that admitted values fit its arithmetic and storage operations. If one representation deliberately approximates another, use CMP.8 for the qualified relation instead of claiming unchanged values.

When several translation passes are used, connect their actual input and output relations. Each pass’s output must satisfy the next one’s premises. MATH.17 and MATH.18 supply composition and interpretation reasoning; the computational work additionally provides the terminating conversion and executable target operations.

CMP.12:4.5 - Establish the correspondence at the scope needed

For a structurally recursive translation of a terminating expression language, use induction on expression construction. Include the context that surrounding code can supply: an arbitrary admitted environment, earlier stored values and the continuation after the translated fragment. A claim that works only with an empty stack may fail as soon as two fragments are composed. Section :5.1 derives the stronger usable claim.

For stateful or interacting languages, relate source and target states and the observations their transitions produce. Explain how matching transitions reestablish the relation. If several internal steps implement one visible step, account for their completion; an infinite internal loop must not masquerade as successful preservation of a terminating computation. Choose the simulation direction or behavior relation that supports the requested conclusion. Showing that one source run has a target counterpart alone leaves other target behavior unresolved.

An alternative is to describe sets of terminating, diverging, failing or interacting behaviors and show that translation preserves the selected relation between them. Use this when the language’s semantic operations and composition laws make the argument simpler. Preserve the distinctions that the use needs when choosing this mathematical representation.

Separate a general preservation claim from a check on selected translations. A small comparison can expose a defective rule or settle a bounded receiving case. A claim covering every admitted expression needs an argument covering that class. Use C.11.DUA to choose further testing, translation-specific validation or a general proof according to what the receiving decision requires.

CMP.12:4.6 - Run the construction and revise the failed correspondence

Evaluate or translate a meaningful input and use the resulting value or behavior. Return the construction together with the input, binding, execution and recovery conditions needed by its recipient. When comparison fails, locate the changed constructor, binding, primitive, control rule or value correspondence.

A changed language feature or execution context reopens its dependent translations. Preserve unaffected rules. Adding assignment requires revisiting captured bindings; changing integer arithmetic requires revisiting arithmetic correspondence; allowing externally supplied code requires examining the contexts with which translated components interact.

CMP.12:5 - Archetypal Grounding

CMP.12:5.1 - Derive an arithmetic interpreter and stack translation

Expressions are integer literals, names and binary addition, subtraction or multiplication. An environment ρ supplies every free name. Both source and target use unbounded integers. The source evaluator returns a literal, looks up a name, or evaluates the left operand and then the right operand before applying the operator.

The target stack is written from bottom to top. PUSH n appends n; LOAD x appends ρ(x). For ADD, SUB or MUL, pop the right operand b and then the left operand a, and append respectively a+b, a-b or a*b.

Construct the compiler C:

• C(n) = PUSH n.
• C(x) = LOAD x.
• C(a op b) = C(a); C(b); OP, where OP is the matching target operation.

The useful induction claim is: for every admitted ρ and every initial stack S, running C(e) leaves S · [eval(e,ρ)], with earlier entries unchanged. Literals and names append the required value. For a binary expression, the induction hypothesis for a gives S · [eval(a,ρ)]; applying the hypothesis for b to that whole stack appends eval(b,ρ). OP replaces just those two entries by their required combination. This proves the claim and supplies the composition condition.

With ρ(x)=5, compile (x+1)*(x-2) to:

LOAD x; PUSH 1; ADD; LOAD x; PUSH 2; SUB; MUL

Starting above an earlier stack value 99 gives successive added values 5, 1, then 6; next 5, 2, then 3; multiplication leaves [99,18]. Each syntax-tree node produces one instruction. Integer operation costs and peak live stack values still depend on the values and expression structure.

Changed arithmetic: suppose the target uses unsigned eight-bit wraparound. For x+1 at x=255 it returns 0, while the source returns 256. Preserve the source by using a wider or multiword representation, restrict the admitted inputs by a valid range argument, or deliberately change the source meaning to modular arithmetic. A successful parse and a preserved instruction order do not fix the arithmetic mismatch.

CMP.12:5.2 - Preserve a function’s binding when its call site changes

Extend the evaluator with immutable lexical bindings, function values and function application. Evaluate:

let x = 2 in
  let f = (lambda y: x + y) in
    let x = 100 in f(3)

Creating f saves its body, parameter y and the environment in which x is 2. Calling f extends that saved environment with y=3, so the body returns 5. Looking up free x in the caller’s environment would return 103 and implement a different binding rule.

The closure makes a rule available as a value without discarding its needed surroundings. A procedure can return it, receive it as an argument or construct a new closure that composes it with another rule. Each later application follows the saved bindings and the new arguments.

Changed feature: now permit assignment to the original captured x before calling f. If the language specifies capture of that variable’s location, assigning it 7 makes f(3) return 10. Keeping a copied value 2 would instead return 5. Represent the environment as names mapped to locations and obtain current values from the store; a later shadowing declaration must allocate a different binding. Revise the capture and lookup rules without changing the arithmetic rule.

CMP.12:5.3 - Preserve which operation is executed

Let ifzero(test,a,b) evaluate test and then only a when the result is zero, otherwise only b. Let division by zero be a defined execution error. The expression ifzero(x,0,10/x) returns 0 at x=0 and 5 at x=2.

A translation that evaluates all three parts and then selects a value raises the unwanted division error at x=0. Instead generate fresh labels and conditional control:

LOAD x
JZ zero
PUSH 10; LOAD x; DIV
JMP end
zero: PUSH 0
end:

JZ pops the test and jumps when it is zero; otherwise execution continues. JMP transfers control unconditionally. DIV pops right then left and divides left by right, using rational values here. Resolve each fresh label to its instruction position before execution. At x=0 the division instructions are skipped; at x=2 they append 5. Either path preserves earlier stack entries and appends one result.

If the branches instead emit commands, the same construction retains which command occurs. If the source is deliberately changed to evaluate both branches, the preservation claim and translation must change with it. The control rule, rather than a particular programming language’s spelling, determines this choice.

CMP.12:5.4 - Preserve completion through internal steps

The source instruction is return 7; the receiving use requires that return. A target first takes k internal steps and then returns 7, where k is a supplied nonnegative integer. Use a remaining-step counter: each internal step reduces it by one, and at zero the target returns. For every finite k the counter proves that the internal phase finishes, so the target supplies the required result.

Change the target to loop: goto loop, leaving return 7 after this loop. Each internal step goes back to loop, so the return is unreachable. A correspondence that allows arbitrarily many silent steps without a completion argument would hide this failure. Restore a finite internal phase to meet the required return.

CMP.12:6 - Bias-Annotation

A familiar implementation language can silently supply truth tests, numeric limits, scope or evaluation order. Recover the intended operation before reusing that default. The arithmetic, closure and conditional cases each show a different observation lost by an apparently straightforward implementation.

CMP.12:7 - Conformance Checklist

• Expression formation, binding and needed observations are recoverable.
• Every required evaluation step has an available operation and an explicit control rule.
• Translation terminates on its admitted descriptions; execution progress has its own stated scope.
• Source and target values, bindings, states and observations have the correspondence required by the use.
• The preservation argument includes the surrounding state or context needed for composition.
• Cost includes translation and execution under the actual arithmetic and storage assumptions.
• A changed rule or failed comparison leads to a specific reconstruction.

CMP.12:8 - Common Anti-Patterns and How to Avoid Them

CMP.12:9 - Consequences

Descriptions of computations become material for further computation. A reader can construct an evaluator, remove repeated interpretation work, combine translated fragments and diagnose a changed result through its binding, control or representation rule.

Preservation is relative to the observations and contexts selected. A useful translation may leave a reverse translation unavailable, select among allowed behaviors, or preserve values while having different resource costs.

CMP.12:10 - Architectural Rationale

An expression, its mathematical meaning, an evaluator and one execution are different objects in this work. Keeping their correspondence visible lets operations themselves become inputs to constructive transformation. MATH.17 and MATH.18 provide the mathematical composition and interpretation; algorithmics supplies an effective evaluator or converter and explains its execution.

The preservation claim includes composition because translated fragments are normally used together. The arbitrary earlier stack, captured environment and selected branch are three forms of context that change what a local construction must retain. State-based and behavior-based descriptions offer different ways to carry that argument across a larger language.

CMP.12:11 - SoTA-Echoing

How should expression meaning become executable? Adopt the constructor-based evaluation and saved-environment application in SICP’s evaluator for :4.2–4.3. Its historical contribution is exposing operations otherwise hidden in a host language. A direct evaluator is a serious cheaper choice for changing or infrequently executed expressions. Adapt SICP’s compilation construction when prior analysis repays its cost over subsequent runs: construct operations instead of repeatedly selecting them during execution. Keep binding and control semantics while comparing conversion, code storage and later execution. A changed execution frequency, primitive or language feature reopens that choice.

Which preservation claim supports actual reuse? Adopt the explicit behavioral scope in the current CompCert manual, section 1.2, for :4.1 and :4.5. Matching final values is sufficient only for uses governed by those values; interaction and termination can require more. CompCert’s theorem has its own language-defined behavior and undefined-behavior treatment, and excludes time and memory consumption from its observed trace. A translator for a language with a defined division error therefore needs the error policy chosen in :5.3, not an imported C-specific permission to remove it. A changed observation or admitted execution context reopens the relation.

For larger compositions, adapt the choice between operational simulation and denotational behavioral refinement examined in Denotation-based Compositional Compiler Verification. The latter uses algebraic composition of behavioral sets to reduce proof duplication, while retaining termination, divergence, failure and interaction distinctions that simpler final-state accounts can lose. Use it when those operations fit the language and simplify the actual preservation argument; a direct structural or state correspondence remains sufficient for the small constructions here. Neither proof representation automatically supplies a cheaper compiler. Changed control features, module interaction or proof-maintenance cost can reverse the selection.

CMP.12:12 - Relations

• MATH.5, MATH.17 and MATH.18: supply extension through expression construction, operations on operations and interpretation/composition arguments.
• CMP.1: supplies effective conversion and answer recovery for computational reductions; interpretation here also retains the required execution behavior.
• CMP.2, CMP.3 and CMP.10: supply recursive construction, sharing and computational representation choices used by an evaluator or translator.
• CMP.8: qualifies deliberate approximation of represented values.
• CMP.15: composes independently added expression variants and operations when new required combinations need their own implementation and preservation conditions. A sufficient closed interpreter does not require that extension architecture.
• C.29.2 and C.29.3: supply the surrounding computational formulation and physical realization questions.
• C.11.DUA: selects additional validation or proof by the conclusion it can change.

CMP.12:End

CMP.13 - Construct a Computational Abstraction for the Property Being Asked

Type: Method Status: Stable Normativity: Normative

CMP.13:1 - Problem frame

Use this when computing every relevant state or execution is unaffordable, but the question needs only some of their properties. You want to calculate with ranges, classes, relations or other summaries and determine what their answers establish about the original computation. Use it also when such a calculation reports an impossible path or loses a distinction needed for the answer.

The reader can describe the admitted inputs, elementary transitions and requested observation. Examples include asking which outcomes a rule system permits, whether a procedure can reach a failing state, or which dependencies can affect a returned value. The method constructs another computation over descriptions of possibilities, then relates its result to the question.

The first useful result is an effective abstract operation or small abstract execution with a justified conclusion about the original process. Extending that result across loops or interacting components requires the corresponding closure or composition argument. A finite reachability example can be done by hand; building an analyzer for a programming language requires its semantics and suitable algorithms for its representations.

Use direct computation when it already answers the question affordably. If the required change is a numerical error allowance, CMP.8 supplies that construction. If the problem is whether the original process describes the intended subject, return to that modeling question: a sound calculation about the process retains its subject assumptions.

CMP.13:2 - Problem

How can a calculation discard detail yet retain a justified answer to the property being asked, and recover the distinctions that an inconclusive answer exposes?

A summary can combine possibilities that never occur together. A sequence of individually possible transitions can then appear to be an executable path. Conversely, retaining every distinction may make the supposedly cheaper calculation as difficult as the original. Loops add another difficulty: successive summaries can keep changing even when each update is easy.

CMP.13:3 - Forces

CMP.13:4 - Solution

Local mantra: choose the property; describe the represented possibilities; derive the abstract operations; compute a sufficient closure; interpret the answer; refine the distinction that blocks its use.

CMP.13:4.1 - Choose the observation and the direction of inference

Specify the original states, initial possibilities and transitions. Include the program location or phase when the same stored values permit different next steps there. Identify what the answer concerns: a reachable value, a path, termination, an interaction or another property. A set of reached states usually loses the order needed for a path question.

Choose what an abstract value represents. Write gamma(a) for the original possibilities represented by abstract value a. It can be a set of integer values, environments, graph states or complete traces. The concrete domain in this construction is the process being analyzed; it need not consist of physical objects.

For an overapproximation, every original possibility must remain among the represented ones. If the calculated possibilities exclude a bad outcome, that outcome is excluded from the original process. An included bad outcome may require reconstruction before it supports a counterexample. For an underapproximation, represented possibilities must be realizable: a retained witness can establish existence, while a missing witness leaves other executions unresolved. Choose the direction for the question and maintain it through the operations. The remaining steps develop the overapproximation branch.

CMP.13:4.2 - Derive computable operations on the summaries

For an original operation f and abstract input a, construct f#(a) so that it covers every allowed result of applying f to an input represented by a. If post(X) collects the one-step successors of states in X, the condition is:

post(gamma(a)) ⊆ gamma(post#(a)).

This is the soundness direction: the abstract step may add possibilities, but it must retain every original successor. Handle branch restrictions, failure and the actual arithmetic under the same interpretation. For example, an interval operation justified over unbounded integers needs revision for wraparound arithmetic.

Provide a way to combine incoming possibilities. An abstract join of a and b covers gamma(a) ∪ gamma(b); it may include additional states. Implement the comparison used to recognize that a new result is already covered. Choose a representation whose operations and comparisons are affordable; an arbitrary logical formula may express the wanted property while making those operations difficult to compute.

A constructive starting point is to apply the original operation conceptually to the represented inputs, identify the property of all resulting outputs, and derive a formula for that property. The derived formula performs the abstract calculation without enumerating those inputs. Independent ranges, relations between variables and partitions by selected conditions provide different choices. Use the stronger choice where the receiving question needs the distinction it retains.

CMP.13:4.3 - Compute a result closed under the admitted transitions

For a finite graph of program points, associate an abstract state with each point. Initialize it from the admitted inputs. Recompute a successor when a predecessor summary changes and join its new contribution with the old one. CMP.3 supplies dependency scheduling and reuse. With finitely many points, monotone updates and an abstract order with no infinite increasing chain, a fair worklist reaches a stable result; the number and cost of updates still determine feasibility.

An infinite or very long increasing chain may need extrapolation. A widening combines successive approximations into a covering value and is chosen so the widening iteration stabilizes. For intervals, a bound that keeps moving outward can be replaced by an infinite bound. Apply such extrapolation where cyclic dependencies need it. Call context, retained relations and placement of widening can change precision, so a larger summary language alone does not guarantee a better computed answer.

Check the resulting closure. If I is the initial set and a the proposed result, the sufficient conditions are:

I ⊆ gamma(a) and post(gamma(a)) ⊆ gamma(a).

Every reachable state is then represented: induction on execution length uses the first condition for the start and the second for each step. An implemented abstract transformer can establish the second condition by showing its result is covered by a. Such an a is often called a post-fixpoint. A prematurely interrupted growing approximation need not contain every reachable state.

If the closure is too broad, use restrictions from guards, a more discriminating representation, or a narrowing operation with its own soundness conditions. A proposed smaller set is useful only while retaining the initial possibilities and closure. Directly checking these two conditions is often enough for a small construction. An all-executions termination or response-time claim needs a corresponding argument; a closed set of reached states alone supplies neither.

CMP.13:4.4 - Recover the conclusion and examine a reported witness

Apply the requested observation to the closed result. If its represented states all satisfy the property, use that conclusion with its original input and transition assumptions. If the result overlaps an unwanted outcome, determine whether the overlap changes the next action. It may already be sufficient to retain the unresolved alternative.

When an actual path matters, reconstruct consecutive original states, starting from an admitted initial state. For abstract path a0, a1, ..., ak, propagate:

X0 = I ∩ gamma(a0);

X(i+1) = post(Xi) ∩ gamma(a(i+1)).

If some Xi is empty, the abstract path is spurious: its steps cannot be joined into one original execution. If the last set is nonempty and these sets were computed without adding possibilities, retained predecessors can recover a concrete path. If this reconstruction is itself approximate, qualify its result with that approximation’s direction; a nonempty overapproximation still leaves feasibility unresolved.

Loops and infinite-path properties require their own path and recurrence conditions. A finite prefix reaching a bad state settles finite reachability; repeating an abstract cycle does not by itself produce an infinite original execution.

CMP.13:4.5 - Refine the lost distinction and continue from the affected computation

Locate where the reported execution or answer became impossible. Restore the distinction responsible: separate a merged state, retain a relation, distinguish a calling context, or make an abstract operation more precise. A false path through one merged class can suggest splitting its reachable dead ends from the states that supply its outgoing edge.

Recompute affected dependencies and reuse results whose inputs and interpretation remain valid. Confirm that the revised construction removes the particular spurious result and still covers all original behavior. Removing one false path may leave others.

Choose further refinement by what it can change in the receiving work. A coarse result that already answers the question is sufficient. A real counterexample changes the original construction or its allowed use; improving the analyzer cannot make that execution disappear. When refinement remains too costly or inconclusive, return the unresolved property and the condition under which another calculation or direct execution would help. C.11.DUA governs the worth of that additional work.

CMP.13:5 - Archetypal Grounding

CMP.13:5.1 - A graph summary invents a path

The original graph has vertices a,b,c,d, edges a->b and c->d, and initial vertex a. The question is whether d is reachable. Merge b and c into abstract vertex q, while keeping a and d separate. An abstract edge exists when any original edge connects the corresponding classes.

The abstract graph has a->q and q->d. Searching it returns the path a,q,d. Each edge has an original witness, yet the first edge arrives at b and the second leaves c.

Reconstruction gives X0={a}, X1={b} and X2=empty, since b has no successor. Split q into {b} and {c}. The recomputed reachable set is {a,b}, so d is unreachable. The useful result is both the answer and the reason the original summary could not establish it.

Changed condition: add edge b->c. The abstract path a,q,q,d now reconstructs to a,b,c,d; this is a real path. The shorter path a,q,d still has no consecutive realization, but its failure no longer excludes reachability. The transition change requires the affected search and reconstruction to be updated.

CMP.13:5.2 - Obtain a loop property without enumerating its iterations

Consider unbounded integers, positive integer N, and:

x = 0
while x < N:
    x = x + 1

At the loop head, a set X of possible values is transformed by F(X)={0} ∪ {x+1: x∈X and x<N}. An interval hull supplies an abstract transformer. Starting at [0,0] produces [0,1], [0,2] and so on until [0,N]; this takes a number of expansions proportional to N even though N can be written with logarithmically many bits.

Widen the increasing upper endpoint of [0,0] and [0,1] to obtain [0,+infinity]. It contains the initial value and is closed under the guarded update. It already establishes that x is never negative.

Suppose the receiving question instead asks for the value on exit. Apply the guard to [0,+infinity]: the integer inputs admitted by x<N are [0,N-1]; adding one and joining the initial value gives [0,N]. This smaller interval is itself closed under F, and contains 0. The exit condition x>=N then leaves [N,N]. Therefore every terminating execution exits with x=N.

For a termination conclusion, add a different argument: while the guard holds, the nonnegative integer N-x decreases by one, and the arithmetic is unbounded. This proves termination from 0 for the stated positive N. It explains why the exit value is obtained, rather than merely describing it if obtained.

Changed condition: replace the update by x=x+2, retaining N=5. The guarded interval calculation now gives [0,6]; exit intersection gives [5,6]. If that bound is sufficient, stop. If the final value is needed, retain the invariant that x is even as well. The exit result becomes {6}. The old answer 5 was tied to the former update.

CMP.13:5.3 - Independent ranges lose the determining relation

Let input b be either 0 or 1. Execute x=b; y=b, then test whether x!=y. Independent intervals give x∈[0,1] and y∈[0,1]. Their product contains (0,1), so it cannot exclude the unequal branch.

Recover the construction: both assignments use the same b. Retain x=y, or keep the two input cases separate. Each choice excludes the unequal branch. The shared equality is the needed distinction; refining both independent endpoint ranges cannot recover it.

If the second assignment becomes y=1-b, both inputs take the unequal branch. A retained relation must be derived again from the changed operation. The earlier equality is an invalid assumption in the new computation.

CMP.13:6 - Bias-Annotation

An alarming abstract result can draw attention away from whether its states form an executable case. Trace reconstruction tests that inference. A preference for simpler summaries can hide correlations; a preference for stronger analyses can spend resources recovering distinctions that the current answer does not need. Compare the actual result and cost under the requested observation.

CMP.13:7 - Conformance Checklist

• The initial possibilities, transitions and requested observation identify the computation being analyzed.
• Each abstract value has an interpretation, and the inference direction supports the claimed conclusion.
• Abstract operations and joins cover their original counterparts; the obtaining algorithm has a justified completion or bounded-result condition.
• A whole-reachability conclusion uses initial containment and transition closure.
• A claimed concrete counterexample has a consecutive realization; a failed reconstruction identifies the lost distinction or remaining uncertainty.
• Refinement preserves the original possibilities and changes a result relevant to the receiving work.

CMP.13:8 - Common Anti-Patterns and How to Avoid Them

CMP.13:9 - Consequences

The reader obtains a computation over properties, together with the direction in which its answers apply. A false abstract counterexample becomes a constructive guide to a better representation. An already adequate coarse result can end the work.

The result depends on the original semantics and on the abstract operations, evaluation strategy and observation. A sound representation can still yield an answer too imprecise or expensive for use. Some properties remain undecidable or require a different form of reasoning.

CMP.13:10 - Architectural Rationale

The construction combines two methods of thinking: choose a mathematical account of possible states, then build an effective algorithm on that account. MATH.2’s quotient preserves specified operations independently of representative. Here a summary may deliberately combine different successors, so its justification is inclusion of possibilities rather than equality of returned classes. MATH.18 supplies the direction-sensitive comparison between accounts.

The examples expose three distinct causes of lost information: incompatible representatives in a path, extrapolation across iteration, and discarded correlation. Their repairs act on the abstraction and its algorithm. The physical or organizational interpretation of the original state system remains a separate subject correspondence.

CMP.13:11 - SoTA-Echoing

How can a cheaper computation answer a selected question about executions? Adopt the calculational approach organized in Cousot’s Principles of Abstract Interpretation: choose the property semantics and derive effective abstract operations. Its scope includes dataflow, dependency and typing as well as numerical properties. This changes :4.1–4.3 from selecting a convenient picture to constructing a sound obtaining procedure. Direct finite exploration remains a serious cheaper alternative when its state space is manageable; a changed property or obtaining cost reopens the choice.

When independent summaries lose a needed relation, adapt the combination of algebraic and logical abstractions in Cousot, Cousot and Mauborgne, especially their sound-transformer and reduced-product constructions. Combine complementary restrictions when that recovers the answer more cheaply than one uniformly rich domain. Solver-backed relations accept solver and representation costs; simple precomputed operations accept reduced expressiveness. The paper’s implementation comparisons are historical, not a ranking of current tools. The choice changes :4.2 and :4.5 and is reopened by a relevant lost correlation or unsupported machine semantics.

For a reported abstract counterexample, adopt the reconstruct-and-refine step from Clarke and colleagues, sections 4.3–4.4. Its finite-path construction motivates :4.4–4.5 and :5.1: split the distinction that prevents consecutive realization. Uniformly increasing precision is the rival; it can resolve more future questions but pays for distinctions this path may not need. Infinite-path properties require the additional loop conditions rather than reuse of the finite-path test alone.

How should cyclic abstract computations be scheduled? Adapt the question raised by Yang and colleagues’ 2025 interprocedural ordering method: distinguish actual recursive dependencies from spurious cycles introduced by merged call contexts, then choose where widening and narrowing operate. This strengthens :4.3’s dependency-sensitive choice. A simple global worklist remains suitable when it produces an adequate result at lower construction cost. The reported advantages concern the paper’s recursive-program analyses; they do not establish a universal schedule for every abstract domain. Lost call correlation or iteration cost can trigger reconsideration.

CMP.13:12 - Relations

• MATH.2 and MATH.18: supply operation-preserving identification and interpretations between mathematical accounts; the overapproximation here has its stated one-way consequence.
• CMP.3 and CMP.4: supply dependency reuse and search; closure over cycles and reconstruction of abstract witnesses are developed here.
• CMP.8: supplies controlled numerical approximation; inclusion of possible executions answers a different question from numerical closeness.
• CMP.12: supplies effective interpretation of the original expressions and operations whose semantics this abstraction uses.
• C.29.1 and C.29.2: supply the surrounding interpretation and computational formulation; applying the result to its intended subject returns to C.29.
• C.11.DUA: selects further analysis by the receiving action or conclusion it could change.

CMP.13:End

CMP.14 - Compose Interacting Computations through Their Required Observations

Type: Method Status: Stable Normativity: Normative

CMP.14:1 - Problem frame

Use this when computations that work separately must run together, but shared state, communication or scheduling can change their results. You need to construct their interaction, repair a failing interleaving, or replace a component while retaining the behavior on which the rest relies.

The reader can describe each component’s operations and the results expected from their combination. This method adds the shared state, communication and ordering rules needed to reason about the whole. It applies to concurrent algorithms and protocols, including computations performed by cooperating software agents. The implementation language and physical machine supply particular operations and failure conditions.

The first useful result is a composed procedure with a trace or invariant explaining how it obtains the required observation, or a counterexample that identifies the interaction to change. A small shared-state example needs only a few explicit steps. A general guarantee over an implementation needs the corresponding memory, scheduling and failure assumptions.

Use ordinary sequential composition or dependency scheduling when completed outputs suffice and no relevant interference remains. If the algorithms are already adequate and only their physical communication or timing is unresolved, take those requirements to the realization method. An organizational division of work needs its own account of actual roles, capabilities and authority; a computational model can help compare it once that correspondence is established.

CMP.14:2 - Problem

How can separately useful computations be connected so that their possible interactions produce the required behavior, and what must change when one component’s assumptions fail?

Two correct increments can lose an update. Retrying a request can repeat its effect. Individually finite operations can wait forever for one another. A replacement that returns the same final value can expose a different intermediate state to its neighbors. These failures concern the composition, so executing each component alone does not expose them.

CMP.14:3 - Forces

CMP.14:4 - Solution

Local mantra: choose the observations; expose the interactions; construct compatible steps; find the failing order or invariant; repair the protocol; establish progress under its actual assumptions.

CMP.14:4.1 - Specify what the combined computation must make observable

State the allowed inputs and required results. Include the observations a receiving component can make while work is in progress: returned values, shared-state reads, messages, failures or completed operations. Distinguish a request from each attempt to transmit or execute it when retries are possible.

Choose the required ordering. For a concurrent object, linearizability compares a history of calls and responses with legal sequential behavior. A finite history can contain pending calls. Append responses to any selected pending calls, then omit those still pending. Keep every originally completed operation, including its arguments and returned value. Seek a legal sequential order of the retained operations that respects every case where one operation returned before another was called. Each retained operation appears to take effect between its call and response in this extended history.

The appended responses belong to this comparison; they do not establish that the pending operations will actually return. Section :5.4 shows a pending call whose effect another operation has already observed. Other applications may accept weaker order, duplicate-tolerant combination or eventual agreement; use the property the receiving computation needs.

Also state required eventual events, such as a pending operation returning. An acceptable state or finite history does not alone settle that question. In concurrency theory, a safety property excludes a violation detectable in a finite execution prefix; a liveness property requires progress that no finite delay alone disproves. These meanings describe execution properties here.

CMP.14:4.2 - Expose steps, shared state and the environment

Give each component its local state and point of execution. Identify shared variables, owned data, channels and the operations that connect them. For each elementary action, specify when it is enabled, what it reads and changes, and which other values remain unchanged.

Choose the granularity supported by the computational model. A source statement that reads and then writes a value may allow another component’s step in between. If a compare-and-swap or transaction is assumed atomic, its availability and scope are part of the construction.

Under an interleaving shared-memory model, form the combined state from the components and shared store, and let an enabled component take one step at a time. Message passing adds channel states and send/receive transitions; rendezvous requires the participating steps together. Include the admitted environment transitions, such as message loss, duplication, restart or input arrival, where the required claim depends on them.

A real language or memory model may permit observations absent from simple interleaving. Recover its ordering and visibility rules before transferring the argument. The method can then change the synchronization or the model instead of concealing the missing premise.

CMP.14:4.3 - Derive a compatible invariant or interaction rule

Construct the relation that must survive composition. For example, the shared counter must equal the number of committed increments, a request identifier must have at most one committed effect, or a waiting computation must request only a resource later in an acquisition order.

Establish that relation initially and inspect each allowed transition that can affect it. Local predicates must survive permitted environment steps. Rely/guarantee reasoning makes this explicit: a component assumes a stated interference relation from its environment and establishes a stated relation for its own steps. Its neighbors’ possible steps must fit that assumption. Check the step-level conditions and their initial basis; mutually assuming that the other component eventually succeeds supplies no initial progress.

For a finite construction, explore enabled interleavings until a failure or the relevant closed state set is obtained. CMP.4 supplies search and CMP.13 supplies a qualified abstraction when the state space is too large. A counterexample should retain enough state and ordering to reproduce the offending interaction.

When operations commute under the observations of interest, exploit that property: some orders can be combined or avoided in exploration. Include intermediate observations in the comparison. Equality of the final store is insufficient if a neighboring read distinguishes the swapped operations.

CMP.14:4.4 - Change the interaction that causes the failure

Construct a repair from the failed premise. Common choices have different costs:

Execute the original failing trace against the repair, then inspect the transition family that caused it. This both explains the changed behavior and identifies what a more general argument must cover.

CMP.14:4.5 - Establish the progress actually promised

Identify what can enable and execute each required next step. A component may wait for another component, a message or a resource. A finite dependency with an available first move differs from a cycle in which every participant waits.

Choose only scheduling and delivery assumptions the intended use can support. Weak fairness excludes postponing an action forever once it remains continuously enabled. Strong fairness also excludes postponing an action forever when it becomes enabled infinitely often. Name the action or action family: fairness for an entire process does not make every branch of its code fair.

Use those assumptions with a progress measure or a dependency argument. Show why a required response eventually becomes possible and occurs. A bound on elapsed time additionally needs timing and resource bounds. A retry limit provides a finite failure return, not a guarantee that the requested effect happened or that it did not happen.

Test the relevant lost-progress case: an unavailable participant, an indefinitely lost reply, a stopped lock holder or an unfair scheduler. Return the supported result or the unresolved execution status. Do not preserve an eventual-response claim after removing its delivery or scheduling premise.

CMP.14:4.6 - Compare replacements through the composed observation

Relate the detailed execution to the promised higher-level operation. Some implementation steps may leave the chosen observation unchanged. That permits a coarser description, but hiding indefinitely many such steps can conceal lost progress; qualify the correspondence accordingly.

For replacement, ask whether the new component introduces an observation the allowed context could not obtain before. Include context interactions, failure and progress when they are part of the required behavior. A final-value comparison is sufficient only for a receiving use governed by that value.

Return the constructed coordination procedure, the result it supports and the assumptions the next user must retain. If a supplier changes its operation, memory rule, failure behavior or response promise, reopen the dependent composition. Use the common result-cost comparison and C.11.DUA when deciding whether another experiment, formal argument or alternative implementation would change the next move.

CMP.14:5 - Archetypal Grounding

CMP.14:5.1 - Two increments need an operation that survives interference

Initially x=0. Two components each perform r=x; x=r+1 once. Reads and writes are atomic, arithmetic uses unbounded integers, but the pair is not atomic. The required final result after both operations is 2.

One admitted execution is:

A reads 0
B reads 0
A writes 1
B writes 1

The final value 1 violates the required result. Replace each increment by:

repeat:
    v = read(x)
    if compare_and_swap(x, v, v+1) succeeds:
        return

Compare-and-swap tests the current value and, only if it equals v, changes it to v+1 in one atomic action. A failed attempt leaves x unchanged.

The invariant is x = number of successful compare-and-swap actions. It holds initially; each success increases both sides by one, while reads and failed attempts change neither. Each component returns after its first success. Thus, when both return, x=2. A successful action supplies the point at which its increment takes effect in the sequential account.

If A and B both read 0, A can succeed first; B’s stale attempt fails. B then reads 1 and succeeds with 2. For these two one-shot callers, each failed attempt is attributable to the other caller’s success, so there can be at most one failed attempt before that caller completes. With both callers continuing to receive steps, both finish. A system with an unlimited stream of competing callers needs a different per-caller progress argument.

Changed condition: the environment supplies only a separate comparison and write. The old failing order is possible again. Use a primitive that really combines them or protect the read-modify-write region. Naming the pair “compare-and-swap” does not create that operation.

CMP.14:5.2 - A retry must refer to the same logical operation

A sender requests that a receiver add 5 to a stored counter. Initially the counter is 0. Messages may be lost or duplicated; the receiver continues running and retains its state. The receiver performs the addition, but the reply is lost. Blindly repeating the addition can leave 10 even though the sender requested one increment.

Give the logical request an identifier k that is not reused while an old request or reply with that identifier can still arrive. The sender retries the same pair (k, add 5). At the receiver, process the following as one atomic state transition:

if k is already in completed:
    result = completed[k]
else:
    counter = counter + 5
    result = counter
    completed[k] = result
send reply(k, result)

Only the state-changing conditional must be atomic; sending the reply can occur afterward. The first request changes the counter to 5 and stores completed[k]=5. Every duplicate returns 5 without another addition. The invariant relates a remembered identifier to its one committed effect. It depends on the same identifier denoting the same request payload.

At-most-once effect needs no promise that a message is eventually delivered. To promise a returned answer as well, suppose the sender keeps retrying, delivered requests are eventually processed, and each direction is a fair-loss channel: a message sent infinitely often is delivered infinitely often. The receiver answers each delivered request. These conditions ensure a reply eventually arrives. The result is a delivery-and-processing argument, not a deadline.

Changed condition: after applying the effect, the receiver can restart with the counter retained but completed lost. A later retry can again produce 10. Preserve the effect and its identifying result together across the admitted failure, for example through a durable atomic state update, or use an operation whose repetition is acceptable. An effect performed by another service needs that service’s corresponding guarantee; persisting only the local identifier leaves the effect/record crash gap unresolved.

CMP.14:5.3 - An acquisition order removes a waiting cycle

Two computations need exclusive resources L and R. A obtains L and waits for R; B obtains R and waits for L. Both acquisitions were locally valid, but neither computation can proceed to release its first resource.

Choose one strict total order, L<R, and require both computations to acquire L before R. More generally, each computation acquires resources in strictly increasing order and releases them after its finite protected work. It waits only for these resource acquisitions.

A resource-wait cycle would require a strictly increasing sequence of resource positions to return to its starting position, which is impossible. The construction therefore excludes deadlock of this acquisition form. A waiting computation can still be postponed indefinitely by unfair grants. A starvation-freedom claim additionally needs a suitable grant policy and progress by holders; a bounded waiting time needs further bounds on their work and scheduling.

Changed condition: introduce a callback while holding R that tries to acquire L. This violates the shared order and can restore a cycle. Move the callback outside the protected region or redesign the acquisition protocol and its argument.

CMP.14:5.4 - Include an observed effect of a pending call

An initially empty FIFO queue has this history: A calls enqueue(7) at t=1; B calls dequeue() at t=2 and receives 7 at t=3; A has not returned by t=4. Comparing only completed operations would leave a dequeue from an empty queue.

For the comparison, append A’s response at t=5. The sequential order enqueue(7); dequeue() returns 7 is legal. For example, their effects can be placed at t=1.5 and t=2.5, within their call/response intervals. This is a witness for the finite history; it supplies no promise that A will eventually respond in the actual execution.

If there is no enqueue call at all, appending responses cannot invent one: a dequeue returning 7 from the empty queue remains invalid. If A instead returned at t=2 before B called at t=3, the sequential order must keep A before B. Pending-call completion thus preserves both the observed values and the order already imposed by completed calls.

CMP.14:6 - Bias-Annotation

Sequential intuition can hide an interleaving between a read and its use. An atomic-looking API can hide a smaller implementation primitive. A successful retry demonstration can hide the uncertainty introduced by a lost reply or restart. Recover the actual transitions and observations before assigning the result of a simpler model to them.

CMP.14:7 - Conformance Checklist

• The combined result includes the intermediate observations and eventual responses its user needs.
• The model states atomicity, visibility, communication and admitted environment changes where they affect the argument.
• Initial conditions and each relevant component or environment step support the shared invariant or protocol relation.
• A proposed repair changes the offending interaction and its general transition family.
• Progress uses named scheduling, delivery and failure assumptions; a finite timeout has its own qualified outcome.
• A replacement preserves the observations and progress required by its receiving context, with physical realization checked where that correspondence matters.

CMP.14:8 - Common Anti-Patterns and How to Avoid Them

CMP.14:9 - Consequences

The reader can construct an interaction protocol, locate a failed order, and explain which whole-computation property follows. An invariant, counterexample or progress argument supports division of algorithmic work while exposing the assumptions shared across components.

Coordination can add waiting, retries, retained state or stronger primitives. Sometimes changing the required observation admits a cheaper useful composition. The improvement is conditional on the receiving computation accepting that changed result.

CMP.14:10 - Architectural Rationale

Mathematical composition supplies an operation for combining descriptions. Computational composition must also establish how the resulting process runs and what other processes can observe. Interference makes a component’s admissible context part of its meaning.

The counter, retry and resource-order cases construct three different repairs: conditional atomic change, identity across repeated communication, and removal of cyclic acquisition. Their shared method is to expose the missing interaction, construct the coordinating steps and retain separate arguments for allowed histories and progress. Modeling a working Method with these operations can sharpen a methodological comparison, but the modeled operations still need a justified correspondence to the actual work.

CMP.14:11 - SoTA-Echoing

How should local computations be combined without losing the required whole behavior? Adopt the separation of state/action description, refinement, progress and environment-dependent composition in Lamport’s A Science of Concurrent Programs, chapters 3, 4, 6 and section 8.2. It supports :4.2–4.6. Its composition discussion exposes the circularity of proving each component’s eventual success by assuming the other’s. A direct global invariant remains a serious simpler choice for small interacting systems; a component proof becomes useful when its explicit environment assumptions reduce repeated reasoning. The accepted cost is recovering those assumptions. Changes in observed behavior or progress premises reopen the choice.

When an abstract atomic object must replace a concurrent implementation, adapt the composition-sensitive account in Oliveira Vale, Shao and Chen. It relates linearizability, locality and observational refinement through explicit composition operations. This sharpens :4.1 and :4.6: ask which context can observe the replacement, rather than checking final values alone. A short history/linearization-point argument is sufficient for :5.1; the richer algebra is useful when it reduces actual composition-proof work. It does not automatically preserve progress or supply an implementation. A new interaction context can reverse the choice.

Which interference may a component assume? Adopt the memory-model parameterization demonstrated by Lahav and colleagues’ rely/guarantee treatment of causally consistent shared memory as a boundary on :4.2–4.3. Sequential interleaving is a convenient comparator, while weaker visibility needs a compatible semantics and reasoning rules. Retaining the simpler model is justified when the implementation supplies its conditions. Otherwise synchronization, the algorithm or the claimed observation must change; relabeling the old proof leaves the gap.

When restart is admitted, adapt the explicit crash-aware observation in Linearizability with Crashes for :4.2 and :5.2. A no-crash history can omit the retained-state distinction that recovery needs. A durable coordination protocol accepts persistence and recovery costs; accepting an uncertain result or an idempotent effect may be a cheaper suitable rival. The framework distinguishes forms of crash-aware correctness, rather than making every retry protocol equivalent. Change the failure model or the effect’s location and reconsider the corresponding claim.

CMP.14:12 - Relations

• MATH.17 and MATH.18: supply composition of operations and interpretation between accounts; this method constructs their interacting computational execution.
• CMP.3 and CMP.10: supply dependency scheduling and data representations; interference can change the operations those representations must support.
• CMP.4 and CMP.13: supply exploration and qualified abstraction for the composed state or trace system.
• CMP.12: supplies interpretation and behavior-preserving translation when the component’s executable description changes.
• C.29.2 and C.29.3: supply computational formulation and realization, including whether the modeled primitives and resource conditions are available.
• C.11.DUA: governs the worth of stronger analysis or testing for the proposed use.

CMP.14:End

CMP.15 - Compose Independent Extensions of Data Variants and Operations

Type: Method Status: Stable Normativity: Normative

CMP.15:1 - Problem frame

Use this when different contributors must add new forms of data and new operations on those forms without repeatedly changing one another’s modules. An expression language may gain a binding construct while an independently developed analysis gains an operation for finding free variables. Each addition works with the old core; using the analysis on the new construct still needs a meaning and an implementation.

Start by choosing the combinations the receiving application must support. Find the first required combination whose implementation is absent or whose selection is unclear, and provide the joining contribution that knows both additions. The useful result is a composed set of operations with explicit coverage, selection rules and preservation conditions. A small composition can be assembled and examined directly; a promise about arbitrary future additions requires stronger interfaces and checking.

This method concerns computational data variants and operations. The reader can follow a recursive function and distinguish a data constructor from an operation that processes it. CMP.12 explains how to derive an interpretation and its correspondence with the intended meaning. The construction here keeps independently supplied additions composable; it does not require the reader to know object algebras or a particular extension system beforehand.

Keep a closed representation and ordinary functions when one owner can maintain the required cases affordably. If only the data variants change, methods attached to those variants may suffice. If only the operations change, functions over a stable closed data type may suffice. Independent extension on both axes earns its additional machinery when those simpler arrangements obstruct actual changes.

CMP.15:2 - Problem

How can independently added data variants and operations be used together while preserving established combinations, detecting unsupported or conflicting combinations, and keeping the cost of extension bounded?

A new data variant and a new operation create a possible intersection that neither author knew. An automatic loader can connect an existing implementation, but that intersection may have no implementation yet. A generic traversal can return a value of the right type while computing the wrong meaning. A new dispatch rule can also redirect an old call without changing any old source file. The construction must address these different failures instead of treating successful registration as sufficient composition.

CMP.15:3 - Forces

CMP.15:4 - Solution

Construct the semantic intersection before relying on the mechanism that binds it. Use the same required combinations to choose a representation, assemble contributions, qualify their guarantees and compare a simpler alternative. CMP.15:5 develops one binding example in executable and typed forms; these are alternative realizations of the method.

CMP.15:4.1 - Select the two extension axes and required combinations

Name the data variants and the operations separately. For an expression language, Literal, Variable, Add and Let are variants; evaluation and free-variable analysis are operations. A variant description gives its fields and their meaning, including which fields contain further expressions and where a name is bound. An operation description gives its inputs, result and intended meaning.

Choose the receiving application before requiring every conceivable combination. An evaluator may accept Let while an exporter intentionally accepts only arithmetic expressions. That restriction can be adequate if inputs are checked before export and the unsupported case is reported. If the exporter promises the full language, the missing Let case is an unfulfilled obligation.

For finite sets of variants V and operations O, let R be the required pairs drawn from O × V. Obtain R from admitted inputs and reachable calls, not just the constructors seen at the roots of sample expressions. An old Add can contain a new Let. An operation can invoke another operation, so its dependencies may enlarge the required set. For mutually recursive operations, continue following these dependencies until no new required pair appears.

A conservative complete set is often cheaper than proving that a difficult pair is unreachable. When reachability depends on arbitrary program behavior, a small collection of successful runs does not settle it. Restrict the admitted input language, require an explicit capability before the call, or retain a checked failure before consequential effects. State which choice bounds the use.

Reuse adequate constructor meanings and operation rules. If these remain unclear, use CMP.12:4.1–4.2 to construct the interpretation; NOT.2 and NOT.3 supply expression structure and meaning when the notation itself is being designed. Return the resulting rules to this composition rather than inferring them from a dispatch key.

CMP.15:4.2 - Assign and provide the joining contribution

A data-extension author supplies the new variant and the operations that the extension promises. An operation-extension author supplies that operation for the variants it promises. For a required intersection unknown to both, one contributor who understands both agreements supplies the missing body. This can be either author or the application’s integrator. The application must have a way to obtain that body; merely naming a future contributor leaves the combination unsupported.

The joining contribution contains an implementation and the grounds for using it: the accepted variant, operation meaning, required context, dependent operations and a case that distinguishes it from a plausible wrong implementation. Place it in a module that can depend on both additions without making either old module depend on its future users. The original contributions remain independently usable on their established cases.

Shared construction can replace many individually written bodies when its law applies. A structural fold, for example, combines results already obtained for children. It is useful when that summary suffices for the operation. Binding, control, object identity or effects can require additional information or a different recursion. Establish what the generic rule preserves before deriving a new intersection from it.

Check whether the implementation environment permits the intended contribution. Some languages restrict implementation of an externally defined interface for an externally defined type. A local wrapper, an explicit object containing the operations, or a contribution maintained by one interface owner can then provide the join. These choices change representation, calling conventions or maintenance; they do not remove the semantic obligation.

When the contributions will be supplied as independently maintained extensions, use SYSE.27 to arrange a reproducible contribution, its dependencies and its support. Bring that obtainable implementation back here. Package availability is necessary for execution but does not establish the meaning of its operations.

CMP.15:4.3 - Derive the new operation from the variant’s meaning

Consider the nonrecursive lexical construct Let(name, value, body). The value is evaluated in the incoming environment; the name is then bound locally while evaluating the body. The binding does not govern occurrences inside its own value expression.

Free-variable analysis returns the names with lexically free occurrences. It is not, in general, the smallest set of external values on which a particular execution depends. For the old forms its rules are:

FV(Literal(k)) = {}
FV(Variable(n)) = {n}
FV(Add(a,b)) = FV(a) union FV(b)

To derive the missing rule, divide the occurrences by field. Every free occurrence in value remains free in the whole Let, because the new binding does not reach that field. In body, the new binding captures free occurrences of its own name; other free occurrences remain free. Therefore:

FV(Let(n,v,b)) = FV(v) union (FV(b) minus {n})

For let x = 2 in x + y, the value contributes no free names and the body contributes {x,y}; removing the body’s bound x leaves {y}. Unioning every child’s result would return {x,y}. Both results are sets of names, so an ordinary result-type check cannot choose between them.

The location of the subtraction matters. For let x = x + 1 in x + y, the x in the value refers to the incoming environment. The whole expression has free names {x,y}. Subtracting x after unioning both fields would incorrectly return only {y}.

For another constructor, repeat this derivation from its rules. A recursive binding has different scope; a branch may require preserving which child is evaluated; a graph analysis may require identity and a fixed-point computation. Use the relevant CMP.12 interpretation or other supplied operation to obtain those facts, then implement the intersection. A common syntax shape alone does not justify copying this Let rule.

CMP.15:4.4 - Bind one applicable body and keep recursion open

Assemble contributions under an explicit selection rule. The simplest rule uses an exact pair (operation, variant). Reject two bodies for the same pair unless the composition explicitly selects one before assembly. Silently letting the last loaded body win makes loading order a semantic decision.

If selection uses subtyping or predicates, determine which bodies apply and how one is chosen. No applicable body means missing support. Several applicable bodies can be acceptable when one is uniquely more specific under the declared rule; incomparable best candidates leave ambiguity. An explicit body for their intersection, a restriction of applicability or an explicit composition-level choice can resolve it. Each repair still needs a semantic justification.

For recursive data, pass recursive requests through the assembled operation. One simple interface is:

run(operation, expression, context):
    body = select(operation, expression.variant)
    return body(run, expression, context)

The body receives run as its recursive entry. Thus an old Add handler can process a Let child using the new body selected by this composition. Calling a private old evaluator from that handler would close recursion over the old cases and defeat the extension. For an algebraic construction that receives already interpreted children, the parameterized algebra performs the corresponding composition during term construction; CMP.15:5.3 shows that alternative.

Connect dependencies between operations in the same manner. If an analysis calls a printer, choose which printer it uses, its required variants and the result it returns. Do not leave that dependency bound to an obsolete private implementation merely because a newer printer is present elsewhere in the application.

Keep the composed selection stable for the execution being qualified. With a copied exact-key table, later additions to a source collection need not alter that table. Shared mutable state inside a handler still can alter behavior. If the application replaces methods during an execution, qualify visibility and interaction through CMP.14 rather than assuming that a successful assembly settles them.

CMP.15:4.5 - Choose checking and binding conditions separately

Choose when contributions become connected and when the required obligations are checked. These are distinct decisions: dynamic composition can carry static constraints, and early registration can still leave semantic errors until execution.

A static realization can express each operation as an implementation of a constructor signature. A term using Let requires that extended signature. An implementation of only the old signature cannot be supplied to it without failing the relevant type requirement. CMP.15:5.3 gives the bodies and the rejected combination. This establishes availability and type compatibility only to the extent enforced by the chosen language; an unchecked cast can conceal the missing obligation. Correctly typed but wrong FV(Let) remains possible.

A dynamic realization can collect explicit bodies, reject conflicts and compare their keys with R before running any handler. Missing pairs then fail during composition rather than halfway through an effectful operation. The check is complete for R; it covers the application only if R covers its reachable uses. Guard calls outside that scope. Loading another extension requires constructing or qualifying another composition.

Keep three failures distinct:

Malformed input, an unbound variable and a language-defined arithmetic error are errors of the represented language or its inputs. A loaded method that is not visible to the running computation is a binding or visibility issue. Diagnose those conditions separately from a missing semantic implementation.

The historical expression problem asks for stronger properties than practical plug-in loading alone, including static type safety and extension without recompiling existing code. Wadler’s formulation supplies those comparison criteria. Use the name as a search cue; state which properties the actual construction achieves.

CMP.15:4.6 - Establish preservation on the promised old uses

Preserve the old meanings as well as the old files. For each established operation, compare which body an old input selects after extension and which dependencies that body invokes. A new, more specific method can redirect an old call in a subtype-based dispatcher. Disallow that override, explicitly retain the earlier selection, or treat it as a behavior change requiring its own correspondence.

For a pure tree interpreter with exact keys, a useful preservation argument is available. Suppose the old keys still select the same bodies, the old expressions contain only old constructors, and primitives, environments and dependent operations retain their meaning. A leaf obtains the same result. At a compound old node, induction gives the same child results, and the unchanged body combines them in the same way. Every finite old expression therefore retains its result. This argument depends on those premises; unchanged source text alone does not prove them.

Test a new form beneath an old constructor as a different obligation. It was not an old expression, so the preservation argument does not establish its new meaning. This case checks whether open recursion reaches the supplied intersection and whether the resulting composition obeys the new rules.

When effects, failures or concurrent replacement matter, use the observations and correspondence from CMP.12 and the interaction method in CMP.14. Preserving a returned number may leave an extra effect or a changed failure observable. Selected tests can expose such differences; a promise for an entire class of executions needs an argument at that scope.

CMP.15:4.7 - Bound the cost and retain the simplest adequate composition

Count the work that the architecture moves as well as the work it removes. Independent authors avoid editing a central list, but someone still writes or derives the required intersections, connects dependencies, diagnoses rejected compositions and supports the result. A generic derivation can reduce the number of bodies; its applicability and exception handling still have a cost.

For an exact-key table with H supplied bodies and Q required pairs, assembly and coverage checking take expected order H + Q dictionary operations and order H table storage. Each recursive dispatch adds an expected constant-time lookup under the hash-table assumptions. Count the bodies separately: free-variable analysis copies or unions sets, and evaluation may copy environments. With N visited nodes and at most K names in intermediate sets, straightforward set operations can cost order N K, rather than merely N. Large-integer arithmetic and representation conversion have their own costs.

A static representation can move selection into compilation or construct terms through operation dictionaries, but it can introduce interface complexity, generated instances, code size, specialization and build dependencies. A dynamic representation adds assembly, visibility, possible runtime failures and often indirect calls. Measure or derive the relevant total for the actual workload; neither label guarantees the cheaper execution.

Compare a closed alternative using the same required cases. For four stable variants, two fixed operations and one maintainer, two exhaustive functions may be easier to understand and maintain than a registry and its coverage description. They still need the correct Let rule. Conversely, repeatedly editing another team’s module for each new operation or variant gives independent composition a concrete benefit. Use SYSE.23 when the broader engineering choice needs comparison of anticipated changes and their complete cost.

Stop with the smallest construction that provides the receiving application’s operations under its admitted inputs and extension conditions. Retain explicit unsupported cases rather than implying a complete open world. Reopen the selection when a new required pair, operation dependency, binding rule, loading condition or change workload invalidates it.

CMP.15:5 - Archetypal Grounding

CMP.15:5.1 - Find the absent intersection before connecting it

Start with integer expressions Literal, Variable and Add, together with evaluation. Contributor A adds nonrecursive lexical Let and its evaluation. Contributor B independently adds free-variable analysis for the original forms.

If the application accepts all four variants for both operations, seven available bodies leave one required pair absent. The joining contributor derives the eighth body as in CMP.15:4.3. For let x = 2 in x + y, evaluation under y = 4 is 6 and free-variable analysis is {y}.

Changing the question to evaluation alone makes the seven-body composition sufficient for that operation. This is a legitimate narrower use, not a repair of the still-unsupported analysis. Changing the binding to recursive Let reopens both its evaluation and free-variable rule.

CMP.15:5.2 - Assemble and run the contributions with exact keys

The following Python 3 example is a complete small realization for finite, well-formed expression trees. Tuple tags stand for already parsed constructors. It has no parser, effects, method replacement or static type checking. Environments are maps from names to integers; missing names raise UnboundName. Set-valued results are compared by membership.

Each contribution is a sequence of explicit bodies. The assembler copies them into a private table, rejects repeated keys and checks any declared required pairs before invoking a handler.

class MissingCase(Exception):
    pass

class MissingCoverage(Exception):
    pass

class ConflictingCase(Exception):
    pass

class UnboundName(Exception):
    pass

def lookup(environment, name):
    if name not in environment:
        raise UnboundName(name)
    return environment[name]

def compose(*contributions, required=()):
    bodies = {}
    for contribution in contributions:
        for operation, variant, body in contribution:
            key = (operation, variant)
            if key in bodies:
                raise ConflictingCase(key)
            bodies[key] = body
    missing = set(required) - bodies.keys()
    if missing:
        raise MissingCoverage(frozenset(missing))

    def run(operation, expression, environment=None):
        key = (operation, expression[0])
        if key not in bodies:
            raise MissingCase(key)
        context = {} if environment is None else environment
        return bodies[key](run, expression, context)
    return run

base = [
    ("eval", "lit", lambda r, e, env: e[1]),
    ("eval", "var", lambda r, e, env: lookup(env, e[1])),
    ("eval", "add",
     lambda r, e, env: r("eval", e[1], env) + r("eval", e[2], env)),
]
data_extension = [
    ("eval", "let",
     lambda r, e, env:
         r("eval", e[3], {**env, e[1]: r("eval", e[2], env)})),
]
operation_extension = [
    ("free", "lit", lambda r, e, env: set()),
    ("free", "var", lambda r, e, env: {e[1]}),
    ("free", "add",
     lambda r, e, env: r("free", e[1]) | r("free", e[2])),
]
joining_contribution = [
    ("free", "let",
     lambda r, e, env: r("free", e[2]) | (r("free", e[3]) - {e[1]})),
]
wrong_join = [
    ("free", "let",
     lambda r, e, env: r("free", e[2]) | r("free", e[3])),
]

old = ("add", ("lit", 2), ("var", "x"))
term = ("let", "x", ("lit", 2),
        ("add", ("var", "x"), ("var", "y")))
required = {
    (operation, variant)
    for operation in ("eval", "free")
    for variant in ("lit", "var", "add", "let")
}

baseline = compose(base)
partial = compose(base, data_extension, operation_extension)
assert baseline("eval", old, {"x": 3}) == 5
assert partial("eval", term, {"y": 4}) == 6

try:
    partial("free", term)
except MissingCase as error:
    assert error.args[0] == ("free", "let")
else:
    raise AssertionError("The absent body was not reported.")

try:
    compose(base, data_extension, operation_extension, required=required)
except MissingCoverage as error:
    assert error.args[0] == frozenset({("free", "let")})
else:
    raise AssertionError("Coverage checking admitted an absent pair.")

incorrect = compose(base, data_extension, operation_extension,
                    wrong_join, required=required)
assert incorrect("free", term) == {"x", "y"}

complete = compose(base, data_extension, operation_extension,
                   joining_contribution, required=required)
assert complete("free", term) == {"y"}
assert complete("eval", term, {"y": 4}) == 6
assert complete("eval", old, {"x": 3}) == baseline("eval", old, {"x": 3})

embedded = ("add", term, ("var", "x"))
assert complete("eval", embedded, {"x": 10, "y": 4}) == 16
assert complete("free", embedded) == {"x", "y"}

outer_name = ("let", "x",
              ("add", ("var", "x"), ("lit", 1)),
              ("add", ("var", "x"), ("var", "y")))
assert complete("eval", outer_name, {"x": 10, "y": 4}) == 15
assert complete("free", outer_name) == {"x", "y"}

shadowed = ("let", "x", ("lit", 2),
            ("let", "x", ("add", ("var", "x"), ("lit", 1)),
             ("add", ("var", "x"), ("var", "y"))))
assert complete("eval", shadowed, {"y": 4}) == 7
assert complete("free", shadowed) == {"y"}

try:
    compose(base, data_extension, operation_extension,
            joining_contribution, wrong_join, required=required)
except ConflictingCase as error:
    assert error.args[0] == ("free", "let")
else:
    raise AssertionError("Two bodies for one pair were accepted.")

The absent pair can be found at use or, when required is supplied, during assembly. The wrong join passes coverage and returns a set, yet fails the semantic requirement. Supplying both joins fails before any handler runs. These are three different outcomes.

An operation can also depend on another operation rather than only on its own recursive calls. Suppose IsClosed(e) asks whether FreeVariables(e) is empty. For each admitted variant, its body calls the assembled free-variable operation: lambda r, e, env: not r("free", e). The required set for this use contains both IsClosed and FreeVariables on all four reachable variants; evaluation is unnecessary. Supplying every IsClosed body without FreeVariables(Let) must therefore fail coverage before execution. This dependency closure is chosen from the bodies’ calls; the assembler does not infer it.

For let x = 2 in x, the correct free-variable join returns the empty set, so IsClosed returns true. The wrong union returns {x}, so IsClosed returns false even though all required bodies are present. Both the missing dependency and the wrong meaning propagate into the receiving operation. Calling a private older analysis would evade the selected join instead of repairing either failure.

The embedded case sends a new Let through an unchanged Add body. Its sibling variable x still reads the outer value 10 because the Let handler extends a copy of its incoming environment. The outer_name and shadowed cases distinguish the binding rules: the value expression sees the incoming binding, while the body sees the new one.

For this grammar, all recursive calls stay within the declared eight pairs. Coverage checking therefore settles absence for these two operations over well-formed trees of the four constructors. It establishes neither the meaning of a body nor static type safety. Arbitrary supplied Python functions could mutate external state or call other operations; those would need an enlarged dependency account and preservation conditions. The induction in CMP.15:4.6, rather than the finite assertions alone, explains preservation for all old trees under the stated pure semantics.

CMP.15:5.3 - Express the same obligation through a typed signature

A static alternative represents a term by its use of constructor operations. Instead of first constructing a stored tree and then dispatching on it, the term receives an algebra: a collection of constructor functions whose common result type R is chosen by the interpretation.

The notation below is typed pseudocode. Base<R> and LetPart<R> are records of functions; & requires both sets of fields. It specifies the constraints a realization must enforce, not a claim about compilation by a particular compiler.

Base<R> = {
    literal: Integer -> R,
    variable: Name -> R,
    add: (R, R) -> R
}
LetPart<R> = {
    let_: (Name, R, R) -> R
}

old<R>(a: Base<R>): R =
    a.add(a.literal(2), a.variable("x"))

extended<R>(a: Base<R> & LetPart<R>): R =
    a.let_("x", a.literal(2),
           a.add(a.variable("x"), a.variable("y")))

withLet<R>(base: Base<R>, part: LetPart<R>):
        Base<R> & LetPart<R> =
    {literal = base.literal, variable = base.variable,
     add = base.add, let_ = part.let_}

For evaluation, choose R = Environment -> Integer. The result of constructing each subexpression is a function awaiting its environment. This delays lookup until the expression’s binding context is known. Let extend(env,n,k) return a new environment that maps n to k and otherwise agrees with env.

evalBase: Base<Environment -> Integer> = {
    literal = k -> (env -> k),
    variable = n -> (env -> lookup(env,n)),
    add = (f,g) -> (env -> f(env) + g(env))
}
evalLet: LetPart<Environment -> Integer> = {
    let_ = (n,v,b) -> (env -> b(extend(env,n,v(env))))
}

For free-variable analysis, choose R = Set<Name>:

freeBase: Base<Set<Name>> = {
    literal = k -> {},
    variable = n -> {n},
    add = (a,b) -> a union b
}
freeLet: LetPart<Set<Name>> = {
    let_ = (n,v,b) -> v union (b minus {n})
}

old(freeBase) = {"x"}
extended(withLet(freeBase, freeLet)) = {"y"}
extended(withLet(evalBase, evalLet))({y = 4}) = 6

The expression extended(freeBase) lacks the required let_ field and is rejected in a realization that enforces these record constraints. The operation author can keep freeBase unchanged; the joining contributor supplies freeLet, and the application assembles them with withLet. A wrong freeLet returning v union b has the required type, demonstrating the same semantic limit as the dynamic example.

Here withLet copies only the old constructor functions and supplies one new field, so it does not silently override an old field. A richer composition with overlapping signatures needs its own explicit selection rule. Interface union alone does not combine implementations. The chosen language must also support any promised separate compilation; satisfying these mathematical signatures does not establish how a build system handles dependencies.

This representation suits operations expressible through the supplied constructor algebra. Context-sensitive evaluation works because its result is an environment-taking function. An operation needing raw child identity, multiple interacting analyses or cyclic data can need richer results, additional operations or a different representation. Previously serialized trees require a reader that recognizes the extended syntax and applies the right constructor functions; adding LetPart does not update an old parser.

CMP.15:5.4 - Stop when independent extension has no useful payoff

Suppose a private calculator has the same four constructors and two operations, and one maintainer changes them together. A closed tagged data type with an exhaustive evaluation function and an exhaustive free-variable function makes every required case visible. Adding Let means editing those two functions, deriving exactly the same binding rule and checking the new cases.

That arrangement loses independent addition without edits, but the application does not require it. A registry, separate contribution interfaces and loading rules would add work without removing an actual obstacle. Keep the closed design.

If a separately maintained analyzer must later add an operation while another team extends the expression language, repeat the comparison. The new independent change requirement can justify interfaces and an external joining module. It still leaves that module’s semantic body to be supplied.

CMP.15:6 - Bias-Annotation

The worked construction favors explicit finite syntax and pure operations because their dispatch and preservation can be inspected directly. Opaque foreign data, cyclic structures, effects and live method replacement need additional representation or interaction arguments. Do not transfer the tree induction to them solely because their implementation also uses handlers.

The method also makes integration work visible. Contributors who each test only their own extension can underestimate the cost of intersections that appear only in the receiving application. Conversely, anticipated openness can be overvalued when stable requirements make a closed representation adequate.

CMP.15:7 - Conformance Checklist

• The data variants, operation meanings and admitted receiving uses determine the required combinations, including nested forms and dependent operations.
• Every required new intersection has an obtainable body or an explicit unsupported-use boundary; its supplier understands both sides.
• Generic derivation is justified by the operation’s meaning, with binding, control or identity distinctions retained where material.
• The composition defines selection, reports missing support and rejects or resolves conflicts without accidental loading-order semantics.
• Recursive and dependent calls reach the implementation selected for the composition.
• Unchanged sources, separate checking and compilation, early coverage and behavior preservation have distinct stated grounds.
• A semantic counterexample can distinguish a present, uniquely selected but wrong body from a correct one.
• Old-use preservation covers the promised observations and assumptions; a new form below an old constructor is exercised separately.
• The full cost is compared with an adequate closed alternative, and a changed required pair or binding condition has a clear return.

CMP.15:8 - Common Anti-Patterns and How to Avoid Them

CMP.15:9 - Consequences

Independent additions can remain useful without edits to their original modules, while the receiving application chooses the combinations it supports. Missing and conflicting combinations become diagnosable at a stated point. Semantic joining work has an explicit location instead of being hidden in a loader or left to each user.

The price is additional interfaces, composition and qualification. Static checking can move some failures earlier; dynamic composition can admit later choices. Neither removes the need to establish the operation’s meaning. A closed design remains a valid result when its total change cost is lower for the actual use.

CMP.15:10 - Architectural Rationale

The two-axis construction separates knowledge that can evolve independently from knowledge that must meet. A variant author knows the new form’s structure; an operation author knows the analysis or transformation. Their future intersection becomes implementable when one contribution can use both. Keeping that contribution outside the old modules preserves their original dependency direction without pretending that the new meaning follows automatically.

The receiving composition bounds the promise. Requiring every possible pair would overstate some applications and make useful partial support expensive. Checking only examples would understate applications that admit arbitrary trees. The required set and its recursion dependencies connect those alternatives to the actual input language.

Exact-key dispatch is the simplest realization in the executable example because it makes absence, conflict and preservation easy to inspect. Subtyping and algebraic interfaces can remove other burdens but require their own resolution or typing conditions. The method therefore selects guarantees independently of binding time.

The semantic rule remains necessary under every realization. The wrong free-variable body passes ordinary type, presence and uniqueness checks in both examples. The explicit derivation and binding variations supply what those checks omit. CMP.12 remains the source of interpretation construction; this method organizes independently supplied extensions of that construction. CMP.14 becomes necessary when effects or changing visible methods alter the composed observations.

CMP.15:11 - SoTA-Echoing

How can both axes extend while missing capabilities remain visible? For a language representable through constructor functions, adapt object algebras and typed tagless-final interpretation as the static line used in CMP.15:5.3. Oliveira and Cook, 2012, sections 5 and 7, supplies parameterized constructor signatures and explicit combination of implementations; Kiselyov, sections 2.2–2.3, exposes the missing interpretation through constraints and treats deserialization separately. A closed data type with exhaustive functions is the serious cheaper alternative when independent changes are unnecessary. The selected construction removes obligatory edits to a central case definition while retaining explicit new bodies. Reconsider it when raw structure access, cyclic data or interface complexity defeats the chosen representation.

Can later composition retain static guarantees? Adapt the separation of binding time from checking time in modern compositional programming. Ye, Sun and Oliveira, 2024, develops operation dependencies and explicitly supplied extensions for imperative analyses. Sun, Huang and Oliveira, 2025, sections 3.4 and 6.6, combines dynamic inheritance through merging with static checking and an implementation of separate compilation through interfaces. These are current research alternatives to treating every late-bound registry as the only open design. They motivate the independent guarantees in CMP.15:4.5; their language proofs do not prove arbitrary user operations correct, and the latter paper distinguishes the core formalization from further implementation features. Reopen a concrete realization when tool support, required effects or compilation obligations differ from those the chosen language supplies.

How should overlapping bodies be resolved? Adopt explicit resolution rather than import-order selection in CMP.15:4.4. The Julia method documentation supplies a practical comparator: incomparable applicable methods need a disambiguating method, and newly defined methods have execution-visibility conditions. The exact-key table deliberately uses the simpler rule of rejecting duplicates. Xu, Huang and Oliveira, 2025, supplies a serious research alternative to rejecting all overlap: apartness and guarded subtyping permit overlap that remains distinguishable at use. Those mechanisms still require supplied behavior. Compare again when useful compositions are rejected by the simpler rule or when a new method changes an established call.

How does an independent join become available? Adapt explicit extension modules from the current Julia package-extension mechanism as a dynamic realization of CMP.15:4.2 and CMP.15:4.5: dependency triggers load already authored code. This improves availability; it does not construct a missing semantic intersection. A static application assembly remains a cheaper alternative for a fixed set. The Rust coherence rules supply a limiting comparator: foreign-interface and foreign-type combinations are restricted, so a wrapper, explicit dictionary or owner-supported contribution may be necessary. Reopen the packaging choice when ownership, compatibility or visibility changes. These sources describe mechanisms, not production guarantees for an arbitrary assembled application.

CMP.15:12 - Relations

• CMP.12: use its interpretation rules and correspondence argument when deriving a body or qualifying preserved behavior; return those results to the chosen composition.
• CMP.14: use its interaction construction when handlers share state, produce effects or change visibility during execution. Pair coverage alone leaves those observations unresolved.
• CMP.2 and CMP.10: supply recursive construction and representation cost analysis when the extension changes decomposition, storage or access.
• NOT.2, NOT.3 and NOT.4: supply expression structure, meaning and permitted transformations when a notation is being designed; the computational implementation here consumes those rules.
• SYSE.23: compares the engineering value and full cost of changeability when choosing an open architecture.
• SYSE.27: supplies the reproducible extension contribution and support arrangement when separately maintained modules are needed; the joining semantics remains the computational work described here.

CMP.15:End