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.
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 in a situation where a value of is fixed for potentially many different values of . In order to do this efficiently, we can try to find a specialization of for every fixed , i.e., such an algorithm , that executing is equivalent to executing .
The specialized algorithm may be more efficient than the generic one, since it can exploit some particular properties of the fixed value . Typically, can avoid some operations that would have to perform, if they are known to be redundant for this particular parameter .
In particular, we can often identify some tests that are true or false for , unroll loops and recursion, etc.
There are situations when many instances of are intended for long-term storage and the calls of occur with different in an unpredictable order.
For example, we may have to check first, then , then , and so on.
In such circumstances, full-scale specialization with compilation may not be suitable due to excessive memory usage.
However, we can sometimes find a compact specialized representation
for every , that can be stored with, or instead of, .
We also define a variant that works on this representation
and any call to is replaced by , intended to do the same job faster.
- A. Riazanov and A. Voronkov, "Efficient Checking of Term Ordering Constraints", Proc. IJCAR 2004, Lecture Notes in Artificial Intelligence 3097, 2004 (compact but self-contained illustration of the method)
- A. Riazanov and A. Voronkov, Efficient Instance Retrieval with Standard and Relational Path Indexing, Information and Computation, 199(1-2), 2005 (contains another illustration of the method)
- A. Riazanov, "Implementing an Efficient Theorem Prover", PhD thesis, The University of Manchester, 2003 (contains the most comprehensive description of the method and many examples)