University of Cambridge

Logic
&
Semantics

Linear types and non-size increasing polynomial time computation

By Martin Hofmann (20th November 1998)

Recent work has shown that predicative recursion combined with a linear typing discipline gives rise to type systems which guarantee polynomial runtime of well-typed programs while allowing for higher-typed primitive recursion on inductive datatypes.

Although these systems allow one to express all polynomial time functions they reject many natural formulations of obviously polynomial time algorithms. The reason is that under the predicativity regime a recursively defined function is not allowed to serve as step function of a subsequent recursive definition. However, in most functional programs involving inductive data structures such iterated recursion does occur. A typical example is insertion sort which involves iteration of a (already recursively defined) insertion function. A closer analysis of such examples reveals that the involved functions do not increase the size of their input and that this is why their repeated iteration does not lead beyond polynomial time.

In this work we present a new linear type system based on this intuition. It boasts unrestricted higher-order recursion operators for inductive datatypes such as integers, lists, and trees, yet ensures polynomial runtime of all first-order programs.

Although the system only contains non-size-increasing functions (and thus not all of PTIME) it is astonishingly expressive; for example familiar sorting algorithms like insertion sort and tree sort are all well-typed in their natural form.

Apart from its intended purpose the type system might also have applications to constant space computation as is required for example in embedded systems.

The proof of the correctness of the type system is based on a semantic model for the system which also suggests the fine points of its design. After motivating examples the talk will concentrate on the construction and verification of this semantic model.

LS Home page or Talks in 1998/99