Órdenes parciales y retículos

Avanzado · Actualizado el 16 de agosto de 2026

Los conjuntos parcialmente ordenados y los retículos completos juegan un papel central en el análisis de programas. El capítulo «5» presentó lo imprescindible bajo la hipótesis de altura finita; este apéndice recoge el tratamiento general, sin esa hipótesis, junto con los resultados sobre condiciones de cadena y puntos fijos que los capítulos «8» y «21» utilizan.

A.1 Definiciones básicas

Un orden parcial es una relación ⊑ : L × L → {true, false} que es reflexiva (∀l : l ⊑ l), transitiva (∀l₁,l₂,l₃ : l₁ ⊑ l₂ ∧ l₂ ⊑ l₃ ⟹ l₁ ⊑ l₃) y antisimétrica (∀l₁,l₂ : l₁ ⊑ l₂ ∧ l₂ ⊑ l₁ ⟹ l₁ = l₂). Un conjunto parcialmente ordenado (L, ⊑) es un conjunto L dotado de un orden parcial. Escribiremos l₂ ⊒ l₁ por l₁ ⊑ l₂.

Sea Y ⊆ L. Un elemento l ∈ L es cota superior de Y si ∀l' ∈ Y : l' ⊑ l, y cota inferior si ∀l' ∈ Y : l ⊑ l'. Una menor cota superior —o supremo— l de Y es una cota superior tal que l ⊑ l₀ para cualquier otra cota superior l₀ de Y; dualmente se define la mayor cota inferior o ínfimo.

Un subconjunto Y de un conjunto parcialmente ordenado L no tiene por qué tener cotas superiores ni inferiores, y aunque las tenga no tiene por qué haber una menor ni una mayor. Pero si existen, son únicas, y se denotan ⊔Y y ⊓Y respectivamente. A ⊔ se le llama operador de unión (join) y a ⊓ operador de intersección (meet); para dos elementos se escribe l₁ ⊔ l₂ y l₁ ⊓ l₂.

Un retículo completo es un conjunto parcialmente ordenado L = (L, ⊑) en el que todos los subconjuntos tienen supremo e ínfimo. Se escribe entonces L = (L, ⊑, ⊔, ⊓, ⊥, ⊤), con

⊥ = ⊔∅ = ⊓L y ⊤ = ⊓∅ = ⊔L

el elemento mínimo y el máximo, respectivamente.

Formalización

Basta con la mitad

Lema. Para un conjunto parcialmente ordenado L = (L, ⊑), las tres afirmaciones siguientes son equivalentes:

L es un retículo completo;
todo subconjunto de L tiene supremo;
todo subconjunto de L tiene ínfimo.

Demostración. (1) implica (2) y (3) trivialmente. Para ver que (2) implica (1), sea Y ⊆ L y defínase

⊓Y = ⊔ { l ∈ L : ∀l' ∈ Y . l ⊑ l' }

y compruébese que el elemento así definido es cota inferior de Y —porque todo elemento del conjunto del lado derecho es cota inferior de Y, luego también lo es su supremo— y que es la mayor. La demostración de que (3) implica (1) es dual. ∎

Consecuencia práctica: al diseñar un dominio abstracto basta comprobar que existen los supremos; los ínfimos vienen gratis. Es el resultado que se usó implícitamente en el capítulo «5».

Ejemplo. Si L = (℘(S), ⊆) para un conjunto S, entonces ⊑ es ⊆, ⊔Y es ⋃Y, ⊓Y es ⋂Y, ⊥ = ∅ y ⊤ = S. Si en cambio L = (℘(S), ⊇), entonces ⊑ es ⊇, ⊔Y es ⋂Y, ⊓Y es ⋃Y, ⊥ = S y ⊤ = ∅. Ambos son retículos completos, y la dualidad entre ellos es la que subyace a la distinción may/must del capítulo «6».

        (a)  (P(S), subset)              (b)  (P(S), superset)

              {1,2,3}                            {}
             /   |   \                        /   |   \
        {1,2} {1,3} {2,3}                  {1}  {2}   {3}
          |  X  |  X  |                      |  X  |  X  |
         {1}  {2}   {3}                  {1,2} {1,3} {2,3}
             \   |   /                        \   |   /
                {}                             {1,2,3}

Dos retículos completos sobre S = {1,2,3}: a la izquierda ordenado por inclusion, a la derecha por inclusion inversa. Son el mismo diagrama, leido al reves.

A.2 Familias de Moore

