Teoría de retículos y puntos fijos

Fundamentos · Actualizado el 16 de agosto de 2026

Todo lo que viene a partir de aquí descansa sobre una única estructura matemática: el retículo completo. Este capítulo la construye desde cero, con la mínima abstracción necesaria, y demuestra el teorema que garantiza que los análisis terminan y devuelven la mejor respuesta posible. La conexión entre retículos y análisis de programas se estableció en los trabajos fundacionales de Kildall (1973) y Kam y Ullman (1977).

5.1 Un ejemplo motivador: el análisis de signos

Supongamos que queremos un análisis que averigüe los signos posibles de los valores enteros de las variables y expresiones de un programa. En una ejecución concreta, los valores pueden ser enteros arbitrarios. Nuestro análisis, en cambio, considera una abstracción agrupándolos en tres categorías, o valores abstractos: positivo (+), negativo (-) y cero (0).

Como en cualquier análisis, la indecidibilidad nos obliga a aproximar, así que hay que estar preparado para información incierta: añadimos un valor abstracto especial ⊤ que significa «no lo sé». Hay que decidir además qué queremos en los casos en que el signo de una expresión es positivo en unas ejecuciones y no en otras. Aquí nos interesa información definida: el análisis sólo debe informar + si es seguro que la expresión evaluará a un número positivo en toda ejecución, y ⊤ en caso contrario. Resulta útil, por último, añadir un valor ⊥ para expresiones cuyos valores no son números —sino punteros, por ejemplo— o que no tienen ningún valor porque el punto en cuestión es inalcanzable desde la entrada.

Considérese este programa:

var a, b, c;
a = 42;
b = 87;
if (input) {
    c = a + b;
} else {
    c = a - b;
}

El análisis puede concluir que a y b son positivos en todas las ejecuciones posibles al final del programa. El signo de c es positivo o negativo según la ejecución concreta, así que el análisis debe informar ⊤ para esa variable.

Tenemos, pues, un dominio abstracto con cinco valores, {+, -, 0, ⊤, ⊥}, que se organiza así, con la información menos precisa arriba y la más precisa abajo:

                    T
                  / | \
                 /  |  \
                -   0   +
                 \  |  /
                  \ | /
                    _|_        (bottom)

El dominio abstracto del analisis de signos. Es un reticulo completo de altura 2.

El orden refleja que ⊥ representa el conjunto vacío de valores enteros y ⊤ el conjunto de todos ellos. Nótese que ⊤ puede surgir por dos razones distintas: (1) porque realmente hay ejecuciones en que c es positiva y ejecuciones en que es negativa, en cuyo caso, con este dominio abstracto, ⊤ es la única respuesta correcta; y (2) porque la imprecisión es inevitable por indecidibilidad, así que por bien que diseñemos el análisis habrá programas donde una variable sólo pueda tomar valores positivos y el análisis no consiga demostrar que no puede tomar también negativos —recuérdese el ejemplo de TM(j) del capítulo «1»—.

5.2 Órdenes parciales

Un orden parcial (partial order) es un conjunto S dotado de una relación binaria ⊑ que satisface:

reflexividad: ∀x ∈ S : x ⊑ x
transitividad: ∀x, y, z ∈ S : x ⊑ y ∧ y ⊑ z ⟹ x ⊑ z
antisimetría: ∀x, y ∈ S : x ⊑ y ∧ y ⊑ x ⟹ x = y

El dominio abstracto de la sección anterior es un orden parcial, con S = {-, 0, +, ⊤, ⊥} y, por ejemplo, ⊥ ⊑ + y + ⊑ ⊤.

Cuando x ⊑ y decimos que y es una aproximación segura de x, o que x es al menos tan preciso como y. Formalmente un orden parcial es el par (S, ⊑), pero se suele usar el mismo nombre para el orden y para su conjunto subyacente. También escribiremos a veces y ⊒ x en lugar de x ⊑ y.

Sea X ⊆ S. Decimos que y ∈ S es una cota superior de X, escrito X ⊑ y, si ∀x ∈ X : x ⊑ y; análogamente, y es cota inferior de X, escrito y ⊑ X, si ∀x ∈ X : y ⊑ x. El supremo o menor cota superior, escrito ⊔X, se define por:

X ⊑ ⊔X ∧ ∀y ∈ S : X ⊑ y ⟹ ⊔X ⊑ y

Dualmente, el ínfimo o mayor cota inferior, ⊓X:

⊓X ⊑ X ∧ ∀y ∈ S : y ⊑ X ⟹ y ⊑ ⊓X

