Propiedad de un sistema de reescritura o reducción que afirma que siempre que un término puede reducirse por dos secuencias (posiblemente distintas) a términos s y t, existe un término u al que tanto s como t pueden reducirse ulteriormente (es decir, s ↓ u y t ↓ u). La confluencia suele llamarse propiedad de Church–Rosser.

Principio

Los diferentes caminos de reducción desde un mismo punto de partida pueden reunirse: la divergencia local es inofensiva porque las reducciones confluyen en un descendiente común, lo que asegura la coherencia del razonamiento equacional y resultados canónicos cuando existen formas normales.

Demostración

En el cálculo lambda con β-reducción, el teorema de Church–Rosser muestra que si dos términos son β-convertibles, tienen un reductor común. En la práctica esto significa que distintas elecciones de orden de evaluación (cuando las reducciones terminan) conducen a la misma forma normal salvo conversión.

Aplicación incorrecta

Suponer que la confluencia implica terminación (es decir, que toda secuencia de reducción alcanza una forma normal) es incorrecto. También presumir confluencia en sistemas con efectos secundarios, reglas sensibles al contexto u operaciones no deterministas puede producir conclusiones no válidas.

Consecuencia

Garantiza la unicidad de las formas normales salvo conversión y permite estrategias de reducción intercambiables: el razonamiento equacional y la transformación de programas son seguros porque distintas secuencias de reescritura no producen resultados irreconciliables.

Inversión

Los sistemas no confluyentes admiten divergencias críticas donde distintas secuencias de reducción conducen a formas normales irreconciliables o a términos sin reductor común, haciendo que el resultado dependa de las elecciones de reducción.

Límite

La confluencia es una propiedad de la relación de reducción y puede no mantenerse en presencia de efectos secundarios, reescrituras sensibles al contexto no restringidas o cuando las reducciones no están cerradas bajo las propiedades de cierre de la relación. El lema de Newman relaciona la confluencia local más la terminación con la confluencia global.

Tensión semántica

Existe tensión entre la confluencia como garantía de corrección y preocupaciones prácticas como la eficiencia de evaluación o el uso de recursos: un sistema confluyente puede admitir rutas de reducción caras o no terminantes, por lo que la confluencia no resuelve problemas de rendimiento o terminación.

Síntesis

La Confluencia (propiedad de Church–Rosser) asegura que las secuencias de reducción divergentes desde un mismo término pueden reunirse en un reductor común, proporcionando coherencia para la reescritura y la transformación de programas, mientras permanece distinta de propiedades de terminación o complejidad.