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.