More Web Proxy on the site http://driver.im/

research-article

Public Access

A semantic account of metric preservation

Authors:

Arthur Azevedo de Amorim,

Marco Gaboardi,

Shin-ya Katsumata,

Ikram CheriguiAuthors Info & Claims

ACM SIGPLAN Notices, Volume 52, Issue 1

Pages 545 - 556

https://doi.org/10.1145/3093333.3009890

Published: 01 January 2017 Publication History

Abstract

Program sensitivity measures how robust a program is to small changes in its input, and is a fundamental notion in domains ranging from differential privacy to cyber-physical systems. A natural way to formalize program sensitivity is in terms of metrics on the input and output spaces, requiring that an r-sensitive function map inputs that are at distance d to outputs that are at distance at most r · d. Program sensitivity is thus an analogue of Lipschitz continuity for programs.

Reed and Pierce introduced Fuzz, a functional language with a linear type system that can express program sensitivity. They show soundness operationally, in the form of a metric preservation property. Inspired by their work, we study program sensitivity and metric preservation from a denotational point of view. In particular, we introduce metric CPOs, a novel semantic structure for reasoning about computation on metric spaces, by endowing CPOs with a compatible notion of distance. This structure is useful for reasoning about metric properties of programs, and specifically about program sensitivity. We demonstrate metric CPOs by giving a model for the deterministic fragment of Fuzz.

References

[1]

M. Abadi and G. D. Plotkin. A PER model of polymorphism and recursive types. In IEEE Symposium on Logic in Computer Science (LICS), Philadelphia, Pennsylvania, pages 355–365, 1990.

[2]

M. Abadi, B. C. Pierce, and G. D. Plotkin. Faithful ideal models for recursive polymorphic types. In IEEE Symposium on Logic in Computer Science (LICS), Asilomar, California, pages 216–225, 1989.

Digital Library

[3]

R. M. Amadio. Recursion over realizability structures. Information and Computation, 91(1):55–85, 1991.

Digital Library

[4]

P. America and J. J. M. M. Rutten. Solving reflexive domain equations in a category of complete metric spaces. In Workshop on the Mathematical Foundations of Programming Semantics (MFPS), New Orleans, Louisiana, volume 298 of Lecture Notes in Computer Science, pages 254–288. Springer-Verlag, 1987.

Digital Library

[5]

A. Arnold and M. Nivat. Metric interpretations of infinite trees and semantics of non-deterministic recursive programs. Theoretical Computer Science, 11(2):181–205, 1980.

[6]

C. Baier and M. Z. Kwiatkowska. Domain equations for probabilistic processes. Electronic Notes in Theoretical Computer Science, 7:34–54, 1997.

[7]

C. Baier and M. E. Majster-Cederbaum. Denotational semantics in the CPO and metric approach. Theoretical Computer Science, 135(2): 171–220, 1994.

Digital Library

[8]

G. Barthe, B. Köpf, F. Olmedo, and S. Zanella Béguelin. Probabilistic relational reasoning for differential privacy. In ACM SIGPLAN– SIGACT Symposium on Principles of Programming Languages (POPL), Philadelphia, Pennsylvania, pages 97–110, 2012.

Digital Library

[9]

G. Barthe, M. Gaboardi, E. J. Gallego Arias, J. Hsu, A. Roth, and P.-Y. Strub. Higher-order approximate relational refinement types for mechanism design and differential privacy. In ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL), Mumbai, India, pages 55–68, 2015.

Digital Library

[10]

L. Birkedal, K. Støvring, and J. Thamsborg. Realizability semantics of parametric polymorphism, general references, and recursive types. In International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), York, England, volume 5504 of Lecture Notes in Computer Science, pages 456–470. Springer-Verlag, 2009.

[11]

L. Birkedal, K. Støvring, and J. Thamsborg. The category-theoretic solution of recursive metric-space equations. Theoretical Computer Science, 411(47):4102–4122, 2010.

