Анализ строгости

В информатике относится к любому алгоритму, используемому для доказательства того , анализ строгости что функция на нестрогом функциональном языке программирования является строгой по одному или нескольким своим аргументам. Эта информация полезна для компиляторов , поскольку строгие функции можно компилировать более эффективно. Таким образом, если во время компиляции доказано, что функция является строгой (с помощью анализа строгости), ее можно скомпилировать для использования более эффективного соглашения о вызовах, не меняя смысла включающей ее программы.

Обратите внимание, что функция f говорят, что он расходится, если возвращается $\{\bot \}$ : с оперативной точки зрения это будет означать, что f либо приводит к ненормальному завершению включающей программы (например, сбой с сообщением об ошибке), либо к бесконечному циклу. Понятие «расхождение» важно, потому что строгая функция — это функция, которая всегда расходится, когда ей дан расходящийся аргумент, тогда как ленивая (или нестрогая) функция — это функция, которая может расходиться, а может и не расходиться, когда ей дан такой аргумент. Анализ строгости пытается определить «свойства дивергенции» функций, что, таким образом, идентифицирует некоторые функции, которые являются строгими.

Подходы к анализу строгости

Прямая абстрактная интерпретация

Анализ строгости можно охарактеризовать как прямую абстрактную интерпретацию , которая аппроксимирует каждую функцию в программе функцией, которая отображает свойства расхождения аргументов на свойства расхождения результатов. В классическом подходе, впервые предложенном Аланом Майкрофтом , абстрактная интерпретация использовала двухточечную область , где 0 обозначает множество $\{\bot \}$ рассматривается как подмножество типа аргумента или возвращаемого значения, а 1 обозначает все значения типа. ^[1]

Анализ спроса

Компилятор Glasgow Haskell (GHC) использует обратную абстрактную интерпретацию, известную как анализ спроса, для выполнения анализа строгости, а также другого анализа программы. В анализе спроса каждая функция моделируется функцией от требований к значению результата к требованиям к значениям аргументов. Функция является строгой в отношении аргумента, если требование ее результата приводит к требованию этого аргумента. ^[2]

Анализ строгости на основе прогнозов

Анализ строгости на основе проекций, предложенный Филипом Уодлером и Р.Дж.М. Хьюзом , использует проекции строгости для моделирования более тонких форм строгости, таких как строгость головы в аргументе списка. (Напротив, анализ спроса GHC может моделировать строгость только внутри типов продуктов , т. е. типов данных, которые имеют только один конструктор .) Функция $f$ считается строгим, если $f=f\circ \pi$ , где $\pi$ — это проекция, которая вычисляет аргумент списка. ^[3]

В 1980-х годах было проведено большое количество исследований по анализу строгости.

Ссылки

^ Майкрофт, Алан (1980). «Теория и практика преобразования вызова по необходимости в вызов по значению». Конспект лекций по информатике: Учеб. 4-й международный Симп. по программированию, Vol. 83 . Спрингер-Верлаг.
^ «Комментарий GHC: анализатор спроса в GHC» . Проверено 12 февраля 2014 г.
^ Вадлер, П.; РДЖМ Хьюз (1987). «Прогнозы для анализа строгости». Функциональное программирование и компьютерная архитектура; ЛНКС 274 . Спрингер-Верлаг.

[1] Майкрофт, Алан (1980). «Теория и практика преобразования вызова по необходимости в вызов по значению». Конспект лекций по информатике: Учеб. 4-й международный Симп. по программированию, Vol. 83 . Спрингер-Верлаг.

[2] «Комментарий GHC: анализатор спроса в GHC» . Проверено 12 февраля 2014 г.

[3] Вадлер, П.; РДЖМ Хьюз (1987). «Прогнозы для анализа строгости». Функциональное программирование и компьютерная архитектура; ЛНКС 274 . Спрингер-Верлаг.

[1]

[2]

[3]