Règle d'élimination fondée sur l'unification pour l'égalité

Il y a quelques années, j'ai rencontré la règle de gauche suivante pour l'égalité dans le calcul séquentiel:

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

Ici, $s \doteq t \leadsto \theta$ calcule l'unificateur le plus général $\theta$ pour $s$ et $t$ , puis applique la sous-position à la conclusion $C$ et à toutes les hypothèses du contexte $\Gamma$ .

La chose intéressante à propos de cette unification est qu'elle équivaut à trouver une substitution pour les variables universelles (c'est-à-dire skolem).

Cependant, je ne me souviens pas où j'ai lu ceci, et je me demandais si quelqu'un pouvait m'aider à trouver une référence.

J'ai souvent attribué cela aux Règles de réflexion définitionnelle de Schroeder-Heister, bien que l'idée remonte au-delà de cela à Girard et à d'autres; la règle que vous recherchez est une instance du premier affichage de la section 4. Cependant, vous avez également besoin d'une règle qui dit que si l'instance d'unification n'est pas satisfaisante, l'hypothèse d'égalité a la force d'une contradiction.

Un compte rendu plus général a été utilisé récemment dans de nombreux travaux de Dale Miller, David Baelde et compagnie (voir, par exemple, Les moindres et les plus grands points fixes en logique linéaire ). La formulation plus générale - qui ne provient pas non plus de Miller et al - est que la règle est

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

où est l' ensemble complet des unifieurs - l'ensemble de toutes les substitutions unificatrices de et . Vous pouvez également préférer la manière équivalente d'écrire cette règle que je préfère (voir ici par exemple).${\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}$$

Dans tous les cas, dans un langage à terme avec unification décidable où l'existence d'un unificateur implique l'existence d'un unificateur le plus général, avoir l'une de ces règles ci-dessus peut être démontré comme équivalant à avoir ces deux règles:

$${{{\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 a discuté de cela dans son cours de programmation logique dans les conférences 6, 7 et 8, ce dont vous vous souvenez peut-être.)