Run-time algorithm specialization

Run-time algorithm specialization is a methodology in computer science for building efficient algorithms for computationally costly tasks, originating in the field of automated theorem proving and specifically in work on the Vampire theorem prover project. The idea is inspired by partial evaluation techniques used in optimizing program translation. Many core operations in theorem provers take the form of an algorithm that must run repeatedly with one argument held fixed while a second argument varies, and the methodology constructs a specialized version of the algorithm for each fixed value of the first argument, so that running the specialized version on the varying argument produces the same result as the general algorithm while skipping operations that would otherwise be redundant for that fixed value.