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

<p>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: <a href="https://stackoverflow.com/questions/1936432/higher-order-unification">https://stackoverflow.com/questions/1936432/higher-order-unification</a>.</p>

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

CC BY-SA 4.0
2019-02-26T23:34:13.107Z
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.
user833970
CC BY-SA 4.0
2019-02-15T19:59:33.520Z
2019-02-15T22:11:21.667Z
2019-02-15T22:11:21.667Z
user833970
<p>Given the usual Calculus of Constructions with an extra primitive, <code>_</code>, 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:</p>

<pre><code>λ (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 _)
</code></pre>

<p>The algorithm would replace <code>_</code> by <code>(B (S (S (S Z))))</code>,  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).</p>

<type-theory><calculus-of-constructions><proof-search>
Is there a simple algorithm for proof search on CoC?
MaiaVictor
# Is there a simple algorithm for proof search on CoC?

(Asked by: username_0 on 2019-02-15)

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).

**Tags:** type-theory, calculus-of-constructions, proof-search


---

## 1 answers

### Answer by username_1 on 2019-02-15. Score: 5 | Accepted answer

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.

> **Comments:**
> **username_1**: 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.  

---

