While the specification for stack code was functional, i.e. there was one unique translation for each abstract syntax term, the combined specification allows more than one translation.
The combined specification is correct in the sense that each possible rule selection results in correct target code. It is also complete in the sense that for each argument term there is a possible selection of rules that emits code for the term. Hence, it should suffice as a specification of code generation.
This is the case if we use cost-driven rule selection.
Cost-driven rule selection is performed for predicates that are declared as being of the category choice. Rules of such predicates may be augmented by cost values. A rule is given a cost by providing a specification of the form
When evaluating invocations of choice predicates, conceptually all possible sequences of rule applications are considered. The total cost of a sequence of rule applications is the sum of the costs of all rules. The sequence of rule applications that leads to the minimal total cost is actually used for evaluation (if there are several best sequences one of them is taken).