Un mecanismo algorítmico que calcula la relación de congruencia mínima que contiene un conjunto dado de igualdades sobre términos, típicamente fusionando clases de equivalencia y propagando congruencia de funciones para permitir un razonamiento eficiente sobre igualdades, especialmente en teorías de funciones no interpretadas.

Principio

Mantener clases de equivalencia de términos bajo igualdades afirmadas, fusionar clases cuando aparezcan igualdades y asegurar que si f(a1,...,an) y f(b1,...,bn) están presentes y ai ≡ bi para todo i, entonces los términos compuestos también se fusionen, repitiendo hasta alcanzar el cierre.

Demostración

Dadas las igualdades a = b y f(a) = c, el cierre fusiona a y b en una clase, reconoce que f(a) y f(b) son equivalentes y fusiona sus clases, lo que permite al solucionador deducir ulteriormente igualdades o contradicciones de manera eficiente.

Aplicación incorrecta

Aplicar el cierre de congruencia de forma ingenua en grafos de términos muy grandes sin hash-consing o union-by-rank puede provocar un gran aumento de coste y memoria; el manejo incorrecto de aridades de símbolos de función o de tipos puede producir fusiones no válidas.

Consecuencia

Un cierre de congruencia correcto proporciona razonamiento de igualdades rápido y canónico usado en motores SMT y demostradores, permitiendo verificaciones de representantes en tiempo constante y actualizaciones incrementales a medida que se añaden igualdades.

Inversión

La inversión es tratar las igualdades solo por emparejamiento sintáctico sin propagación de cierre: esto conserva las igualdades iniciales pero omite muchas igualdades implícitas y ofrece menor potencia de razonamiento.

Límite

Se dirige al razonamiento de igualdad para funciones no interpretadas en términos de primer orden y igualdades ground; no maneja por sí solo teorías interpretadas (aritmética, arreglos) sin combinarse con otros solucionadores de teoría.

Tensión semántica

Existe tensión entre el cierre de congruencia y el tratamiento de igualdades estilo resolución: el cierre de congruencia proporciona mantenimiento incremental impulsado por estructuras de datos, mientras la resolución maneja igualdades mediante manipulación e inferencia de cláusulas.

Síntesis

El cierre de congruencia fusiona incrementalmente clases de equivalencia de términos y propaga la congruencia de funciones para formar la congruencia mínima que contiene las igualdades dadas, ofreciendo razonamiento de igualdad compacto y eficiente que se integra naturalmente en procedimientos SMT y de decisión.