7
$\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
    $\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 '18 at 11:19
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$
  • 1
    $\begingroup$ Do you have any nice reference for the same? I would really like to understand this better? $\endgroup$ – Vinothkumar Raman Oct 25 '18 at 15:27
  • 1
    $\begingroup$ @VinothkumarRaman I would look for the work of (Martin) Hofmann and (Jan) Hoffmann. $\endgroup$ – xuq01 Oct 26 '18 at 4:18

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

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