τTau SolutionsApéndices

Índice de notación

Actualizado el 16 de agosto de 2026

La literatura usa notaciones distintas, y a veces incompatibles, para las mismas cosas. Aquí se emplea una sola, coherente de principio a fin. Este apéndice la recoge entera, con el capítulo donde se introduce cada símbolo y, cuando procede, un aviso sobre en qué difiere de la convención más extendida.

D.1 Órdenes y retículos

Símbolo Significado Cap.
⊑ ⊒ orden parcial: x ⊑ y es «x es al menos tan preciso como y» 5
⊏ orden estricto 5
⊔ supremo, join; combinación en puntos de confluencia 5
⊓ ínfimo, meet 5
⊥ elemento mínimo; «inalcanzable» o «sin valor» 5
⊤ elemento máximo; «no lo sé» 5
℘(A) conjunto de partes de A 5
L₁ × L₂ producto de retículos 5
A → L retículo de aplicaciones, ordenado punto a punto 5
lift(L) retículo L con un nuevo elemento mínimo 5
flat(A) retículo plano sobre A, de altura 2 5
height(L) altura: longitud de la cadena más larga 5
f[a ↦ x] la función f modificada para que aplique a a x 5
lfp(f) gfp(f) menor y mayor punto fijo 5, A
Fix(f) conjunto de puntos fijos A
Red(f) Ext(f) elementos donde f es reductiva / extensiva A
ACC, DCC condiciones de cadena ascendente y descendente A

D.2 Programas, puntos y flujo

Símbolo Significado Cap.
Var conjunto de variables del programa 3
Lab conjunto de etiquetas, o puntos de programa 3
Node conjunto de nodos del CFG 4
AExp conjunto de expresiones no triviales del programa 6
[S]ℓ bloque elemental S con etiqueta ℓ 3
⟦v⟧ variable de restricción asociada al nodo v 6
pred(v) succ(v) predecesores y sucesores de v en el CFG 4
JOIN(v) combinación de los estados de los vecinos de v 6
entry exit nodos de entrada y salida del CFG 4
r nodo raíz del CFG; en la literatura de SSA, la entrada 4
flow(S) flowR(S) relación de flujo, hacia adelante y hacia atrás 6
init(S) final(S) etiqueta inicial y etiquetas finales 6
E, ι etiquetas extremales y valor extremal 6
gen, kill conjuntos generados y destruidos por un bloque 6
fℓ función de transferencia de la etiqueta ℓ 6
Analysis∘ Analysis• información a la entrada y a la salida de un bloque 6
MFP, MOP maximal fixed point y meet over all paths 7
dep(v) nodos cuya información depende de la de v 7
Context conjunto de contextos de llamada 10
Call≤k cadenas de llamada de longitud a lo sumo k 10
Path conjunto de contextos de camino 9

D.3 Dominancia y estructura del grafo

Símbolo Significado Cap.
n₁ dom n₂ n₁ domina a n₂ 4
n₁ sdom n₂ n₁ domina estrictamente a n₂ 4
idom(n) dominador inmediato de n 4
Dom(n) conjunto de dominadores de n 4, C
DF(n) frontera de dominancia de n 4
DF⁺(S) frontera de dominancia iterada de S 4
J(S) conjunto de confluencia de S 4, 12
HLC(v) cabeceras de los bucles que contienen a v 4
dominated(x) nodos dominados por x 14
x.depth profundidad de x en el árbol de dominadores 14
D-edge, J-edge aristas de dominancia y de confluencia del DJ-graph 13
rPO orden inverso de postorden 7, C
SC relación de conexión fuerte C
pathsA(n,n') conjunto de caminos de n a n' C

D.4 Forma SSA

Símbolo Significado Cap.
φ función φ, en los puntos de confluencia 12
xᵢ versión i de la variable x 12
Defs(v) nodos que contienen definiciones de v 13
φ-web clase de equivalencia de variables φ-relacionadas 12
C-SSA, T-SSA SSA convencional y transformada 12
‖ ejecución en paralelo de dos instrucciones 13, 16
⊥ (en un operando de φ) uso de un valor indefinido 13
σ función σ, en los puntos de bifurcación (forma SSI) 15
μ función μ: uso potencial, MayUse (HSSA) 16
χ función χ: definición potencial, MayDef (HSSA) 16
v* variable virtual asociada a una región de memoria 16
versión 0 versión sin ocurrencia real, factorizada 16
γ, η funciones de puerta de GSA 16
ψ función ψ de Psi-SSA, con predicados 16
Φ operador Φ del FRG en SSAPRE (mayúscula) 22
h temporal hipotético de SSAPRE 22

D.5 Análisis de valores, punteros y tipos

Símbolo Significado Cap.
Sign retículo de signos, flat({+, 0, -}) 5
State retículo de estados abstractos, Var → L 5
eval(σ, E) evaluación abstracta de E en el estado σ 6
op̂ versión abstracta del operador op 6
Interval retículo de intervalos 8
ω, ∇ operadores de widening, unario y binario 8
Δ operador de narrowing 8, 21
B conjunto de cotas permitidas en el widening 8
s[l,h] intervalo con paso s entre l y h 8
Cell conjunto de celdas abstractas 18
alloc-i celda abstracta del sitio de asignación i 18
pt(X) conjunto de celdas a las que X puede apuntar 18
↑t constructor «puntero a t» (Steensgaard) 18
^τ tipo puntero a τ 19
μα.τ tipo recursivo 19
Γ ⊢ e : τ juicio de tipos 20
Γ ⊢ e : τ & φ juicio de tipos y efectos 20
τ̂ tipo anotado 20
⌊τ̂⌋ tipo subyacente de un tipo anotado 20
refϖ τ̂ tipo de una referencia creada en los puntos de ϖ 20
!π, π:=, new π efectos: acceso, asignación y creación 20

D.6 Semántica e interpretación abstracta

Símbolo Significado Cap.
ConcreteState estados concretos, Var ⇀ ℤ 21
{[v]} conjunto de estados concretos posibles tras v 21
{[P]} semántica de P, igual a lfp(cf) 21
⟦P⟧ resultado del análisis de P, igual a lfp(af) 21
cf, af funciones de restricción semántica y del análisis 21
ceval, csucc evaluación y sucesores concretos 21
α función de abstracción 21
γ función de concretización 21
α ∘ cf ∘ γ abstracción óptima de cf 21
⇀ aplicación parcial 21

D.7 Convenciones tipográficas

  • Negrita para la primera aparición de un concepto que se define en ese punto.
  • Cursiva para el término inglés de un tecnicismo, la primera vez que aparece.
  • Monoespaciado para código, identificadores, nombres de instrucción y elementos de retículo dentro del texto corrido.
  • Los recuadros ▸ Formalización contienen definiciones precisas, teoremas y demostraciones, y pueden saltarse en una primera lectura.
  • Los recuadros ▸ En ingeniería inversa conectan la teoría con lo que hacen las herramientas reales sobre un binario.
  • Los diagramas van en arte ASCII dentro de bloques monoespaciados, con pie numerado por capítulo.
  • El pseudocódigo va en inglés, con := para la asignación.