3
$\begingroup$

A similar question was answered here: 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 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

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

Improve this question
$\endgroup$
3
  • $\begingroup$ 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? $\endgroup$
    – Charlie Parker
    Dec 2, 2021 at 23:01
  • $\begingroup$ related: cs.stackexchange.com/questions/147810/… $\endgroup$
    – Charlie Parker
    Dec 20, 2021 at 17:46
  • $\begingroup$ @CharlieParker See en.wikipedia.org/wiki/P-complete . Please ask such basic terminology questions on cs.stackexchange.com , not here. $\endgroup$
    – Emil Jeřábek
    Dec 21, 2021 at 7:50

1 Answer 1

Reset to default
6
$\begingroup$

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.

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.

Improve this answer
$\endgroup$
2
  • 1
    $\begingroup$ 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? $\endgroup$
    – Charlie Parker
    Dec 2, 2021 at 23:00
  • 1
    $\begingroup$ @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. $\endgroup$
    – Blaisorblade
    Dec 20, 2021 at 19:15

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.