2
$\begingroup$

The theorem of completeness of type inference states the following:

Suppose $\Gamma \vdash t:S| _{\mathcal{X}}C$,

In other words, I have some term "t" 
whose type is "S" under the assumptions in Gamma, 
assuming the constraints "C" is met.
The "x" denotes that we assign the typed variable "x" to this inference.

And sigma is a mapping of type variables to types.

If:

$\sigma(\Gamma)\vdash \sigma(t) : T$, and

When assume a mapping that Gamma has some t whose type is "T".  When we apply
sigma to that Gamma, our assumptions are still valid

$dom(\sigma)\cap\mathcal{X} = \emptyset$

We want the domain of the type mappings to be disjoint from our type variables.

then there is some solution:

$(\sigma', T)= T$ and

The tuple (sigma', T) is equivalent to T

$\sigma'\backslash\mathcal{X}=\sigma$

sigma' set minus type variables will be equal to sigma

What I don't fully understand (and the Pierce book is so very opaque) is why the need for the $\sigma'$ to prove that the program is typeable. What exactly is happening in that transition from $\sigma \rightarrow \sigma'$.

Or am I being as dense as I think, and this theorem is able to simultaneously look at the step rules I have defined for my language and resolve the term to a concrete value. And Completeness implicitly uses those rules, thus the need for $\sigma'$

$\endgroup$
  • 1
    $\begingroup$ The question would be more useful and answerable if you told us what those notions and symbols mean. $\endgroup$ – Jan Johannsen Jun 30 '17 at 7:58
  • $\begingroup$ That is fair -- I assumed that people on the TCS stackexchange would have some basic understanding. That was clearly misguided, my apologies for that. $\endgroup$ – lilott8 Jun 30 '17 at 20:17
3
$\begingroup$

Assuming that this is from Chapter 22 of Pierce's book, what's going on is that Pierce had to strengthen the statement of the theorem slightly to deal with all the fresh constraint variables tracked in $\mathcal{X}$.

The naive statement of completeness would be is that

If $\Gamma \vdash t:S|_{\mathcal{X}}C$ and $(\sigma, T)$ is a solution for $(\Gamma, t)$, then $(\sigma, T)$ is a solution for $(\Gamma, t, S, C)$.

Basically, this says that if $(\sigma, T)$ is a solution to the type inference problem, then it will be a solution of the generated constraints $C$. However, the inference rules in Figure 22-1 sometimes will create some new contraint variables (for example, rule CT-App), all of which are recorded in $\mathcal{X}$.

If the domain of $\sigma$ overlapped with the new variables constraint generation introduced, then you're in trouble, because now we have the possibility of inconsistencies between $\sigma$ and the constraints in $C$. So, instead Pierce proves that:

If $\Gamma \vdash t:S|_{\mathcal{X}}C$ and $(\sigma, T)$ is a solution for $(\Gamma, t)$ and $\mathrm{dom}(\sigma) \cap \mathcal{X} = \emptyset$, then there exists a $\sigma'$ such that $(\sigma', T)$ is a solution for $(\Gamma, t, S, C)$ and $\sigma'/\mathcal{X} = \sigma$.

So he says that if $(\sigma, T)$ is a solution for $(\Gamma, t)$ that doesn't overlap with $\mathcal{X}$, then there is a solution $(\sigma', T)$ for $(\Gamma, t, S, C)$ such that $\sigma'$ is an extension of $\sigma$ to cover the variables in $\mathcal{X}$.

$\endgroup$
  • $\begingroup$ O.K. so the naive T.I. proves that your assumptions in $\Gamma$ also hold true in $\sigma$. Then we need to introduce a $\sigma'$ s.t. our constraints hold true. Which enables $\sigma'(\Gamma) \vdash \sigma'(t):T$ to be true. Is that a correct restatement? $\endgroup$ – lilott8 Jun 30 '17 at 20:15

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.