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

<p>The naive statement of completeness  would be is that </p>

<blockquote>
  <p>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)$. </p>
</blockquote>

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

<p>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:</p>

<blockquote>
  <p>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$.</p>
</blockquote>

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

CC BY-SA 3.0
2017-06-30T20:15:48.327Z
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?
lilott8
CC BY-SA 3.0
2017-06-30T09:32:09.627Z
2017-06-30T09:32:09.627Z
Neel Krishnaswami
<p>The theorem of completeness of type inference states the following:</p>

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

<pre><code>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.
</code></pre>

<p>If:</p>

<p>$\sigma(\Gamma)\vdash \sigma(t) : T$, and</p>

<pre><code>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
</code></pre>

<p>$dom(\sigma)\cap\mathcal{X} = \emptyset$</p>

<pre><code>We want the domain of the type mappings to be disjoint from our type variables.
</code></pre>

<p>then there is some solution:</p>

<p>$(\sigma', T)= T$ and</p>

<pre><code>The tuple (sigma', T) is equivalent to T
</code></pre>

<p>$\sigma'\backslash\mathcal{X}=\sigma$</p>

<pre><code>sigma' set minus type variables will be equal to sigma
</code></pre>

<p>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'$.</p>

<p>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'$</p>

CC BY-SA 3.0
2017-06-30T07:58:36.847Z
The question would be more useful and answerable if you told us what those notions and symbols mean.
Jan Johannsen
CC BY-SA 3.0
2017-06-30T20:17:52.470Z
That is fair -- I assumed that people on the TCS stackexchange would have some basic understanding.  That was clearly misguided, my apologies for that.
lilott8
<pl.programming-languages><type-theory><type-systems>
Completeness of Constraint Typing (type inference) question regarding $\sigma'$
lilott8
# Completeness of Constraint Typing (type inference) question regarding $\sigma'$

(Asked by: username_0 on 2017-06-29)

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'$

**Tags:** pl.programming-languages, type-theory, type-systems
> **Comments:**
> **username_1**: The question would be more useful and answerable if you told us what those notions and symbols mean.  
> **username_0**: That is fair -- I assumed that people on the TCS stackexchange would have some basic understanding.  That was clearly misguided, my apologies for that.  

---

## 1 answers

### Answer by username_2 on 2017-06-30. Score: 3 | Accepted answer

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}$.

> **Comments:**
> **username_0**: 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?  

---

