A Partial Metric Semantics of Higher-Order Types and Approximate Program Transformations
| Autor: | Geoffroy, Guillaume, Pistone, Paolo |
|---|---|
| Přispěvatelé: | Alma Mater Studiorum Università di Bologna [Bologna] (UNIBO), Foundations of Component-based Ubiquitous Systems (FOCUS), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Dipartimento di Informatica - Scienza e Ingegneria [Bologna] (DISI), Alma Mater Studiorum Università di Bologna [Bologna] (UNIBO)-Alma Mater Studiorum Università di Bologna [Bologna] (UNIBO), ANR-16-CE25-0011,REPAS,Des systèmes logiciels fiables et conscients des données privées, via les métriques de bisimulation(2016), European Project: 818616,H2020-EU.1.1. - EXCELLENT SCIENCE - European Research Council (ERC),DIAPASoN(2019), European Project: 818616,DIAPASoN, Alma Mater Studiorum University of Bologna (UNIBO), Baier, Christel, Goubault-Larrecq, Jean, Geoffroy G., Pistone P. |
| Rok vydání: | 2021 |
| Předmět: |
060201 languages & linguistics
Program metric [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL] Partial metric space partial metric spaces [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] 06 humanities and the arts 02 engineering and technology Theory of computation → Denotational semantics approximate program transformations simply typed λ-calculus 0602 languages and literature program metrics 0202 electrical engineering electronic engineering information engineering Computer Science::Programming Languages 020201 artificial intelligence & image processing [INFO]Computer Science [cs] Approximate program transformation |
| Zdroj: | Proceedings of CSL 2021, 29th EACSL Annual Conference on Computer Science Logic CSL 2021-Computer Science Logic CSL 2021-Computer Science Logic, Jan 2021, Lubjana, Slovenia. ⟨10.4230/LIPIcs.CSL.2021.23⟩ Computer Science Logic, CSL 2021 Computer Science Logic, CSL 2021, Jan 2021, Lubjana, Slovenia |
| DOI: | 10.4230/lipics.csl.2021.23 |
| Popis: | 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 higher-order types in a novel way, yielding a metric semantics of the simply typed lambda-calculus in which types are interpreted as quantale-valued partial metric spaces. Using such metrics we define a class of higher-order denotational models, called diameter space models, that provide a quantitative semantics of approximate program transformations. Noticeably, the distances between objects of higher-types are elements of functional, thus non-numerical, quantales. This allows us to model contextual reasoning about arbitrary functions, thus deviating from classic metric semantics. LIPIcs, Vol. 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021), pages 23:1-23:18 |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|