Tree rewrite with typed variables can be used to represent many tree transformations in a more compact form than systems with untyped variables. By building on the work of Eduardo Pelegri-Llopart, it is possible to generate linear-time optimal solutions to SET-REACHABILITY -- a generalization of REACHABILITY with a possibly infinite goal set -- for a useful class of typed rewrite systems. The algorithms developed can also handle some untyped systems that are not in BURS, such as systems with rules of the form X --> a(X).
An experiment involving a rewrite system for instruction selection for the Motorola 68000 produced table sizes an order of magnitude larger than those produced by an untyped rewrite system for the same task. It is not clear whether this table size can be limited, or if it is an inherent cost of the power given by types. Although discouraging for the instruction selection application, the table sizes are small enough (under 100k bytes) that the techniques may be useful for smaller applications, or in cases where the added expressability of typed variables outweighs the size explosion of the tables.