Definition

Proof

To prove: This is equivalent to the rule s1 = S'(a1), S' being a synthetic node inserted into the input tree.

A concrete example makes the formal statement more comprehensible. Suppose we have the rules:

int = INTEGER_LITERAL { /* Use LDC, BIPUSH, ICONST */ }
long = int; // No code necessary, the JVM will widen the int to a long
object = int { /* new Integer(int) */ }
string = object { /* object.toString() */ }

• The stages of a BURM transformation are the nodes in the tree, so S is the INTEGER_LITERAL node.
• The int state is produced directly by pattern-matching S and has no antecedents.
• The long state is a transitive closure (INTEGER_LITERAL = int = long) and has no antecedents, long being considered identical to int.
• The object state has antecedent state int.
• The string state has antecedent state object.

int = INTEGER_LITERAL { /* as before }
object = TO_OBJECT(int) { /* new Integer(int) */ }
string = TO_STRING(object) { /* object.toString() */ }

What does it mean to be "equivalent" in the context of a BURM?

1. The labeler must recognize the same sequence of rules and compute the same costs.
2. The reducer must run the same rules, in the same order.

1. Cost computations: assume that the int rule has cost 1, the object=int rule has cost 5, and the string = object rule has cost 2. These costs would be assigned to the corresponding cast nodes: TO_OBJECT(int) costs 5, TO_STRING(object) costs 2, INTEGER_LITERAL still costs 1. The labeler computes a state/stage pair's cost to be its intrinsic cost plus the cost of its operand(s): the cost of the TO_OBJECT stage is 6 (its intrinsic cost, 5, plus the unit cost of its int operand), and the cost of the string stage is 8 (its intrinsic cost, 2, plus the cost (6) of its object operand).

   The costs of the antecedent rules add up in the same way: the cost of the int state is 1, the cost of the object state is 5 + 1, and the cost of the string state is 2 + 6. Note that each state only needs to obtain the (aggregate) cost of its immediate antecedent.

2. In order for the labeler to find all possible antecedent-dependent closures, the BURG must construct a partial ordering of the states that have antecedents and emit the stage's closure computations in the correct order.

   The partial order starts with a state, sPrime, that has no antecedents. There must be at least one such state per stage. Any states whose antecedent is sPrime are next, then their antecedents, and so on.

   This is the way that the BURM's labler works; it begins with a pattern-matching rule, which has no antecedents. Then it finds transformational rules that depend on that primary state. For any transformational rule that may run, the labeler finds additional transformational rules, sequentially constructing a set of orderings of the set of states.

   This set is ambiguous, in that it may contain cycles; the BURM guards against cycles by using the pigeonhole principle to assert that there are no more than k-1 possible antecedents at any stage; if the reducer requests additional antecedent states, then the ordering contains cycles.

   TODO: The labeler can detect these cycles as well, and it should, since it has more information available for diagnostics.

3. Reduce-time behavior requires that we run the correct rules in the correct order. Again, the proof is constructive. Using our example states and rules:

   The string state, which is our overall goal, notes that its antecedent is object. The string rule goes onto a rule stack, and the reducer investigates object's antecedents.

   The object state's antecedent is int. The object goes onto the rule stack, and the reducer investigates int's antecedents.

   int has no antecedent, so the reducer "reduces" int by running its rule, pops the object rule and "reduces," and finally pops the string rule and "reduces" to the goal state.

Corollary

This is nothing more than an observation that the Principle of Optimality, a basic Dynamic Programming concept, holds for antecedent states because they're equivalent to a mutated tree, as demonstrated above.