3
$\begingroup$

Given the usual Calculus of Constructions with an extra primitive, _, that stands for "attempt to fill this location in a way that type-checks", is there any simple/elegant algorithm capable of solving this problem for a large class of terms? For example, given the term below:

λ (N : Type)
λ (S : {x : N} N)
λ (Z : N)
λ (A : {x : N} Type)
λ (B : {x : N} (A x))
λ (C : {x : (A (S (S (S Z))))} Type)
(C _)

The algorithm would replace _ by (B (S (S (S Z)))), as it is the only substitution that makes the resulting term well-typed. I'm specifically looking for keywords / references, as I believe this is a pretty well-researched subject (given that most theorem provers feature proof search), but I've never seen an algorithm described in a simpler setup (like plain CoC).

$\endgroup$
4
$\begingroup$

Is there a simple algorithm? yes. Simply enumerate all possibilities. Of course this is pretty intractable in practice.

A proper sub-problem of term generation in CoC is "higher-order unification". It handles the simply typed lambda calculus. It is undecidable. But there is a classic practical solution by Huet. There are a lot of resources here: https://stackoverflow.com/questions/1936432/higher-order-unification.

Now the only good reference I know for CoC term generation is "A Complete Proof Synthesis Method for the Cube of Type Systems" by Dowek. I believe this summarizes his thesis work (in french) and there is a draft pdf floating around (it has some errors). His r-splitting construction is a little awkward for implementations, but he does a good job of highlighting the difficulties, and suggesting practical in-complete solutions.

$\endgroup$
  • $\begingroup$ forgot to add I have a bad haskell implementation of some of the paper. I wouldn't want to make it public in it's current state but am happy to share it privately. $\endgroup$ – user833970 Feb 26 at 23:34

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.