Run-time algorithm specialization

In <a href="/facts/Computer_science/lN3pEyPz">computer science</a>, 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 <a href="/facts/Automated_theorem_proving/vKGvuKFI">automated theorem proving</a> and, more specifically, in the <a href="/facts/Vampire_theorem_prover/BIBnqWVn">Vampire theorem prover</a> project.
The idea is inspired by the use of <a href="/facts/Partial_evaluation/cSBKhRPo">partial evaluation</a> in optimising program translation. 
Many core operations in theorem provers exhibit the following pattern.
Suppose that we need to execute some algorithm 
 
 
 
 
 
 a
 l
 g
 
 
 (
 A
 ,
 B
 )
 
 
 {\displaystyle {\mathit {alg}}(A,B)}
 
 in a situation where a value of 
 
 
 
 A
 
 
 {\displaystyle A}
 
 is fixed for potentially many different values of 
 
 
 
 B
 
 
 {\displaystyle B}
 
. In order to do this efficiently, we can try to find a specialization of 
 
 
 
 
 
 a
 l
 g
 
 
 
 
 {\displaystyle {\mathit {alg}}}
 
 for every fixed 
 
 
 
 A
 
 
 {\displaystyle A}
 
, i.e., such an algorithm 
 
 
 
 
 
 
 a
 l
 g
 
 
 
 A
 
 
 
 
 {\displaystyle {\mathit {alg}}_{A}}
 
, that executing 
 
 
 
 
 
 
 a
 l
 g
 
 
 
 A
 
 
 (
 B
 )
 
 
 {\displaystyle {\mathit {alg}}_{A}(B)}
 
 is equivalent to executing 
 
 
 
 
 
 a
 l
 g
 
 
 (
 A
 ,
 B
 )
 
 
 {\displaystyle {\mathit {alg}}(A,B)}
 
.
The specialized algorithm may be more efficient than the generic one, since it can exploit some particular properties of the fixed value 
 
 
 
 A
 
 
 {\displaystyle A}
 
. Typically, 
 
 
 
 
 
 
 a
 l
 g
 
 
 
 A
 
 
 (
 B
 )
 
 
 {\displaystyle {\mathit {alg}}_{A}(B)}
 
 can avoid some operations that 
 
 
 
 
 
 a
 l
 g
 
 
 (
 A
 ,
 B
 )
 
 
 {\displaystyle {\mathit {alg}}(A,B)}
 
 would have to perform, if they are known to be redundant for this particular parameter 
 
 
 
 A
 
 
 {\displaystyle A}
 
. 
In particular, we can often identify some tests that are true or false for 
 
 
 
 A
 
 
 {\displaystyle A}
 
, unroll loops and recursion, etc.

Run-time algorithm specialization open-in-new

Run-time algorithm specialization