In computer science, run-time algorithm specialization is a methodology for creating efficient algorithms for costly computation tasks of certain kinds. The methodology originates in the field of automated theorem proving and, more specifically, in the Vampire theorem prover project.
Contents
- Difference from partial evaluation
- Specialization with compilation
- Data and algorithm specialization
- References
The idea is inspired by the use of partial evaluation in optimising program translation. Many core operations in theorem provers exhibit the following pattern. Suppose that we need to execute some algorithm
The specialized algorithm may be more efficient than the generic one, since it can exploit some particular properties of the fixed value
Difference from partial evaluation
The key difference between run-time specialization and partial evaluation is that the values of
There is also an important technical difference. Partial evaluation is applied to algorithms explicitly represented as codes in some programming language. At run-time, we do not need any concrete representation of
Specialization with compilation
The specialized algorithm has to be represented in a form that can be interpreted. In many situations, usually when
Instructions of the abstract machine can usually be represented as records. One field of such a record stores an integer tag that identifies the instruction type, other fields may be used for storing additional parameters of the instruction, for example a pointer to another instruction representing a label, if the semantics of the instruction requires a jump. All instructions of a code can be stored in an array, or list, or tree.
Interpretation is done by fetching instructions in some order, identifying their type and executing the actions associated with this type. In C or C++ we can use a switch statement to associate some actions with different instruction tags. Modern compilers usually compile a switch statement with integer labels from a narrow range rather efficiently by storing the address of the statement corresponding to a value
Data-and-algorithm specialization
There are situations when many instances of