Formalizing Termination Proofs under Polynomial Quasi-interpretations

TL;DR

This paper formalizes termination proofs for certain functional programs using minimal function graphs, showing they can be performed within polynomial space and establishing a connection to polynomial-time computability.

Contribution

It introduces a novel formalization of termination proofs via minimal function graphs for LPO-terminating, polynomially quasi-interpretable programs, linking them to polynomial space complexity.

Findings

Termination proofs are formalized in a weak Peano arithmetic fragment.

Programs with LPO termination and polynomial quasi-interpretations compute in polynomial space.

Every polynomial-space computable function can be represented by such programs.

Abstract

Usual termination proofs for a functional program require to check all the possible reduction paths. Due to an exponential gap between the height and size of such the reduction tree, no naive formalization of termination proofs yields a connection to the polynomial complexity of the given program. We solve this problem employing the notion of minimal function graph, a set of pairs of a term and its normal form, which is defined as the least fixed point of a monotone operator. We show that termination proofs for programs reducing under lexicographic path orders (LPOs for short) and polynomially quasi-interpretable can be optimally performed in a weak fragment of Peano arithmetic. This yields an alternative proof of the fact that every function computed by an LPO-terminating, polynomially quasi-interpretable program is computable in polynomial space. The formalization is indeed optimal since every polynomial-space computable function can be computed by such a program. The crucial observation is that inductive definitions of minimal function graphs under LPO-terminating programs can be approximated with transfinite induction along LPOs.