On the complexity of stratified logics

TL;DR

This paper compares two logical and algebraic frameworks, ILAL and SRN, used to characterize polynomial time computable functions, highlighting their shared principles and differences.

Contribution

It analyzes the common principles underlying stratification in ILAL and predicative recursion in SRN, providing insights into their relationship.

Findings

ILAL captures FPTIME via stratification.

SRN characterizes FPTIME through safe recursion.

Shared principles underlie stratification and predicative recursion.

Abstract

Our primary motivation is the comparison of two different traditions used in ICC to characterize the class FPTIME of the polynomial time computable functions. On one side, FPTIME can be captured by Intuitionistic Light Affine Logic (ILAL), a logic derived from Linear Logic, characterized by the structural invariant Stratification. On the other side, FPTIME can be captured by Safe Recursion on Notation (SRN), an algebra of functions based on Predicative Recursion, a restriction of the standard recursion schema used to defiine primitive recursive functions. Stratifiication and Predicative Recursion seem to share common underlying principles, whose study is the main subject of this work.