Digital Library

[12]

L. Birkedal, R. E. Møgelberg, J. Schwinghammer, and K. Støvring. First steps in synthetic guarded domain theory: Step-indexing in the topos of trees. In IEEE Symposium on Logic in Computer Science (LICS), Toronto, Ontario, pages 55–64, 2011.

Digital Library

[13]

S. Chaudhuri, S. Gulwani, and R. Lublinerman. Continuity analysis of programs. In ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL), Madrid, Spain, pages 57–70, 2010.

Digital Library

[14]

S. Chaudhuri, S. Gulwani, R. Lublinerman, and S. NavidPour. Proving programs robust. In Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE), Szeged, Hungary, pages 102–112, 2011.

Digital Library

[15]

S. Chaudhuri, S. Gulwani, and R. Lublinerman. Continuity and robustness of programs. Communications of the ACM, 55(8):107–115, 2012.

Digital Library

[16]

J. Chroboczek. Subtyping recursive games. In International Conference on Typed Lambda Calculi and Applications (TLCA), Kraków, Poland, volume 2044 of Lecture Notes in Computer Science, pages 61–75. Springer-Verlag, 2001.

Digital Library

[17]

I. Csiszár and P. C. Shields. Information theory and statistics: A tutorial. Foundations and Trends® in Communications and Information Theory, 1(4):417–528, 2004.

Digital Library

[18]

J. W. de Bakker and J. I. Zucker. Denotational semantics of concurrency. In ACM SIGACT Symposium on Theory of Computing (STOC), San Francisco, California, pages 153–158, 1982.

Digital Library

[19]

E. P. de Vink and J. J. M. M. Rutten. Bisimulation for probabilistic transition systems: A coalgebraic approach. Theoretical Computer Science, 221(1–2):271–293, 1999.

Digital Library

[20]

J. den Hartog, E. P. de Vink, and J. W. de Bakker. Metric semantics and full abstractness for action refinement and probabilistic choice. Electronic Notes in Theoretical Computer Science, 40:72–99, 2000.

[21]

J. Desharnais, R. Jagadeesan, V. Gupta, and P. Panangaden. The metric analogue of weak bisimulation for probabilistic processes. In IEEE Symposium on Logic in Computer Science (LICS), Copenhagen, Denmark, pages 413–422, 2002.

Digital Library

[22]

C. Dwork, F. McSherry, K. Nissim, and A. D. Smith. Calibrating noise to sensitivity in private data analysis. In IACR Theory of Cryptography Conference (TCC), New York, New York, volume 3876 of Lecture Notes in Computer Science, pages 265–284. Springer-Verlag, 2006.

Digital Library

[23]

M. H. Escardó. A metric model of PCF, 1999. Workshop on Realizability Semantics and Applications, Trento, Italy.

[24]

M. P. Fiore and G. D. Plotkin. An axiomatization of computationally adequate domain theoretic models of FPC. In IEEE Symposium on Logic in Computer Science (LICS), Paris, France, pages 92–102, 1994.

[25]

P. Freyd. Algebraically complete categories. In International Category Theory Conference (CT), Como, Italy, volume 1488 of Lecture Notes in Mathematics, pages 95–104. Springer-Verlag, 1990. ISBN 978-3-540-46435-8.

[26]

M. Gaboardi, A. Haeberlen, J. Hsu, A. Narayan, and B. C. Pierce. Linear dependent types for differential privacy. In ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL), Rome, Italy, pages 357–370, 2013.

Digital Library

[27]

A. Haeberlen, B. C. Pierce, and A. Narayan. Differential privacy under fire. In USENIX Security Symposium, San Francisco, USA, 2011.

Digital Library

[28]

D. Hofmann, G. J. Seal, and W. Tholen, editors. Monoidal Topology. Cambridge University Press, 2014.

[29]

D. Kozen. Semantics of probabilistic programs. Journal of Computer and System Sciences, 22(3):328–350, 1981.