Para parejas de elementos se usa la notación infija x ⊔ y —el join de x e y— en lugar de ⊔{x, y}, y x ⊓ y —el meet— en lugar de ⊓{x, y}.

La operación de supremo es la que hace todo el trabajo en el análisis de programas. Es la que se usa para combinar información abstracta procedente de varias fuentes: por ejemplo, cuando el flujo de control confluye tras las ramas de un if. En el ejemplo de la «sección 5.1 · Un ejemplo motivador: el análisis de signos», c acaba valiendo + ⊔ - = ⊤.

5.3 Retículos y retículos completos

Un retículo (lattice) es un orden parcial (S, ⊑) en el que x ⊔ y y x ⊓ y existen para todos x, y ∈ S.

Un retículo completo (complete lattice) es un orden parcial (S, ⊑) en el que ⊔X y ⊓X existen para todo X ⊆ S. Trivialmente, todo retículo completo es un retículo. Casi todos los retículos que aparecen en análisis de programas son completos.

Todo retículo completo tiene un único elemento máximo, denotado ⊤ («top»), y un único elemento mínimo, ⊥ («bottom»); en concreto ⊤ = ⊔S y ⊥ = ⊓S, y también ⊤ = ⊓∅ y ⊥ = ⊔∅.

Todo orden parcial finito puede dibujarse mediante un diagrama de Hasse, en el que los elementos son nodos y la relación de orden es la clausura transitiva de las aristas que van de nodos inferiores a superiores. Éstos son retículos:

     T           T             T
     |          / \           /|\
     a         a   b         a b c
     |          \ /           \|/
     _|_        _|_           _|_

Tres ordenes parciales que si son reticulos.

Y éstos no lo son, porque hay parejas de elementos sin supremo o sin ínfimo:

      c   d          a   b
       \ / \          \ /
        a   b          c   d
                        \ /
                         e

Dos ordenes parciales que no son reticulos: a y b no tienen un unico supremo minimo.

En el primero, a y b tienen dos cotas superiores minimales incomparables (c y d) y por tanto no tienen supremo.

Formalización

Dos propiedades útiles

