<p>I've often attributed this to <a href="http://dx.doi.org/10.1109/LICS.1993.287585">Rules of definitional reflection</a> by Schroeder-Heister, though the idea goes back beyond that to Girard and others; the rule you're looking for is an instance of the first display in Section 4. You also, however, need a rule that says that if the unification instance is unsatisfiable, then the assumption of equality has the force of a contradiction.</p>

<p>A more general account has been used recently in a lot of work by Dale Miller, David Baelde, and company (see, for instance, <a href="http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/lpar07final.pdf">Least and greatest fixed points in linear logic</a>). The more general formulation - which also doesn't originate with Miller et al - is that the rule is</p>

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

<p>where ${\sf csu}(t,s)$ is the <i>complete set of unifiers</i> - the set of all unifying substitutions of $t$ and $s$. You might also prefer the equivalent way of writing this rule that I prefer (see <a href="http://reports-archive.adm.cs.cmu.edu/anon/2010/abstracts/10-147.html">here</a> for example). </p>

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

<p>In any case, in a term language with decidable unification where the existence of a unifier implies the existence of a most general unifier, having either of these rules above can be shown to be equivalent to having these two rules:</p>

<p>$$
{{{\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}}
$$</p>

<p>(P.S. Frank discussed this in his <a href="http://www.cs.cmu.edu/~fp/courses/lp/lectures/lp-all.pdf">logic programming course</a> in lectures 6, 7, and 8, which may be where you remember it from.)</p>

CC BY-SA 3.0
2012-05-04T14:27:47.973Z
Thanks! I was looking at the wrong papers of Schroeder-Heister.
Neel Krishnaswami
CC BY-SA 3.0
2012-05-04T15:16:45.120Z
I should probably add that I've been thinking about this in the context of typechecking for GADTs.
Neel Krishnaswami
CC BY-SA 3.0
2012-05-04T15:53:36.883Z
Huh. I have been writing about this in the context of OMG THESIS MUST GRADUATE, so I am not allowed to think about this in the context of typechecking for GADTs ;-).
Rob Simmons
CC BY-SA 3.0
2012-05-04T12:16:13.097Z
2012-05-04T12:39:12.787Z
2012-05-04T12:39:12.787Z
Rob Simmons
<p>A few years back, I ran across the following left-rule for equality in sequent calculus:</p>

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

<p>Here, $s \doteq t \leadsto \theta$ computes the most general unifier $\theta$ for $s$ and $t$, and then applies the substition to the conclusion $C$ and all the hypotheses in the context $\Gamma$. </p>

<p>The interesting thing about this unification is that it equates finds a substitution for universal (i.e., skolem) variables. </p>

<p>However, I cannot remember where I read this, and was wondering if anyone could help me find a reference to it. </p>

<reference-request><lo.logic><pl.programming-languages><proof-theory><sequent-calculus>
Unification-based elimination rule for equality
Neel Krishnaswami
# Unification-based elimination rule for equality

(Asked by: username_0 on 2012-05-04)

A few years back, I ran across the following left-rule for equality in sequent calculus:

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

Here, $s \doteq t \leadsto \theta$ computes the most general unifier $\theta$ for $s$ and $t$, and then applies the substition to the conclusion $C$ and all the hypotheses in the context $\Gamma$.

The interesting thing about this unification is that it equates finds a substitution for universal (i.e., skolem) variables.

However, I cannot remember where I read this, and was wondering if anyone could help me find a reference to it.

**Tags:** reference-request, lo.logic, pl.programming-languages, proof-theory, sequent-calculus


---

## 1 answers

### Answer by username_1 on 2012-05-04. Score: 9 | Accepted answer

I've often attributed this to [Rules of definitional reflection](http://dx.doi.org/10.1109/LICS.1993.287585) by Schroeder-Heister, though the idea goes back beyond that to Girard and others; the rule you're looking for is an instance of the first display in Section 4. You also, however, need a rule that says that if the unification instance is unsatisfiable, then the assumption of equality has the force of a contradiction.

A more general account has been used recently in a lot of work by Dale Miller, David Baelde, and company (see, for instance, [Least and greatest fixed points in linear logic](http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/lpar07final.pdf)). The more general formulation - which also doesn't originate with Miller et al - is that the rule is

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

where ${\sf csu}(t,s)$ is the *complete set of unifiers* - the set of all unifying substitutions of $t$ and $s$. You might also prefer the equivalent way of writing this rule that I prefer (see [here](http://reports-archive.adm.cs.cmu.edu/anon/2010/abstracts/10-147.html) for example).

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

In any case, in a term language with decidable unification where the existence of a unifier implies the existence of a most general unifier, having either of these rules above can be shown to be equivalent to having these two rules:

$$
{{{\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}}
$$

(P.S. Frank discussed this in his [logic programming course](http://www.cs.cmu.edu/~fp/courses/lp/lectures/lp-all.pdf) in lectures 6, 7, and 8, which may be where you remember it from.)

> **Comments:**
> **username_0**: Thanks! I was looking at the wrong papers of Schroeder-Heister.  
> **username_0**: I should probably add that I've been thinking about this in the context of typechecking for GADTs.  
> **username_1**: Huh. I have been writing about this in the context of OMG THESIS MUST GRADUATE, so I am not allowed to think about this in the context of typechecking for GADTs ;-).  

---

