Análisis de rigurosidad - Strictness analysis

En informática , el análisis de rigor se refiere a cualquier algoritmo utilizado para probar que una función en un lenguaje de programación funcional no estricto es estricta en uno o más de sus argumentos. Esta información es útil para los compiladores porque las funciones estrictas se pueden compilar de manera más eficiente. Por lo tanto, si se demuestra que una función es estricta (usando análisis de rigurosidad) en tiempo de compilación, se puede compilar para usar una convención de llamada más eficiente sin cambiar el significado del programa adjunto.

Tenga en cuenta que f se dice que una función diverge si regresa : operacionalmente, eso significaría que causa una terminación anormal del programa adjunto (por ejemplo, falla con un mensaje de error) o que se repite infinitamente. La noción de "divergencia" es significativa porque una función estricta es aquella que siempre diverge cuando se le da un argumento que diverge, mientras que una función perezosa (o no estricta) es aquella que puede o no divergir cuando se le da tal argumento. El análisis de rigidez intenta determinar las "propiedades de divergencia" de las funciones, lo que identifica algunas funciones que son estrictas. ${\ Displaystyle \ {\ bot \}}$f

Enfoques del análisis de rigor

Interpretación abstracta hacia adelante

El análisis de rigurosidad se puede caracterizar como una interpretación abstracta directa que aproxima cada función del programa mediante una función que mapea las propiedades de divergencia de los argumentos con las propiedades de divergencia de los resultados. En el enfoque clásico iniciado por Alan Mycroft , la interpretación abstracta usó un dominio de dos puntos donde 0 denota el conjunto considerado como un subconjunto del argumento o tipo de retorno, y 1 denota todos los valores en el tipo. ${\ Displaystyle \ {\ bot \}}$

Análisis de demanda

El compilador de Glasgow Haskell (GHC) utiliza una interpretación abstracta hacia atrás conocida como análisis de demanda para realizar análisis de rigor, así como otros análisis de programas. En el análisis de demanda, cada función es modelada por una función desde las demandas de valor en el resultado hasta las demandas de valor en los argumentos. Una función es estricta en un argumento si una demanda de su resultado conduce a una demanda de ese argumento.

Análisis de rigurosidad basado en proyecciones

El análisis de rigurosidad basado en proyecciones, introducido por Philip Wadler y RJM Hughes , utiliza proyecciones de rigurosidad para modelar formas más sutiles de rigurosidad, como el rigor de la cabeza en un argumento de lista. (Por el contrario, el análisis de demanda de GHC solo puede modelar el rigor dentro de los tipos de productos , es decir, tipos de datos que solo tienen un constructor único ). Una función se considera estricta en la cabeza si , donde es la proyección que evalúa en la cabeza su argumento de lista. ${\ Displaystyle f}$${\ Displaystyle f = f \ circ \ pi}$${\ Displaystyle \ pi}$

Hubo una gran cantidad de investigaciones sobre análisis de rigor en la década de 1980.

Referencias