Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Содержание
Введение
В информатике, анализ строгости относится к любому алгоритму, используемому для доказательства того, что функция в не строгом функциональном языке программирования строга в одном или нескольких своих аргументах. Эта информация полезна для компиляторов, потому что строгие функции могут быть скомпилированы более эффективно. Таким образом, если функция доказана строгой (с помощью анализа строгости) во время компиляции, ее можно компилировать, чтобы использовать более эффективную конвенцию вызова без изменения значения окружающей программы. Обратите внимание, что функция f расходится, если она возвращает : оперативно, это означает, что f либо вызывает ненормальное завершение закрывающей программы (например, сбой с сообщением об ошибке), либо она бесконечно циркулирует. Понятие "дивергенции" имеет значение, потому что строгая функция - это та, которая всегда расходится, когда дается аргумент, который расходится, тогда как ленивая (или не строгая) функция - это та, которая может или не может расходиться, когда дается такой аргумент. Анализ строгости пытается определить "свойства дивергенции" функций, что позволяет определить некоторые строгие функции.
In computer science, strictness analysis refers to any algorithm used to prove that a function in a non strict functional programming language is strict in one or more of its arguments. This information is useful to compilers because strict functions can be compiled more efficiently. Thus, if a function is proven to be strict (using strictness analysis) at compile time, it can be compiled to use a more efficient calling convention without changing the meaning of the enclosing program. Note that a function f is said to diverge if it returns : operationally, that would mean that f either causes abnormal termination of the enclosing program (e. g., failure with an error message) or that it loops infinitely. The notion of "divergence" is significant because a strict function is one that always diverges when given an argument that diverges, whereas a lazy (or non strict) function is one that may or may not diverge when given such an argument. Strictness analysis attempts to determine the "divergence properties" of functions, which thus identifies some functions that are strict.
Передача абстрактного толкования
Анализ строгости может быть охарактеризован как передовая абстрактная интерпретация, которая приближает каждую функцию в программе функцией, которая отображает дивергентные свойства аргументов на дивергентные свойства результатов. В классическом подходе, впервые разработанном Аланом Майкрофтом, абстрактная интерпретация использовала двухточечную область с 0 обозначающей множество, рассматриваемое как подмножество аргумента или типа возвращения, и 1 обозначающая все значения в типе.
Strictness analysis can be characterized as a forward abstract interpretation which approximates each function in the program by a function that maps divergence properties of the arguments onto divergence properties of the results. In the classical approach pioneered by Alan Mycroft, the abstract interpretation used a two point domain with 0 denoting the set considered as a subset of the argument or return type, and 1 denoting all values in the type.
Анализ спроса
Компилятор Glasgow Haskell (GHC) использует обратную абстрактную интерпретацию, известную как анализ спроса, для выполнения анализа строгости, а также других программных анализов. В анализе спроса каждая функция моделируется функцией от стоимостных требований к результату до стоимостных требований к аргументам. Функция строга в аргументе, если требование ее результата приводит к требованию этого аргумента.
The Glasgow Haskell Compiler (GHC) uses a backward abstract interpretation known as demand analysis to perform strictness analysis as well as other program analyses. In demand analysis, each function is modelled by a function from value demands on the result to value demands on the arguments. A function is strict in an argument if a demand for its result leads to a demand for that argument.
Анализ строгости на основе проекции
Анализ строгости на основе проекции, введенный Филиппом Уодлером и Р. Дж. М. Хьюзом, использует проекции строгости для моделирования более тонких форм строгости, таких как строгость головы в аргументе списка. (Напротив, анализ спроса GHC может моделировать строгость только в пределах типов продукта, т.е. типов данных, которые имеют только один конструктор.) Функция считается строгой для головы, если , где проекция, что голова оценивает свой аргумент списка. В 1980-х годах был проведен большой объем исследований по анализу строгости.
Projection based strictness analysis, introduced by Philip Wadler and R. J. M. Hughes, uses strictness projections to model more subtle forms of strictness, such as head strictness in a list argument. (By contrast, GHC's demand analysis can only model strictness within product types, i. e., datatypes that only have a single constructor.) A function is considered head strict if , where is the projection that head evaluates its list argument. There was a large body of research on strictness analysis in the 1980s.