Regla de eliminación basada en la unificación para la igualdad

Hace unos años, me encontré con la siguiente regla de la izquierda para la igualdad en el cálculo posterior:

$$\frac{s \doteq t \leadsto \theta \qquad \theta(\Gamma) \vdash \theta(C)} {\Gamma, s \doteq t \vdash C}$$

Aquí, $s \doteq t \leadsto \theta$ computa el unificador más general, $\theta$ de $s$ y $t$ , y luego se aplica la SUSTITUCIÓN a la conclusión $C$ y todas las hipótesis en el contexto $\Gamma$ .

Lo interesante de esta unificación es que iguala encuentra una sustitución para variables universales (es decir, skolem).

Sin embargo, no recuerdo dónde leí esto, y me preguntaba si alguien podría ayudarme a encontrar una referencia.

A menudo atribuyo esto a las Reglas de reflexión definitoria de Schroeder-Heister, aunque la idea se remonta más allá de eso a Girard y otros; la regla que está buscando es una instancia de la primera presentación en la Sección 4. Sin embargo, también necesita una regla que diga que si la instancia de unificación no es satisfactoria, entonces el supuesto de igualdad tiene la fuerza de una contradicción.

Una cuenta más general ha sido utilizada recientemente en muchos trabajos por Dale Miller, David Baelde y compañía (ver, por ejemplo, los puntos fijos mínimos y mayores en lógica lineal ). La formulación más general, que tampoco se origina con Miller et al., Es que la regla es

$${\{\theta \in {\sf csu}(t,s) \mid \theta\Gamma \vdash \theta{C} \}}\over{\Gamma, t \doteq s \vdash C}$$

donde es el conjunto completo de unificadores , el conjunto de todas las sustituciones unificadoras de y . También puede preferir la forma equivalente de escribir esta regla que prefiero (ver aquí, por ejemplo).${\sf csu}(t,s)$$t$$s$

$${\forall \theta. \theta{t} = \theta{s} \longrightarrow \theta\Gamma \vdash \theta{C}}\over{\Gamma, t \doteq s \vdash C}$$

En cualquier caso, en un lenguaje de términos con unificación decidible donde la existencia de un unificador implica la existencia de un unificador más general, tener cualquiera de estas reglas anteriores puede ser equivalente a tener estas dos reglas:

$${{{\sf no~mgu}(t,s)}\over{\Gamma, t \doteq s \vdash C}} \qquad {{{\sf mgu}(t,s) = \theta \quad \theta\Gamma \vdash \theta{C}}\over{\Gamma, t \doteq s \vdash C}}$$

(PS Frank discutió esto en su curso de programación lógica en las conferencias 6, 7 y 8, que pueden ser de donde lo recuerde).