8
$\begingroup$

Is there a type system, which restricts the lambda terms to the terms which fall inside a complexity class? Like the typable terms in the theory are strictly inside the complexity class ? Or is it not possible at all?

I find the there are lot of studies on expressibility of the type theory, like provably terminating, extended polynomials etc.. But is there any way to restrict that to a complexity class?

Improve this question
$\endgroup$
1
  • 1
    $\begingroup$ This topic is part of the area of Implicit Computational Complexity, where there are lots of results of that type. Type systems considered there are "ramified types" or variants of linear logic, e.g. Light Affine Logic or Soft Affine Logic. $\endgroup$
    – Jan Johannsen
    Oct 25, 2018 at 11:19

1 Answer 1

Reset to default
10
$\begingroup$

The keywords you are looking for are "Implicit Computational Complexity". The field studies for instance variants of linear logic and the complexity bounds they can guarantee on the terms underlying the derivations.

Improve this answer
$\endgroup$
2
  • 1
    $\begingroup$ Do you have any nice reference for the same? I would really like to understand this better? $\endgroup$
    – Vinothkumar Raman
    Oct 25, 2018 at 15:27
  • 1
    $\begingroup$ @VinothkumarRaman I would look for the work of (Martin) Hofmann and (Jan) Hoffmann. $\endgroup$
    – xrq
    Oct 26, 2018 at 4:18

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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