Análisis de estrictez

El análisis de estrictez puede caracterizarse 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 a las propiedades de divergencia de los resultados. En el enfoque clásico iniciado por Alan Mycroft , la interpretación abstracta utilizaba un dominio de dos puntos donde 0 denotaba el conjunto${\displaystyle \{\bot \}}$considerado como un subconjunto del argumento o tipo de retorno, y 1 denota todos los valores en el tipo. ^{[ 1 ]}

El compilador Glasgow Haskell (GHC) utiliza una interpretación abstracta inversa conocida como análisis de demanda para realizar análisis de estrictez, así como otros análisis de programas. En el análisis de demanda, cada función se modela mediante una función que relaciona las demandas de valor sobre el resultado con las demandas de valor sobre los argumentos. Una función es estricta en un argumento si una demanda sobre su resultado conlleva una demanda sobre ese argumento. ^{[ 2 ]}

El análisis de estrictez basado en proyecciones, introducido por Philip Wadler y RJM Hughes , utiliza proyecciones de estrictez para modelar formas más sutiles de estrictez, como la estrictez de cabeza en un argumento de lista. (Por el contrario, el análisis de demanda de GHC solo puede modelar la estrictez dentro de los tipos de producto , es decir, tipos de datos que solo tienen un único constructor ). Una función${\displaystyle f}$se considera estricto en la cabeza si${\displaystyle f=f\circ \pi }$, dónde${\displaystyle \pi }$es la proyección que evalúa en primer plano su argumento de lista. ^{[ 3 ]}

En la década de 1980, existió un amplio corpus de investigación sobre el análisis de la rigurosidad.