[30]

N. R. Krishnaswami and N. Benton. Ultrametric semantics of reactive programs. In IEEE Symposium on Logic in Computer Science (LICS), Toronto, Ontario, pages 257–266, 2011.

Digital Library

[31]

D. B. MacQueen, G. D. Plotkin, and R. Sethi. An ideal model for recursive polymorphic types. In ACM Symposium on Principles of Programming Languages (POPL), Salt Lake City, Utah, pages 165–174, 1984.

Digital Library

[32]

M. E. Majster-Cederbaum. On the uniqueness of fixed points of endofunctors in a category of complete metric spaces. Information Processing Letters, 29(6):277–281, 1988.

Digital Library

[33]

M. E. Majster-Cederbaum and F. Zetzsche. Towards a foundation for semantics in complete metric spaces. Information and Computation, 90(2):217–243, 1991.

Digital Library

[34]

M. E. Majster-Cederbaum and F. Zetzsche. The comparison of a CPObased semantics with a CMS-based semantics for CSP. Theoretical Computer Science, 124(1):1–40, 1994.

Digital Library

[35]

H. Nakano. A modality for recursion. In IEEE Symposium on Logic in Computer Science (LICS), Santa Barbara, California, pages 255–266, 2000.

Digital Library

[36]

A. M. Pitts. Relational properties of domains. Information and Computation, 127(2):66–90, 1996.

[37]

G. Plotkin. Lectures on predomains and partial functions. Notes for a course given at the Center for the Study of Language and Information, Stanford, 1985.

[38]

J. Reed and B. C. Pierce. Distance makes the types grow stronger: A calculus for differential privacy. In ACM SIGPLAN International Conference on Functional Programming (ICFP), Baltimore, Maryland, pages 157–168, 2010. ISBN 978-1-60558-794-3.

Digital Library

[39]

J. Schwinghammer, L. Birkedal, and K. Støvring. A step-indexed Kripke model of hidden state via recursive properties on recursively defined metric spaces. In International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), Saarbrücken, Germany, volume 6604 of Lecture Notes in Computer Science, pages 305–319. Springer-Verlag, 2011.

Digital Library

[40]

M. B. Smyth and G. D. Plotkin. The category-theoretic solution of recursive domain equations. SIAM Journal on Computing, 11(4): 761–783, 1982.

Digital Library

[41]

F. van Breugel. An introduction to metric semantics: operational and denotational models for programming and specification languages. Theoretical Computer Science, 258(1–2):1–98, 2001.

Digital Library

[42]

Introduction Metric Spaces Core Fuzz Metric CPOs Preliminaries Adding Metrics Domain Equations Full Fuzz Adapting the Model Metatheory A Remark on Recursive Functions Related Work Conclusion

Cited By

Pistone PGorla D(2021)On generalized metric spaces for the simply typed lambda-calculusProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470696(1-14)Online publication date: 29-Jun-2021
https://dl.acm.org/doi/10.1109/LICS52264.2021.9470696
Lago UGavazzo F(2021)Differential Logical Relations, Part II Increments and DerivativesTheoretical Computer Science10.1016/j.tcs.2021.09.027Online publication date: Sep-2021
https://doi.org/10.1016/j.tcs.2021.09.027
de Amorim AGaboardi MHsu JKatsumata SBouyer P(2019)Probabilistic relational reasoning via metricsProceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science10.5555/3470152.3470192(1-19)Online publication date: 24-Jun-2019
https://dl.acm.org/doi/10.5555/3470152.3470192
Show More Cited By

Index Terms

A semantic account of metric preservation
1. Theory of computation
  1. Semantics and reasoning
    1. Program semantics

Recommendations

A semantic account of metric preservation
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages

Program sensitivity measures how robust a program is to small changes in its input, and is a fundamental notion in domains ranging from differential privacy to cyber-physical systems. A natural way to formalize program sensitivity is in terms of metrics ...
Logics of metric spaces