Una familia de Moore (Moore family) es un subconjunto Y de un retículo completo L que es cerrado bajo ínfimos:

∀Y' ⊆ Y : ⊓Y' ∈ Y

De la definición se sigue que una familia de Moore siempre tiene elemento mínimo, ⊓Y, y elemento máximo, ⊓∅, que coincide con el ⊤ de L. En particular, una familia de Moore nunca es vacía.

Ejemplo. Sobre (℘({1,2,3}), ⊆), los conjuntos {{2},{1,2},{2,3},{1,2,3}} y {∅, {1,2,3}} son familias de Moore, mientras que {{1},{2}} y {∅,{1},{2},{1,2}} no lo son.

Las familias de Moore aparecen en el capítulo «21»: el conjunto de elementos abstractos que son imagen de una concretización, γ(L₂) ⊆ L₁, es siempre una familia de Moore cuando (α, γ) es una conexión de Galois. Recíprocamente, toda familia de Moore induce una conexión de Galois. Es la caracterización más limpia de qué subconjuntos del dominio concreto pueden servir como dominio abstracto.

A.3 Propiedades de las funciones

Sea f : L₁ → L₂ una función entre conjuntos parcialmente ordenados L₁ = (L₁, ⊑₁) y L₂ = (L₂, ⊑₂).

