Divergencia (informática)

En la reescritura abstracta , un sistema de reescritura abstracta se denomina convergente si es confluente y terminante . ^{[ 2 ]}

La notación t ↓ n significa que t se reduce a la forma normal n en cero o más reducciones , t ↓ significa que t se reduce a alguna forma normal en cero o más reducciones, y t ↑ significa que t no se reduce a una forma normal; esto último es imposible en un sistema de reescritura terminante.

En el cálculo lambda, una expresión es divergente si no tiene forma normal . ^{[ 3 ]}

En la semántica denotacional, una función de objeto f  : A → B puede modelarse como una función matemática.${\displaystyle f:A\cup \{\perp \}\rightarrow B\cup \{\perp \}}$donde ⊥ ( abajo ) indica que la función objeto o su argumento diverge.

En el cálculo de procesos secuenciales comunicantes (CSP), la divergencia ocurre cuando un proceso realiza una serie interminable de acciones ocultas. ^{[ 4 ]} Por ejemplo, considérese el siguiente proceso, definido por la notación CSP: $${\displaystyle Clock=tick\rightarrow Clock}$$ Las huellas de este proceso se definen como: $${\displaystyle \operatorname {trazas} (Reloj)=\{\langle \rangle ,\langle tick\rangle ,\langle tick,tick\rangle ,\ldots \}=\{tick\}^{*}}$$ Ahora bien, consideremos el siguiente proceso, que oculta el evento de tick del proceso Clock : $${\displaystyle P=Reloj\setminus tick}$$ Como${\displaystyle P}$no puede hacer otra cosa que realizar acciones ocultas para siempre, es equivalente al proceso que no hace más que divergir, denotado${\displaystyle \mathbf {div} }$Un modelo semántico de CSP es el modelo de fallos-divergencias, que refina el modelo de fallos estables al distinguir los procesos en función de los conjuntos de trazas tras los cuales pueden divergir.