On Quantitative Algebraic Higher-Order Theories

TL;DR

This paper extends the framework of quantitative algebras to structures from combinatory logic and lambda calculus, establishing soundness, completeness, and exploring limitations of metric space models.

Contribution

It demonstrates the applicability of quantitative algebraic theories to higher-order structures and provides new examples and limitations of such models.

Findings

Framework applicable to lambda calculus structures

Soundness and completeness results established

Identified limitations of metric space models

Abstract

We explore the possibility of extending Mardare et al. quantitative algebras to the structures which naturally emerge from Combinatory Logic and the lambda-calculus. First of all, we show that the framework is indeed applicable to those structures, and give soundness and completeness results. Then, we prove some negative results which clearly delineate to which extent categories of metric spaces can be models of such theories. We conclude by giving several examples of non-trivial higher-order quantitative algebras.