10
$\begingroup$

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.

$\endgroup$
9
$\begingroup$

I've often attributed this to Rules of definitional reflection 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). 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 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 in lectures 6, 7, and 8, which may be where you remember it from.)

$\endgroup$
  • 1
    $\begingroup$ Thanks! I was looking at the wrong papers of Schroeder-Heister. $\endgroup$ – Neel Krishnaswami May 4 '12 at 14:27
  • 2
    $\begingroup$ I should probably add that I've been thinking about this in the context of typechecking for GADTs. $\endgroup$ – Neel Krishnaswami May 4 '12 at 15:16
  • 1
    $\begingroup$ 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 ;-). $\endgroup$ – Rob Simmons May 4 '12 at 15:53

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.