f es sobreyectiva (surjective, o epic) si ∀l₂ ∈ L₂ ∃l₁ ∈ L₁ : f(l₁) = l₂.
f es inyectiva (injective, o monic) si ∀l, l' ∈ L₁ : f(l) = f(l') ⟹ l = l'.
f es monótona (monotone, isotone, order-preserving) si ∀l, l' ∈ L₁ : l ⊑₁ l' ⟹ f(l) ⊑₂ f(l').
f es aditiva (additive, join morphism, a veces distributiva) si ∀l₁, l₂ ∈ L₁ : f(l₁ ⊔₁ l₂) = f(l₁) ⊔₂ f(l₂).
f es multiplicativa (multiplicative, meet morphism) si ∀l₁, l₂ ∈ L₁ : f(l₁ ⊓₁ l₂) = f(l₁) ⊓₂ f(l₂).
f es completamente aditiva (complete join morphism) si f(⊔₁Y) = ⊔₂{f(l') : l' ∈ Y} siempre que ⊔₁Y exista; y completamente multiplicativa (complete meet morphism) dualmente.
f es estricta (strict) si f(⊥₁) = ⊥₂.
f es afín (affine) si f(⊔₁Y) = ⊔₂{f(l') : l' ∈ Y} siempre que ⊔₁Y exista y Y ≠ ∅.

Obsérvese la relación entre las tres últimas: una función es completamente aditiva si y sólo si es afín y estricta. La distinción importa: en el análisis de flujo de datos las funciones de transferencia gen/kill son afines pero no siempre estrictas, y la diferencia es exactamente el conjunto gen.

Cuando ⊔₁Y y ⊔₂Y existen siempre —es decir, cuando L₁ y L₂ son retículos completos— las definiciones anteriores requieren también que existan los ínfimos correspondientes, cosa que el lema de la «sección A.1 · Definiciones básicas» garantiza.

Formalización

Dos caracterizaciones útiles

Multiplicatividad completa con codominio finito. Sean L y M retículos completos con M finito. Las tres condiciones siguientes son conjuntamente equivalentes a que γ : M → L sea completamente multiplicativa:

γ es monótona;
γ(⊤) = ⊤;
γ(m₁ ⊓ m₂) = γ(m₁) ⊓ γ(m₂) siempre que m₁ ⋢ m₂ y m₂ ⋢ m₁.

Es un resultado muy práctico: reduce la comprobación de una propiedad sobre todos los subconjuntos a una comprobación sobre las parejas incomparables, que en un dominio abstracto pequeño son pocas. Es la forma habitual de verificar que una función de concretización define una conexión de Galois.

Funciones afines sobre retículos de partes. Una función f : ℘(D) → ℘(E) es afín si y sólo si existen una función φ : D → ℘(E) y un conjunto φ_∅ ∈ ℘(E) tales que

f(Y) = ⋃ { φ(d) : d ∈ Y } ∪ φ_∅

y es completamente aditiva si y sólo si además φ_∅ = ∅.

Esta caracterización es exactamente la representación compacta de funciones distributivas del capítulo «11»: φ_∅ es g(•) y φ(d) es g(d). El grafo bipartito de IFDS es, pues, la forma canónica de una función afín sobre un retículo de partes.

A.4 Construcción de retículos completos

Los retículos completos se combinan para construir otros nuevos. Además de los constructores del capítulo «5», conviene conocer los siguientes.

Producto cartesiano. Dados L₁ = (L₁, ⊑₁) y L₂ = (L₂, ⊑₂), se define L = (L, ⊑) con L = {(l₁, l₂) : l₁ ∈ L₁, l₂ ∈ L₂} y

(l₁₁, l₂₁) ⊑ (l₁₂, l₂₂) ⟺ l₁₁ ⊑₁ l₁₂ ∧ l₂₁ ⊑₂ l₂₂

Si L₁ y L₂ son retículos completos, L también lo es, con supremos e ínfimos calculados componente a componente.

Producto aplastado (smash product). Variante del anterior en la que se exige que todas las parejas (l₁, l₂) cumplan l₁ = ⊥₁ ⟺ l₂ = ⊥₂. Es decir, se identifican todas las parejas en las que alguna componente es ⊥ con un único ⊥ global. Es el constructor adecuado cuando ⊥ significa «inalcanzable»: si un componente es inalcanzable, todo lo es.

Espacio de funciones totales. Sea L₁ un conjunto parcialmente ordenado y S un conjunto. Se define

L = { f : S → L₁ } con f ⊑ f' ⟺ ∀s ∈ S : f(s) ⊑₁ f'(s)

Es el retículo de aplicaciones del capítulo «5». Si L₁ es completo, L también, con ⊔Y = λs. ⊔₁{f(s) : f ∈ Y} y análogamente para ⊓.

Espacio de funciones monótonas. Sean L₁ y L₂ conjuntos parcialmente ordenados. Se define

L = { f : L₁ → L₂ : f\ es\ monótona } con f ⊑ f' ⟺ ∀l ∈ L₁ : f(l) ⊑₂ f'(l)

También es un retículo completo si L₂ lo es. Este constructor es el que da sentido al enfoque funcional de la sensibilidad al contexto del capítulo «10»: los resúmenes de función son elementos de un espacio de funciones monótonas.

Obsérvese que el producto aplastado no preserva la condición de cadena ascendente en general, mientras que los otros tres constructores sí preservan la finitud, las condiciones de cadena y la altura.

A.5 Cadenas y condiciones de cadena

Un subconjunto Y ⊆ L es una cadena (chain) si

∀l₁, l₂ ∈ Y : (l₁ ⊑ l₂) ∨ (l₂ ⊑ l₁)

es decir, si está totalmente ordenado. Es una cadena finita si además es finito.

Una sucesión (lₙ)ₙ es una cadena ascendente si n ≤ m ⟹ lₙ ⊑ l_m, y descendente si n ≤ m ⟹ l_m ⊑ lₙ. Una sucesión se estabiliza eventualmente (eventually stabilises) si

∃n₀ ∈ ℕ : ∀n ≥ n₀ . lₙ = l_n₀

L satisface la condición de cadena ascendente (Ascending Chain Condition, ACC) si todas sus cadenas ascendentes se estabilizan eventualmente.
L satisface la condición de cadena descendente (DCC) si lo hacen las descendentes.
L tiene altura finita si todas sus cadenas son finitas; tiene altura a lo sumo h si todas contienen a lo sumo h+1 elementos.

Formalización

Las tres nociones, relacionadas

Lema. Un conjunto parcialmente ordenado L tiene altura finita si y sólo si satisface simultáneamente la ACC y la DCC.

Demostración. Si L tiene altura finita, toda cadena es finita, luego toda cadena ascendente y toda descendente se estabilizan. Recíprocamente, supóngase que L satisface ambas condiciones y que Y ⊆ L es una cadena; si Y es vacía es finita, así que supóngase (Y, ⊑) no vacía. Usando que todo subconjunto no vacío de una cadena que satisface la DCC tiene elemento mínimo, se construye una cadena ascendente (lₙ)ₙ en Y tomando en cada paso el menor elemento del resto; por la ACC esa cadena se estabiliza, y eso sólo puede ocurrir si Y es finita. ∎

Ejemplos que separan las nociones. El conjunto {-∞, …, -2, -1, 0} con el orden habitual satisface la ACC pero no tiene altura finita. El conjunto {0, 1, 2, …, ∞} satisface la DCC pero tampoco tiene altura finita. Éstos son exactamente los fenómenos que aparecen en el análisis de intervalos del capítulo «8», y la razón de que allí haga falta widening.

Caracterización de los retículos completos con ACC. Para un conjunto parcialmente ordenado L, son equivalentes:

L es un retículo completo que satisface la ACC;
L tiene elemento mínimo ⊥, tiene supremos binarios, y satisface la ACC.

Es el resultado práctico por excelencia: para comprobar que un dominio abstracto sirve, basta exhibir ⊥, definir ⊔ sobre parejas y demostrar la ACC. No hace falta razonar sobre subconjuntos arbitrarios.

Aditividad y afinidad coinciden bajo ACC. En un retículo completo que satisface la ACC, para una función f son equivalentes: (i) f es aditiva, f(l₁ ⊔ l₂) = f(l₁) ⊔ f(l₂); y (ii) f es afín. Y en ambos casos f es monótona. Es decir, bajo ACC la distinción entre distributividad binaria y completa desaparece, lo que simplifica considerablemente las comprobaciones del capítulo «6».

A.6 Puntos fijos

Sea f : L → L una función monótona sobre un retículo completo L.

Un punto fijo de f es un l con f(l) = l. El conjunto de puntos fijos se denota Fix(f) = {l : f(l) = l}.
f es reductiva en l si f(l) ⊑ l; el conjunto de tales elementos se denota Red(f) = {l : f(l) ⊑ l}. Se dice que f es reductiva si Red(f) = L.
f es extensiva en l si f(l) ⊒ l; se escribe Ext(f) = {l : f(l) ⊒ l}. Se dice que f es extensiva si Ext(f) = L.

Como L es un retículo completo, Fix(f) tiene ínfimo y supremo, que se denotan

lfp(f) = ⊓ Fix(f) , gfp(f) = ⊔ Fix(f)

La situación general se resume en el siguiente diagrama, donde todas las desigualdades pueden ser estrictas:

                            T
                            |
                       f^n(T)             conjunto Red(f)
                            |
                   meet_n f^n(T)
                            |
                       gfp(f)   ---------- conjunto Fix(f)
                            |
                       lfp(f)
                            |
                   join_n f^n(_|_)
                            |
                       f^n(_|_)           conjunto Ext(f)
                            |
                          _|_

  _|_  <=  f^n(_|_)  <=  join_n f^n(_|_)  <=  lfp(f)
       <=  gfp(f)   <=  meet_n f^n(T)  <=  f^n(T)  <=  T

Los puntos fijos de f. Ninguna de las desigualdades es en general una igualdad.

En semántica denotacional es habitual iterar hasta el menor punto fijo tomando el supremo de la sucesión (fⁿ(⊥))ₙ. Pero eso requiere una hipótesis de continuidad —f(⊔ₙ lₙ) = ⊔ₙ f(lₙ) para cadenas ascendentes— que aquí no se ha impuesto, así que en general la iteración no alcanza el punto fijo.

Formalización

Cuándo la iteración sí alcanza el punto fijo

Si L satisface la ACC, existe n con fⁿ(⊥) = fⁿ⁺¹(⊥), y entonces

lfp(f) = fⁿ(⊥)

Dualmente, si L satisface la DCC, existe n con fⁿ(⊤) = fⁿ⁺¹(⊤) y gfp(f) = fⁿ(⊤).

Éste es el teorema de Kleene del capítulo «5», ahora con la hipótesis exacta: no hace falta altura finita, basta la ACC. Y obsérvese además que toda función monótona sobre un conjunto parcialmente ordenado que satisfaga la ACC es automáticamente continua, así que la hipótesis de continuidad de la semántica denotacional queda subsumida.

Iteración transfinita. Cuando no hay ACC siempre es posible obtener lfp(f) como límite de una cadena transfinita: se define f^κ ∈ L para un ordinal κ por f^κ = f(⊔_{κ' < κ} f^κ'), y entonces lfp(f) = f^κ para algún ordinal κ estrictamente mayor que el cardinal de L —basta, por ejemplo, el cardinal de ℘(L)—. Es la construcción que justifica que el lfp exista aunque el algoritmo no lo alcance, y la razón teórica por la que el widening del capítulo «8» es una aproximación legítima y no un parche.

A.7 Notas

El capítulo «5» sigue este mismo material bajo la hipótesis de altura finita, que basta para casi todo lo que se hace con él.

Las referencias históricas son Knaster (1928) y Tarski (1955) para el teorema del punto fijo, y Kleene (1952) para la versión iterativa. Para un tratamiento completo de la teoría de órdenes conviene acudir a un texto especializado.