Geoffroy, Guillaume ;
Pistone, Paolo
A Partial Metric Semantics of HigherOrder Types and Approximate Program Transformations
Abstract
Program semantics is traditionally concerned with program equivalence. However, in fields like approximate, incremental and probabilistic computation, it is often useful to describe to which extent two programs behave in a similar, although non equivalent way. This has motivated the study of program (pseudo)metrics, which have found widespread applications, e.g. in differential privacy. In this paper we show that the standard metric on real numbers can be lifted to higherorder types in a novel way, yielding a metric semantics of the simply typed lambdacalculus in which types are interpreted as quantalevalued partial metric spaces. Using such metrics we define a class of higherorder denotational models, called diameter space models, that provide a quantitative semantics of approximate program transformations. Noticeably, the distances between objects of highertypes are elements of functional, thus nonnumerical, quantales. This allows us to model contextual reasoning about arbitrary functions, thus deviating from classic metric semantics.
BibTeX  Entry
@InProceedings{geoffroy_et_al:LIPIcs:2021:13457,
author = {Guillaume Geoffroy and Paolo Pistone},
title = {{A Partial Metric Semantics of HigherOrder Types and Approximate Program Transformations}},
booktitle = {29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
pages = {23:123:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959771757},
ISSN = {18688969},
year = {2021},
volume = {183},
editor = {Christel Baier and Jean GoubaultLarrecq},
publisher = {Schloss DagstuhlLeibnizZentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2021/13457},
URN = {urn:nbn:de:0030drops134578},
doi = {10.4230/LIPIcs.CSL.2021.23},
annote = {Keywords: Simply typed λcalculus, program metrics, approximate program transformations, partial metric spaces}
}
13.01.2021
Keywords: 

Simply typed λcalculus, program metrics, approximate program transformations, partial metric spaces 
Seminar: 

29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

Issue date: 

2021 
Date of publication: 

13.01.2021 