Complexity Analysis for Call-by-Value Higher-Order Rewriting

TL;DR

This paper introduces a complexity analysis framework for call-by-value higher-order rewriting, using algebraic interpretations to bound reduction costs and normal form sizes, aiding in understanding program efficiency.

Contribution

It presents a novel cost-size semantics for call-by-value rewriting based on algebraic interpretations, bridging a gap in complexity analysis for higher-order programs.

Findings

Provides a formal semantics for call-by-value rewriting

Establishes bounds on reduction costs and normal form sizes

Lays groundwork for complexity analysis in higher-order rewriting systems

Abstract

In this short paper, we consider a form of higher-order rewriting with a call-by-value evaluation strategy so as to model call-by-value programs. We briefly present a cost-size semantics to call-by-value rewriting: a class of algebraic interpretations that map terms to tuples that bound both the reductions' cost and the size of normal forms.