<p>Type inference for simply typed lambda calculus is complete for polynomial time, as elegantly explained in section 1 of Harry Mairson's <a href="https://www.cs.brandeis.edu/%7Emairson/Papers/jfp02.pdf" rel="noreferrer">Linear lambda calculus and PTIME-completeness</a>.</p>
<p>To be a bit more precise, here &quot;type inference&quot; is taken to mean the problem of computing the principal simple type of an untyped lambda term. This is strictly speaking a functional problem (&quot;Given a term <span class="math-container">$t$</span>, compute its principal type&quot;), but Mairson shows that the corresponding decision problem (&quot;Given a term <span class="math-container">$t$</span> and type <span class="math-container">$A$</span>, is <span class="math-container">$A$</span> the principal type of <span class="math-container">$t$</span>?&quot;) is PTIME-hard, by reduction from the circuit value problem.  This implies PTIME-completeness, since simple type inference can be performed efficiently using first-order unification.  Moreover, Mairson's encoding of the circuit value problem has the property that the terms representing boolean circuits are affine (variables used at most once), and in Section 2 of the paper he gives another encoding that produces linear terms (variables used exactly once).  So his proof implies PTIME-completeness of simple type inference even when restricted to affine/linear lambda terms.</p>

CC BY-SA 4.0
2021-12-02T23:00:48.077Z
what does it mean that it "is complete for polynomial time"? Or PTIME-completness? Intuitively it feels trivial to compose the type...just go through the typing rules from the top and apply them recursively in the structure of the formula until you form the type. This seems linear in the length of lambda term $O(n)$ is it not?
Charlie Parker
CC BY-SA 4.0
2021-12-20T19:15:36.740Z
@CharlieParker If your program has type annotations for variables (as in your other question), you're not doing type inference; if the program has no type annotations, the trivial answer does not work any more.
Blaisorblade
CC BY-SA 4.0
2020-10-02T07:21:45.630Z
2020-10-02T07:21:45.630Z
Noam Zeilberger
<p>A similar question was answered here:
<a href="https://cstheory.stackexchange.com/questions/38556/is-simply-typed-lambda-calculus-equivalent-to-primitive-recursive-functions">Is simply typed lambda calculus equivalent to primitive recursive functions</a></p>
<p>What I conclude from the answers is that the complexity is that of the extended polynomials, but this refers to what can be computed in the STLC, not of type checking expressions in the STLC.</p>
<p>This <a href="https://softwarefoundations.cis.upenn.edu/plf-current/Typechecking.html" rel="noreferrer">link</a> provides an algorithm for type-checking. It is claimed that
type checking is linear time in an answer to this question: <a href="https://cstheory.stackexchange.com/questions/41362/complexity-of-type-checking-in-relation-to-complexity-of-normalization">Complexity of type-checking in relation to complexity of normalization</a></p>
<p>Also, a survey of algorithms that do type inference for STLC, using unification occurs here, but no complexity result is given.</p>

CC BY-SA 4.0
2021-12-02T23:01:02.533Z
what does it mean that it "is complete for polynomial time"? Or PTIME-completness? Intuitively it feels trivial to compose the type...just go through the typing rules from the top and apply them recursively in the structure of the formula until you form the type. This seems linear in the length of lambda term $O(n)$ is it not?
Charlie Parker
CC BY-SA 4.0
2021-12-20T17:46:28.563Z
related: https://cs.stackexchange.com/questions/147810/what-is-the-runtime-of-type-inference-in-simply-typed-lambda-calculus
Charlie Parker
CC BY-SA 4.0
2021-12-21T07:50:21.557Z
@CharlieParker See https://en.wikipedia.org/wiki/P-complete . Please ask such basic terminology questions on https://cs.stackexchange.com , not here.
Emil Jeřábek
<complexity-classes><typed-lambda-calculus>
Complexity of type inference in the simply typed lambda calculus
Yossi Gil
# Complexity of type inference in the simply typed lambda calculus

(Asked by: username_0 on 2020-09-29)

A similar question was answered here:
[Is simply typed lambda calculus equivalent to primitive recursive functions](https://cstheory.stackexchange.com/questions/38556/is-simply-typed-lambda-calculus-equivalent-to-primitive-recursive-functions)

What I conclude from the answers is that the complexity is that of the extended polynomials, but this refers to what can be computed in the STLC, not of type checking expressions in the STLC.

This [link](https://softwarefoundations.cis.upenn.edu/plf-current/Typechecking.html) provides an algorithm for type-checking. It is claimed that
type checking is linear time in an answer to this question: [Complexity of type-checking in relation to complexity of normalization](https://cstheory.stackexchange.com/questions/41362/complexity-of-type-checking-in-relation-to-complexity-of-normalization)

Also, a survey of algorithms that do type inference for STLC, using unification occurs here, but no complexity result is given.

**Tags:** complexity-classes, typed-lambda-calculus
> **Comments:**
> **username_1**: what does it mean that it "is complete for polynomial time"? Or PTIME-completness? Intuitively it feels trivial to compose the type...just go through the typing rules from the top and apply them recursively in the structure of the formula until you form the type. This seems linear in the length of lambda term $O(n)$ is it not?  
> **username_1**: related: https://cs.stackexchange.com/questions/147810/what-is-the-runtime-of-type-inference-in-simply-typed-lambda-calculus  
> **username_2**: @CharlieParker See https://en.wikipedia.org/wiki/P-complete . Please ask such basic terminology questions on https://cs.stackexchange.com , not here.  

---

## 1 answers

### Answer by username_3 on 2020-10-02. Score: 8 | Accepted answer

Type inference for simply typed lambda calculus is complete for polynomial time, as elegantly explained in section 1 of Harry Mairson's [Linear lambda calculus and PTIME-completeness](https://www.cs.brandeis.edu/%7Emairson/Papers/jfp02.pdf).

To be a bit more precise, here "type inference" is taken to mean the problem of computing the principal simple type of an untyped lambda term. This is strictly speaking a functional problem ("Given a term $t$, compute its principal type"), but Mairson shows that the corresponding decision problem ("Given a term $t$ and type $A$, is $A$ the principal type of $t$?") is PTIME-hard, by reduction from the circuit value problem. This implies PTIME-completeness, since simple type inference can be performed efficiently using first-order unification. Moreover, Mairson's encoding of the circuit value problem has the property that the terms representing boolean circuits are affine (variables used at most once), and in Section 2 of the paper he gives another encoding that produces linear terms (variables used exactly once). So his proof implies PTIME-completeness of simple type inference even when restricted to affine/linear lambda terms.

> **Comments:**
> **username_1**: what does it mean that it "is complete for polynomial time"? Or PTIME-completness? Intuitively it feels trivial to compose the type...just go through the typing rules from the top and apply them recursively in the structure of the formula until you form the type. This seems linear in the length of lambda term $O(n)$ is it not?  
> **username_4**: @CharlieParker If your program has type annotations for variables (as in your other question), you're not doing type inference; if the program has no type annotations, the trivial answer does not work any more.  

---

