On Generalized Metric Spaces for the Simply Typed Lambda-Calculus (Extended Version)

TL;DR

This paper introduces a new approach to applying generalized metric spaces to the simply typed lambda calculus, extending Euclidean metrics to higher-order types via a quantitative semantics based on generalized logical relations.

Contribution

It develops a novel construction of cartesian closed categories of generalized metric spaces tailored for higher-order languages.

Findings

Extended Euclidean metric to all higher-order types.

New categorical framework for generalized metrics in lambda calculus.

Enhanced understanding of program similarity measures.

Abstract

Generalized metrics, arising from Lawvere's view of metric spaces as enriched categories, have been widely applied in denotational semantics as a way to measure to which extent two programs behave in a similar, although non equivalent, way. However, the application of generalized metrics to higher-order languages like the simply typed lambda calculus has so far proved unsatisfactory. In this paper we investigate a new approach to the construction of cartesian closed categories of generalized metric spaces. Our starting point is a quantitative semantics based on a generalization of usual logical relations. Within this setting, we show that several families of generalized metrics provide ways to extend the Euclidean metric to all higher-order types.