Специализация алгоритмов во время выполнения: повышение эффективности вычислений в задачах, вдохновленное теоремой доказывания и частичной оценкой. Оптимизация!
Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Введение
В информатике специализация алгоритмов во время выполнения — это методология создания эффективных алгоритмов для ресурсоемких вычислительных задач определенного типа. Эта методология берет начало в области автоматического доказательства теорем и, в частности, в проекте автоматического доказателя теорем Vampire. Идея вдохновлена использованием частичной оценки для оптимизации трансляции программ. Многие основные операции в автоматических доказателях теорем демонстрируют следующий шаблон. Предположим, что нам необходимо выполнить некоторый алгоритм в ситуации, когда значение некоторой переменной фиксировано для потенциально многих различных значений другой переменной. Чтобы сделать это эффективно, мы можем попытаться найти специализацию этого алгоритма для каждого фиксированного значения, то есть такой алгоритм, что выполнение специализированного алгоритма эквивалентно выполнению исходного. Специализированный алгоритм может быть более эффективным, чем общий, поскольку он может использовать определенные свойства фиксированного значения. Как правило, можно избежать некоторых операций, которые исходный алгоритм должен был бы выполнять, если известно, что они избыточны для данного параметра. В частности, мы часто можем определить тесты, которые истинны или ложны для этого значения, развернуть циклы и рекурсию и т.д.
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.
Отличие от частичной оценки
Ключевое различие между специализацией во время выполнения и частичной оценкой заключается в том, что значения, относительно которых выполняется специализация, неизвестны статически, поэтому специализация происходит во время выполнения. Существует также важное техническое различие. Частичная оценка применяется к алгоритмам, явно представленным в виде кода на каком-либо языке программирования. Во время выполнения нам не требуется какое-либо конкретное представление . Мы должны лишь представить его, когда программируем процедуру специализации. Это также означает, что мы не можем использовать универсальные методы для специализации алгоритмов, что обычно характерно для частичной оценки. Вместо этого, нам необходимо программировать процедуру специализации для каждого конкретного алгоритма. Важное преимущество такого подхода заключается в том, что мы можем использовать мощные ad hoc приемы, использующие особенности и представления и , которые недоступны универсальным методам специализации.
The key difference between run time specialization and partial evaluation is that the values of on which is specialised are not known statically, so the specialization takes place at run time. 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 We only have to imagine when we program the specialization procedure. All we need is a concrete representation of the specialized version This also means that we cannot use any universal methods for specializing algorithms, which is usually the case with partial evaluation. Instead, we have to program a specialization procedure for every particular algorithm An important advantage of doing so is that we can use some powerful ad hoc tricks exploiting peculiarities of and the representation of and , which are beyond the reach of any universal specialization methods.