The Geometry of Linear Higher-Order Recursion

TL;DR

This paper explores how adjusting linearity and ramification constraints affects the expressive power of higher-order recursion, introducing algebraic context semantics to analyze normalization beyond polynomial time.

Contribution

It introduces algebraic context semantics as a new framework to analyze the expressive strength of higher-order recursion under different constraints.

Findings

Different constraints lead to varying expressive powers, some beyond polynomial time.

Algebraic context semantics effectively analyzes normalization in higher-order recursion.

Framework extends Gonthier's work to quantify recursion complexity.

Abstract

Linearity and ramification constraints have been widely used to weaken higher-order (primitive) recursion in such a way that the class of representable functions equals the class of polytime functions. We show that fine-tuning these two constraints leads to different expressive strengths, some of them lying well beyond polynomial time. This is done by introducing a new semantics, called algebraic context semantics. The framework stems from Gonthier's original work and turns out to be a versatile and powerful tool for the quantitative analysis of normalization in presence of constants and higher-order recursion.