We investigate the expressive power and computational properties of two different types of languages intended for speaking about distances. First, we consider a first-order language FM the two-variable fragment of which turns out to be undecidable in ...
Observationally-induced Effect Monads: Upper and Lower Powerspace Constructions

Alex Simpson has suggested to use an observationally-induced approach towards modelling computational effects in denotational semantics. The principal idea is that a single observation algebra is used for defining the computational type structure. He ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 52, Issue 1

POPL '17

January 2017

901 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/3093333

Editor:
Matthew Fluet

Issue’s Table of Contents

POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages
January 2017
901 pages
ISBN:9781450346603
DOI:10.1145/3009837
General Chair:
Giuseppe Castagna
Paris Diderot University, France / CNRS, France
,
Program Chair:
Andrew D. Gordon
Microsoft Research, UK / University of Edinburgh, UK

Copyright © 2017 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 January 2017

Published in SIGPLAN Volume 52, Issue 1

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

National Science Foundation
Japan Society for the Promotion of Science
Simons Foundation

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

26
Total Citations
View Citations
657
Total Downloads

Downloads (Last 12 months)127
Downloads (Last 6 weeks)13

Reflects downloads up to 13 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Pistone PGorla D(2021)On generalized metric spaces for the simply typed lambda-calculusProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470696(1-14)Online publication date: 29-Jun-2021
https://dl.acm.org/doi/10.1109/LICS52264.2021.9470696
Lago UGavazzo F(2021)Differential Logical Relations, Part II Increments and DerivativesTheoretical Computer Science10.1016/j.tcs.2021.09.027Online publication date: Sep-2021
https://doi.org/10.1016/j.tcs.2021.09.027
de Amorim AGaboardi MHsu JKatsumata SBouyer P(2019)Probabilistic relational reasoning via metricsProceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science10.5555/3470152.3470192(1-19)Online publication date: 24-Jun-2019
https://dl.acm.org/doi/10.5555/3470152.3470192
Lobo-Vesga ERusso AGaboardi MCortiñas C(2024)Sensitivity by ParametricityProceedings of the ACM on Programming Languages10.1145/36897268:OOPSLA2(415-441)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689726
Kellison AHsu J(2024)Numerical Fuzz: A Type System for Rounding Error AnalysisProceedings of the ACM on Programming Languages10.1145/36564568:PLDI(1954-1978)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656456
Ehling GKutsia T(2024)Solving Quantitative EquationsAutomated Reasoning10.1007/978-3-031-63501-4_20(381-400)Online publication date: 2-Jul-2024
https://doi.org/10.1007/978-3-031-63501-4_20
Pettersson MLjung Ekeroth JRusso A(2023)Calculating Function Sensitivity for Synthetic Data AlgorithmsProceedings of the 35th Symposium on Implementation and Application of Functional Languages10.1145/3652561.3652567(1-12)Online publication date: 29-Aug-2023
https://dl.acm.org/doi/10.1145/3652561.3652567
Toro MDarais DAbuah CNear JÁrquez DOlmedo FTanter É(2023)Contextual Linear Types for Differential PrivacyACM Transactions on Programming Languages and Systems10.1145/358920745:2(1-69)Online publication date: 17-May-2023
https://dl.acm.org/doi/10.1145/3589207
wunder jAmorim ABaillot PGaboardi M(2023)Bunched Fuzz: Sensitivity for Vector MetricsProgramming Languages and Systems10.1007/978-3-031-30044-8_17(451-478)Online publication date: 22-Apr-2023
https://dl.acm.org/doi/10.1007/978-3-031-30044-8_17
Dagnino FPasquali F(2022)Logical Foundations of Quantitative EqualityProceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3531130.3533337(1-13)Online publication date: 2-Aug-2022
https://dl.acm.org/doi/10.1145/3531130.3533337
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents