A type assignment for lambda-calculus complete both for FPTIME and strong normalization

TL;DR

This paper introduces STR, a stratified type system for lambda-calculus that guarantees polynomial time computation and strong normalization, enhancing expressivity over previous systems.

Contribution

The paper presents STR, a novel stratified type system for lambda-calculus that is both correct and complete for polynomial time and includes typing for strongly normalizing terms.

Findings

STR is correct and complete for polynomial time computations.

All strongly normalizing terms are typable in STR.

STR allows typing of a restricted form of iteration, increasing expressivity.

Abstract

One of the aims of Implicit Computational Complexity is the design of programming languages with bounded computational complexity; indeed, guaranteeing and certifying a limited resources usage is of central importance for various aspects of computer science. One of the more promising approaches to this aim is based on the use of lambda-calculus as paradigmatic programming language and the design of type assignment systems for lambda-terms, where types guarantee both the functional correctness and the complexity bound. Here we propose a system of stratified types, inspired by intersection types, where intersection is a non-associative operator. The system, called STR, is correct and complete for polynomial time computations; moreover, all the strongly normalizing terms are typed in it, thus increasing the typing power with respect to the previous proposals. Moreover, STR enjoys a stronger expressivity with respect to the previous system STA, since it allows to type a restricted version of iteration.