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

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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsDigital Image Processing Techniques · Advanced Numerical Analysis Techniques · Advanced Banach Space Theory