Unicidad. Si ⊔X existe, es único. En efecto, si s y s' fueran ambos supremos de X, entonces s ⊑ s' (porque s' es cota superior y s es la menor) y s' ⊑ s (por lo mismo), luego s = s' por antisimetría. El argumento dual vale para ⊓X.

Caracterización del orden. Si x ⊔ y existe, entonces x ⊑ y ⟺ x ⊔ y = y; y si x ⊓ y existe, entonces x ⊑ y ⟺ x ⊓ y = x. Esta equivalencia se usará continuamente para reescribir desigualdades como ecuaciones.

Basta con una de las dos. Si S es un conjunto parcialmente ordenado, todo subconjunto de S tiene supremo si y sólo si todo subconjunto tiene ínfimo. La construcción es ⊓X = ⊔{y ∈ S | y ⊑ X}. Por tanto, para demostrar que un orden parcial es un retículo completo basta con argumentar la existencia de supremos.

Finito implica completo. Todo retículo finito no vacío es completo. En cambio, existen retículos no vacíos que no son completos: por ejemplo, el conjunto de los enteros con el orden habitual es un retículo (el supremo de dos enteros es el mayor) pero no es completo, porque el conjunto de todos los enteros no tiene supremo.

5.4 Cómo construir retículos

En la práctica casi nunca se define un retículo desde cero: se combinan unos pocos constructores.

Retículo de partes (powerset lattice). Todo conjunto A = {a₁, a₂, …} define un retículo completo (℘(A), ⊆), donde ⊥ = ∅, ⊤ = A, x ⊔ y = x ∪ y y x ⊓ y = x ∩ y. Para A = {0,1,2,3}:

                    {0,1,2,3}
                 /      |     \      \
          {0,1,2}   {0,1,3}  {0,2,3}  {1,2,3}
          /  |  \    /  |  \   /  |  \  /  | \
       {0,1} {0,2} {0,3} {1,2} {1,3} {2,3}
          \  |  /    \  |  /   \  |  /
           {0}      {1}      {2}      {3}
                 \    |     |     /
                       (vacio)

Reticulo de partes de {0,1,2,3}. Tiene altura 4.

Es el retículo que usaremos en el capítulo «6» para representar conjuntos de variables o de expresiones.

Retículo de partes invertido. El mismo conjunto con el orden ⊇. Se usa cuando el análisis es must en lugar de may: allí el supremo es la intersección.

Retículo plano (flat lattice). Dado un conjunto A, flat(A) es:

                   T
              /  /   \  \
            a1  a2  ...  an
              \  \   /  /
                  _|_

Reticulo plano sobre un conjunto A. Altura 2.

Es un retículo completo de altura 2. El dominio Sign = {+, -, 0, ⊤, ⊥} de la «sección 5.1 · Un ejemplo motivador: el análisis de signos» no es más que flat({+, 0, -}).

Producto. Si L₁, …, Lₙ son retículos completos, también lo es el producto

L₁ × L₂ × … × Lₙ = { (x₁, …, xₙ) | xᵢ ∈ Lᵢ }

con el orden definido componente a componente: (x₁,…,xₙ) ⊑ (x'₁,…,x'ₙ) ⟺ ∀i : xᵢ ⊑ x'ᵢ. Las operaciones ⊔ y ⊓ también se calculan componente a componente, y la altura es la suma de las alturas: height(L₁ × … × Lₙ) = height(L₁) + … + height(Lₙ). El producto de n copias del mismo retículo se escribe Lⁿ.

Retículo de aplicaciones (map lattice). Si A es un conjunto y L un retículo completo, el conjunto de funciones de A en L, ordenado punto a punto, es un retículo completo:

A → L = { [a₁ ↦ x₁, a₂ ↦ x₂, …] } con f ⊑ g ⟺ ∀aᵢ ∈ A : f(aᵢ) ⊑ g(aᵢ)

Éste es el constructor decisivo. El estado abstracto de un análisis es típicamente un elemento de StateSign = Var → Sign, donde Var es el conjunto de nombres de variable del programa: una función que asigna a cada variable su valor abstracto. Y como todo producto Lⁿ es isomorfo a un retículo de aplicaciones A → L y viceversa, decir «un vector de n estados abstractos» o «una función de nodos del CFG en estados abstractos» es lo mismo: StateSignⁿ ≅ Node → StateSign.

Usaremos la notación f[a ↦ x] para la función idéntica a f salvo que asigna x a a.

Elevación (lift). Si L es un retículo completo, también lo es lift(L), una copia de L con un nuevo elemento mínimo debajo. Su altura es height(L) + 1. Se usa para el análisis de intervalos (capítulo «8») y para representar información de alcanzabilidad (capítulo «15»).

Altura. La altura (height) de un retículo es la longitud del camino más largo de ⊥ a ⊤. La altura del retículo de signos es 2; la de (℘(A), ⊆) es |A|. Algunos retículos tienen altura infinita, y ése es exactamente el problema que resuelve el widening del capítulo «8».

5.5 Sistemas de ecuaciones

Sigamos con el análisis de signos. ¿Cuáles son los signos de las variables en cada línea del siguiente programa?

var a, b;      // 1
a = 42;        // 2
b = a + input; // 3
a = a - b;     // 4

Podemos derivar un sistema de ecuaciones con una variable de restricción por cada pareja (variable del programa, número de línea):

a1 = T          b1 = T
a2 = +          b2 = b1
a3 = a2         b3 = a2 + T
a4 = a3 - b3    b4 = b3

donde a₂ denota el valor abstracto de a inmediatamente después de la línea 2, y los operadores + y - operan aquí sobre valores abstractos —el capítulo «6» los define—. Alternativamente, y de forma equivalente, se puede usar una sola variable de restricción por línea, con valores en el retículo de estados abstractos StateSign:

x1 = [a -> T, b -> T]
x2 = x1[a -> +]
x3 = x2[b -> x2(a) + T]
x4 = x3[a -> x3(a) - x3(b)]

En este ejemplo cada ecuación sólo depende de las anteriores, así que la solución se halla por sustitución. Pero en cuanto el programa tenga bucles aparecerán ecuaciones mutuamente recursivas, y ahí la sustitución no sirve.

Obsérvese también que para este programa importa el orden de las sentencias: cuando se lee a en la línea 3, el valor viene de la asignación de la línea 2, no de la de la línea 4. A un análisis que tiene en cuenta el orden se le llama sensible al flujo (flow-sensitive).

Desigualdades. Los sistemas de inecuaciones se reducen a sistemas de ecuaciones sin cambiar sus soluciones. Como x ⊒ y ⟺ x = x ⊔ y, el sistema xᵢ ⊒ fᵢ(x₁,…,xₙ) se reescribe como xᵢ = xᵢ ⊔ fᵢ(x₁,…,xₙ); y como x ⊑ y ⟺ x = x ⊓ y, el sistema xᵢ ⊑ fᵢ(…) se reescribe como xᵢ = xᵢ ⊓ fᵢ(…). Varias inecuaciones sobre la misma variable se agrupan en una sola: x₁ ⊒ f₁ₐ(…) y x₁ ⊒ f₁ᵦ(…) equivalen a x₁ = x₁ ⊔ f₁ₐ(…) ⊔ f₁ᵦ(…).

Esto explica formalmente la afirmación del capítulo «1» de que el enfoque por ecuaciones y el enfoque por restricciones son intercambiables.

5.6 Monotonía

Una función f : L₁ → L₂ entre retículos es monótona (monotone, o order-preserving) cuando

∀x, y ∈ L₁ : x ⊑ y ⟹ f(x) ⊑ f(y)

Como el orden del retículo representa precisión de la información, la intuición de la monotonía es que «una entrada más precisa no produce una salida menos precisa». Es una condición sorprendentemente débil —no dice nada sobre cuánta información se pierde— y sin embargo es todo lo que hace falta.

Propiedades que se usarán sin mencionarlas:

Toda función constante es monótona.
La composición de funciones monótonas es monótona.
Los operadores ⊔ y ⊓, vistos como funciones de dos argumentos, son monótonos.
f es monótona si y sólo si ∀x, y : f(x) ⊔ f(y) ⊑ f(x ⊔ y).
Una función f : L₁ → L₂ es distributiva (distributive) cuando ∀x, y : f(x) ⊔ f(y) = f(x ⊔ y). Toda función distributiva es monótona, pero no al revés. La distributividad es la hipótesis extra que hace exactos los marcos IFDS del capítulo «11» y el resultado MOP del capítulo «6».
La diferencia de conjuntos X \ Y sobre un retículo de partes es monótona en X pero no en Y. Es un detalle que hay que vigilar al escribir funciones de transferencia con conjuntos kill.

5.7 El teorema del punto fijo

Decimos que x ∈ L es un punto fijo de f si f(x) = x. Un menor punto fijo de f es un punto fijo x tal que x ⊑ y para todo punto fijo y de f.

Un sistema de ecuaciones sobre un retículo completo L tiene la forma

x1 = f1(x1, ..., xn)
x2 = f2(x1, ..., xn)
...
xn = fn(x1, ..., xn)

donde f₁,…,fₙ : Lⁿ → L son las funciones de restricción. Combinándolas en una sola función f : Lⁿ → Lⁿ, el sistema se escribe simplemente x = f(x), lo que deja claro que una solución del sistema es un punto fijo de f. Y como buscamos la solución más precisa, buscamos el menor punto fijo. Además, f es monótona si y sólo si cada fᵢ lo es.

Formalización

Teorema del punto fijo (Kleene)

En un retículo completo L de altura finita, toda función monótona f : L → L tiene un único menor punto fijo, denotado lfp(f), dado por

lfp(f) = ⊔_{i ≥ 0} fⁱ(⊥)

Demostración. Como ⊥ es el elemento mínimo, ⊥ ⊑ f(⊥). Por monotonía, f(⊥) ⊑ f²(⊥), y por inducción fⁱ(⊥) ⊑ fⁱ⁺¹(⊥) para todo i. Tenemos, pues, una cadena creciente

⊥ ⊑ f(⊥) ⊑ f²(⊥) ⊑ …

Como L tiene altura finita, existe algún k con f^k(⊥) = f^k+1(⊥), es decir, f^k(⊥) es un punto fijo de f, y es el supremo de todos los elementos de la cadena, luego lfp(f) = f^k(⊥).

Supongamos ahora que x es otro punto fijo cualquiera. Como ⊥ ⊑ x, la monotonía da f(⊥) ⊑ f(x) = x, y por inducción f^k(⊥) ⊑ x. Luego lfp(f) es efectivamente el menor punto fijo, y por antisimetría de ⊑ es único. ∎

Knaster–Tarski. Sin la hipótesis de altura finita el teorema de Kleene falla como algoritmo, pero la existencia se conserva: en cualquier retículo completo, toda función monótona f tiene menor punto fijo, dado por lfp(f) = ⊓{x ∈ L | f(x) ⊑ x}. Lo que se pierde es la garantía de que la iteración desde ⊥ lo alcance en un número finito de pasos, y esa pérdida es exactamente el problema que el widening del capítulo «8» resuelve.

Monotonía imprescindible. Sin monotonía el teorema es falso. Sobre el retículo {⊥, ⊤}, la función f(⊥) = ⊤, f(⊤) = ⊥ no tiene ningún punto fijo.

El teorema es un resultado potente. No sólo dice que los sistemas de ecuaciones sobre retículos completos siempre tienen solución —siempre que los retículos tengan altura finita y las funciones de restricción sean monótonas—, sino que existe siempre una solución únicamente más precisa que todas las demás. Y además proporciona un algoritmo: calcular la cadena creciente ⊥ ⊑ f(⊥) ⊑ f²(⊥) ⊑ … hasta llegar al punto fijo.

procedure NaiveFixedPoint(f)
    x := bottom
    repeat
        x_old := x
        x := f(x)
    until x = x_old
    return x

El cálculo puede visualizarse como un ascenso por el retículo empezando en ⊥:

        T
        ^
        |  f^k(bottom) = lfp(f)
        |     ^
        |     |
        |   f^2(bottom)
        |     ^
        |     |
        |   f(bottom)
        |     ^
        |     |
       _|_ ---+

El calculo del punto fijo como ascenso por el reticulo desde bottom.

Se le llama «ingenuo» porque no explota ninguna de las estructuras habituales de los retículos de análisis: recalcula todas las componentes en cada iteración, incluso las que no han podido cambiar. El capítulo «7» presenta las variantes serias.

El coste depende de dos factores: la altura del retículo, que acota el número de iteraciones, y el coste de calcular f(x) y de comparar por igualdad, que se paga en cada iteración.

Formalización

La solución del sistema no es la respuesta verdadera

El menor punto fijo es la solución más precisa posible del sistema de ecuaciones. Pero el sistema de ecuaciones es a su vez una aproximación conservadora del comportamiento real del programa. Por tanto, la respuesta semánticamente más precisa que sería correcta está en general por debajo del menor punto fijo en el retículo.

Hay, pues, dos fuentes de imprecisión superpuestas: la que introduce el dominio abstracto —no hay ningún elemento de Sign que describa exactamente «los múltiplos de 3»— y la que introduce la formulación por ecuaciones —que confunde caminos distintos al unirlos en los nodos de confluencia—. El capítulo «6» caracteriza la segunda mediante la comparación entre las soluciones MOP y MFP, y el capítulo «21» da el marco general.

5.8 Qué retículo usa cada herramienta

En ingeniería inversa

Los retículos que uno se encuentra en la práctica

Los dominios abstractos que aparecen en el análisis de binarios son casi siempre combinaciones de los constructores de la «sección 5.4 · Cómo construir retículos»:

Propagación de constantes: Var → flat(ℤ), altura 2 por variable. Es lo que usan casi todos los decompiladores para resolver saltos indirectos sencillos.
Análisis de intervalos: Var → (ℤ ∪ {-∞}) × (ℤ ∪ {+∞}), altura infinita. Necesita widening. Se usa para acotar índices de array y tamaños de buffer.
Value-Set Analysis (Balakrishnan y Reps): Var → (región de memoria → *stride interval*), un producto de retículos indexado por regiones —pila, montón, estático—. Es la generalización de los intervalos que hace falta cuando los valores son direcciones y no números.
Variables vivas / definiciones alcanzables: retículos de partes ℘(Var) y ℘(Def), altura lineal en el tamaño del programa.
Análisis de punteros: Var → ℘(AllocSite), retículo de aplicaciones sobre retículo de partes.
Análisis de taint: Var → flat({tainted, untainted}), el más simple de todos, y sin embargo el que más vulnerabilidades ha encontrado.

Cuando una herramienta de RE le da un resultado, merece la pena preguntarse cuál de estos retículos hay detrás. El de la propagación de constantes tiene altura 2: pierde toda la información en cuanto una variable toma dos valores distintos. Eso explica por qué un decompilador resuelve perfectamente un switch con tabla contigua y se rinde ante uno con dos tablas.

5.9 Lecturas

El apéndice «A» cubre el mismo material con más generalidad —cadenas ascendentes y descendentes, condiciones ACC y DCC, y el teorema de Knaster–Tarski en su forma general—, para quien quiera los enunciados sin la hipótesis de altura finita.

La referencia histórica de la conexión entre retículos y análisis de programas es Kildall (1973) y Kam y Ullman (1977); el teorema del punto fijo es de Kleene (1952) en la forma aquí usada, y de Knaster (1928) y Tarski (1955) en la forma general. La referencia sobre Value-Set Analysis es Balakrishnan y Reps (2004).