A generic imperative language for polynomial time

TL;DR

This paper introduces a novel ramification method for imperative programming that extends the concept of implicit computational complexity to finite structures, bridging type theory and static analysis.

Contribution

It presents a new ramification approach that adapts to general imperative programming by focusing on finite structures, linking implicit complexity with data-flow analysis.

Findings

The new ramification method applies to finite structures.

It bridges implicit complexity and static data-flow analysis.

It enables polynomial-time guarantees for imperative programs.

Abstract

The ramification method in Implicit Computational Complexity has been associated with functional programming, but adapting it to generic imperative programming is highly desirable, given the wider algorithmic applicability of imperative programming. We introduce a new approach to ramification which, among other benefits, adapts readily to fully general imperative programming. The novelty is in ramifying finite second-order objects, namely finite structures, rather than ramifying elements of free algebras. In so doing we bridge between Implicit Complexity's type theoretic characterizations of feasibility, and the data-flow approach of Static Analysis.