1
$\begingroup$

I'm wondering if type inhabitance for the calculus of constructions is semi-decideable. I know the following:

  1. System F inhabitance and, correspondingly, second-order unification are semi-decideable
  2. Higher-order unification is at least as hard as second order unification
  3. Folk knowledge holds that higher-order untyped unification is semi-decideable (I haven't found any concrete sources for this)
  4. CoC is a higher-order full dependently-typed logic
  5. Some simpler restrictive dependently typed higher-order logics have decidable type inhabitance

I don't know what is true about inhabitance in CoC. I don't know how dependent types with no restrictions impact semidecidability. This feels to me like it should be an obvious question, but hours of searching and talking to other PL researchers today gave me nothing but different accounts of people's intuition, with nothing concrete.

$\endgroup$
  • 6
    $\begingroup$ Yes: just enumerate the raw terms and use decidability of type checking. $\endgroup$ – Ulrik Buchholtz Jan 13 '18 at 9:24
  • 1
    $\begingroup$ (Even systems of dependent type theory with equality reflection have semi-decidable type inhabitance: since type checking is then semi-decidable, you can interleave type checking with term enumeration.) $\endgroup$ – Ulrik Buchholtz Jan 13 '18 at 9:26
  • $\begingroup$ But how can you enumerate all terms in an order that is guaranteed to terminate if one is well-typed? There are many orders in which you can enumerate and you could go on infinitely in some orders if you proceed naively (for example, by applying the rule for product types over and over again). $\endgroup$ – Lambda Pi Omega Jan 13 '18 at 15:49
  • 2
    $\begingroup$ You mean: how do you ensure that it's actually an enumeration? Well, the raw terms are given by a context free grammar, so standard techniques work. Your mention of rules suggests an alternative strategy to prove semi-decidability of type inhabitance: enumerate derivable judgments. That also works, but as usual we have to ensure that all rules are tried infinitely often. Again, that's a standard technique. $\endgroup$ – Ulrik Buchholtz Jan 13 '18 at 15:56
  • $\begingroup$ Ok, thanks! Do you know if there's any practical reason a generalization of Huet's doesn't exist (AFAIK) in a CoC context? $\endgroup$ – Lambda Pi Omega Jan 13 '18 at 15:59
2
$\begingroup$

As a rule of thumb, take any formal system $\cal S$ which can be described as a finite (or recursively enumerable) set of rules of the form

$$\frac{P_1\quad \ldots \quad P_n}{C} $$

and suppose that it is decidable whether or not a concrete tuple of formulae (or terms, or typing judgements...) $\phi_1,\ldots,\phi_n, \psi$ is an instance of one of these rules.

Then the following theorem holds:

The set of $\cal T$ of derivable conclusions of $\cal S$ is recursively enumerable.

The proof simply describes a way of enumerating all well-formed derivation trees. In particular in this setting it is semi-decidable whether any conclusion is derivable, and with a tiny bit more work one can describe the type inhabitation problem of any reasonable type system.

$\endgroup$

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

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