2
$\begingroup$

How one does prove that if algorithm W failed for a given program $e$ and context $\Gamma$, then there is no substitution $S$ and type $\tau$ such that $S\Gamma \vdash e : \tau$ ?

The original paper states that from the completeness proof one can derive that "it is decidable whether $e$ has any type at all under the assumptions $\Gamma$". However, I didn't found this proof in the literature.

The algorithm W has some failures cases: the unification algorithm failed, an identifier was not found in the context, a recursive call failed, etc.

I more interested in the hard cases, the easy ones I can do myself.

One hard case seems to be the failure of the unification. In this case we know about the soundness and completeness of both recursive calls and, also, the non-existence of a unifier for $S_2\tau_1$ and $\tau_2\rightarrow \alpha$. How those informations can be used to prove $\neg \exists \tau \:S, S\Gamma \vdash e_1 \: e_2 : \tau $ ?

This part of algorithm W may be relevant here:

$W(\Gamma, e_1\: e_2) =$

$\quad (\tau_1,S_1) \leftarrow W(\Gamma, e_1)$

$\quad (\tau_2,S_2) \leftarrow W(S_1\Gamma, e_2)$

$\quad S \leftarrow \mathrm{unify}(S_2\tau_1, \tau_2\rightarrow \alpha)$ where $\alpha$ is fresh

$\quad$return $(S\alpha, S \circ S_1 \circ S_2)$

There are other hard cases, but I will be accepting an answer if it is about at least this one.

EDIT:

In Damas' PhD thesis, the pages 74-82 are the completeness proof of algorithm W. After this proof there are two corollaries about the existence of principal type schemes. After that the thesis changes to subjects no related to my question.

$\endgroup$
  • 1
    $\begingroup$ The statement you want is just the contrapositive of the completeness theorem which is the content of section 7. It doesn't go into much detail, but does state that you do an induction and formulates the theorem appropriately for that induction. It also states Damas' PhD thesis would have detailed proofs, so I would attempt to look that up. $\endgroup$ – Derek Elkins Jul 1 at 5:01
  • $\begingroup$ @DerekElkins I already looked Damas' PhD thesis, the only corollaries derived from the completeness theorem are about principal type, but not about the decidability of the existence of a type for a given program and context. Although that paper claims such derivation is possible, I haven't yet found the proof. I don't think that this corollary is so trivial. $\endgroup$ – Rafael Castro Jul 1 at 15:18
  • $\begingroup$ @DerekElkins I know you haven't said that this is trivial, I'm sorry about that. $\endgroup$ – Rafael Castro Jul 1 at 16:02

Your Answer

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

Browse other questions tagged or ask your own question.