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?

$\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$ Oct 25, 2018 at 11:19

1 Answer 1

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.

$\endgroup$
2
  • 1
    $\begingroup$ Do you have any nice reference for the same? I would really like to understand this better? $\endgroup$ 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, privacy policy and cookie policy

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