10
$\begingroup$

Yo! This is probably a stupid question, however I've never seen it written down explicitly if, for instance, decidability of type-checking is equivalent to the strong normalization property. Therefore I'm asking this question to clarify all possible relations between type-checking, typability and strong normalization.

Let me explain my motivation. For type theories (I'm being intentionally vague here, but I'm interested mainly in dependent type theories), strong normalization is used to prove the decidability of type-checking. On the other side, any typed systems that I know that have one of these properties also have the other one. However I've never seen explicitly stated that strong normalization is equivalent to decidability of type-checking.

Analogously, to prove typability, one usually (maybe always), reduces a term to a normal form. However it's know that typability is not true for dependent type theories, whereas strong normalization may hold.

By decidability of type-checking, I mean that for any given type $A$, context $\Gamma$ and untyped term $a$, it's possible to decide in a finite number of steps whether $\Gamma \vdash a: A$ is true or not.

By decidability of typability, I mean that for any given untyped term $a$, it's possible to decide in a finite number of steps whether there exist a context $\Gamma$ and a type $A$ such that $\Gamma \vdash a: A$ is true.

1)Is it true that decidability of type-checking is equivalent to every term being strongly normalizable?

2)More generally, what's the relation between decidability of type-checking, typability and strong normalization? Which one implies the other?

Thanks in advance.

EDIT

Given the unsatisfaction regarding the level of generality of my question (which I was unaware of), I would like to delimit it only to Pure Type Systems. Of course, additional comments or counterexamples regarding other type theories will be of great utility.

Improve this question
$\endgroup$
3
  • 4
    $\begingroup$ With no restrictions whatsoever? What if we take the trivial type system where every term has every type? That's trivially decidable but not normalizing. I fear that, in general, unless more constraints are put on the type system, there might be no relations among the notions you cite. $\endgroup$
    – chi
    Commented Apr 30, 2017 at 23:19
  • $\begingroup$ @chi I'm sorry. I wasn't aware of the level of generality of the definition of a typed system. What I had in mind was something like a fragment of Martin-Löf (extensional) type theory with universes. I believe, therefore, that Pure Typed Systems would be the correct bound in my question. $\endgroup$
    – user40276
    Commented May 2, 2017 at 3:39
  • $\begingroup$ What do you mean that Expansion Postponement has been settled? The link is not available anymore. My understanding so far is that it is known to be true for a subclass of PTS (semi-full I think) but it is still an open conjecture for the general case. $\endgroup$
    – Saroupille
    Commented Jul 26, 2019 at 8:02

2 Answers 2

Reset to default
13
$\begingroup$

I'll give a more focused and technical answer to Martin's. If we're interested in dependent type theories, then neither direction is obvious, but both are generally assumed to hold. However the direction Decidable $\Rightarrow$ Normalizing is open, I believe, even for relatively well understood systems, though we do have partial results. This question explores some of the same issues.

More technically: a good technical framework for these questions is the setting of Pure Type Systems in which normalization does imply decidability of type checking. The result is folklore, but non-trivial, since a strategy for when to apply the conversion rule needs to be found. The obvious strategy is to normalize inferred types before all applications of the application rule. There are some subtleties even here, where the correctness of a natural (more efficient) strategy called expansion postponment was open for a while, but has been settled since.

There are type systems which are normalizing but undecidable, most notably the system with intersection types which types exactly the normalizing terms, and so must be undecidable (since otherwise it could be used to identify normalizing terms). It would be tempting to say here that the system is defective in the sense that it is not type directed, i.e. the terms do not contain enough information to figure out the type.

Now the converse, which would suggest non-normalizing systems are undecidable, is far from obvious: it was even open for a while for the famous $Type:Type$ system of Martin-Löf! This case was solved by giving an example of a looping combinator, which allows writing arbitrary computations.

However the general problem is still open for general pure type systems, though it is widely believed to be true, and some partial results have been shown in this direction, e.g. here.

Improve this answer
$\endgroup$
2
  • $\begingroup$ Thanks for your answer. What about decidability of typability? $\endgroup$
    – user40276
    Commented May 2, 2017 at 3:59
  • 1
    $\begingroup$ @user40276 this is a pretty different question. With annotations on the abstractions, typeability and type-inference are equally hard. Without annotations, things get undecidable almost immediately, regardless of termination, as explained in the answers here: cs.stackexchange.com/questions/12691/… $\endgroup$
    – cody
    Commented May 2, 2017 at 13:14
4
$\begingroup$

(1) False. Counter example: Java, Scala, Haskell, ...

(2) No general relations hold, really depends on the details of the language/typing system. There is one exception: for sane languages and typing systems, I imagine that decidability of type inference (which I assume is what you mean by "typability") trivially implies type-checking. But I would not be surprised if one could concoct a crazy system where even that implication doesn't hold.

Improve this answer
$\endgroup$
6
  • $\begingroup$ Thanks for your answer. Typability refers to the process of finding a type such that a term belongs to it and not all these types. $\endgroup$
    – user40276
    Commented May 2, 2017 at 3:55
  • $\begingroup$ How does this relate to the conventional concept of type-inference? $\endgroup$
    – Martin Berger
    Commented May 2, 2017 at 8:20
  • $\begingroup$ A specific example where decidable type-inference does not entail decidable type-checking: rank-2 polymorphic lambda calculus. There exist inference algorithms for this language, however they are not stable under the addition of type signatures. That is, we do not have that Γ⊢a:A entails Γ⊢(a::A):A where I'm using :: for the object-language's phrasing of "a has type A". Thus, even though we can infer A for a, we cannot always check a against A. $\endgroup$
    – wren romano
    Commented May 3, 2017 at 5:41
  • $\begingroup$ @wrenromano Interesting. System F has undecidable inference and checking, and rank-2 polymorphic lambda calculus is a subsystem (of sorts). Have you got a reference for this phenomenon? $\endgroup$
    – Martin Berger
    Commented May 3, 2017 at 13:50
  • $\begingroup$ Sorry. My comment is wrong as I have written, it should be: "Typability refers to the process of finding a type such that the given term belongs to it and not all these types". Decidability of type-inference implies decidability of typability. I'm almost sure that the reciprocal assertion does not hold, but I'm not aware of a counter-example. $\endgroup$
    – user40276
    Commented May 4, 2017 at 1:24

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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