Document Open Access Logo

Differential Logical Relations, Part I: The Simply-Typed Case (Track B: Automata, Logic, Semantics, and Theory of Programming)

Authors Ugo Dal Lago, Francesco Gavazzo, Akira Yoshimizu

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2019.111.pdf
  • Filesize: 0.55 MB
  • 14 pages

Document Identifiers

Author Details

Ugo Dal Lago
  • University of Bologna, Italy
  • INRIA Sophia Antipolis, France
Francesco Gavazzo
  • IMDEA Software Institute, Spain
Akira Yoshimizu
  • INRIA Sophia Antipolis, France

Funding

The authors are partially supported by the ERC Consolidator Grant DLV-818616 DIAPASoN, as well as by the ANR projects 14CE250005 ELICA and 16CE250011 REPAS.

Cite As Get BibTex

Ugo Dal Lago, Francesco Gavazzo, and Akira Yoshimizu. Differential Logical Relations, Part I: The Simply-Typed Case (Track B: Automata, Logic, Semantics, and Theory of Programming). In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, pp. 111:1-111:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.ICALP.2019.111

Abstract

We introduce a new form of logical relation which, in the spirit of metric relations, allows us to assign each pair of programs a quantity measuring their distance, rather than a boolean value standing for their being equivalent. The novelty of differential logical relations consists in measuring the distance between terms not (necessarily) by a numerical value, but by a mathematical object which somehow reflects the interactive complexity, i.e. the type, of the compared terms. We exemplify this concept in the simply-typed lambda-calculus, and show a form of soundness theorem. We also see how ordinary logical relations and metric relations can be seen as instances of differential logical relations. Finally, we show that differential logical relations can be organised in a cartesian closed category, contrarily to metric relations, which are well-known not to have such a structure, but only that of a monoidal closed category.

Subject Classification

ACM Subject Classification
  • Theory of computation → Lambda calculus
Keywords
  • Logical Relations
  • lambda-Calculus
  • Program Equivalence
  • Semantics

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. S. Abramsky. The Lazy Lambda Calculus. In D. Turner, editor, Research Topics in Functional Programming, pages 65-117. Addison Wesley, 1990. Google Scholar
  2. Samson Abramsky. Abstract Interpretation, Logical Relations and Kan Extensions. J. Log. Comput., 1(1):5-40, 1990. Google Scholar
  3. Mario Alvarez-Picallo and C.-H. Luke Ong. Change Actions: Models of Generalised Differentiation. In Proc. of FOSSACS 2019, pages 45-61, 2019. Google Scholar
  4. A. Arnold and M. Nivat. Metric Interpretations of Infinite Trees and Semantics of non Deterministic Recursive Programs. Theor. Comput. Sci., 11:181-205, 1980. Google Scholar
  5. C. Baier and M.E. Majster-Cederbaum. Denotational Semantics in the CPO and Metric Approach. Theor. Comput. Sci., 135(2):171-220, 1994. Google Scholar
  6. Gilles Barthe, Marco Gaboardi, Justin Hsu, and Benjamin C. Pierce. Programming language techniques for differential privacy. SIGLOG News, 3(1):34-53, 2016. Google Scholar
  7. Michael A. Bukatin, Ralph Kopperman, Steve Matthews, and Homeira Pajoohesh. Partial Metric Spaces. The American Mathematical Monthly, 116(8):708-718, 2009. Google Scholar
  8. Yufei Cai, Paolo G. Giarrusso, Tillmann Rendel, and Klaus Ostermann. A theory of changes for higher-order languages: incrementalizing λ-calculi by static differentiation. In Proc. of PLDI, pages 145-155, 2014. Google Scholar
  9. Konstantinos Chatzikokolakis, Daniel Gebler, Catuscia Palamidessi, and Lili Xu. Generalized Bisimulation Metrics. In CONCUR 2014 - Concurrency Theory - 25th International Conference, CONCUR 2014, Rome, Italy, September 2-5, 2014. Proceedings, pages 32-46, 2014. Google Scholar
  10. Raphaëlle Crubillé and Ugo Dal Lago. Metric Reasoning about λ-Terms: The Affine Case. In Proc. of LICS 2015, pages 633-644, 2015. Google Scholar
  11. Raphaëlle Crubillé and Ugo Dal Lago. Metric Reasoning About λ-Terms: The General Case. In Proc. of ESOP 2017, pages 341-367, 2017. Google Scholar
  12. Ugo Dal Lago, Francesco Gavazzo, and Akira Yoshimizu. Differential Logical Relations, Part I: The Simply-Typed Case (Extended Version), 2018. URL: http://arxiv.org/abs/1904.12137.
  13. A.A. de Amorim, M. Gaboardi, J. Hsu, S. Katsumata, and I. Cherigui. A semantic account of metric preservation. In Proc. of POPL 2017, pages 545-556, 2017. Google Scholar
  14. J.W. de Bakker and J.I. Zucker. Denotational Semantics of Concurrency. In STOC, pages 153-158, 1982. Google Scholar
  15. Josee Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden. Metrics for labelled Markov processes. Theor. Comput. Sci., 318(3):323-354, 2004. Google Scholar
  16. M.H. Escardo. A metric model of PCF. In Workshop on Realizability Semantics and Applications, 1999. Google Scholar
  17. Francesco Gavazzo. Quantitative Behavioural Reasoning for Higher-order Effectful Programs: Applicative Distances. In Proc. of LICS 2018, pages 452-461, 2018. Google Scholar
  18. D. Hofmann, G.J. Seal, and W. Tholen, editors. Monoidal Topology. A Categorical Approach to Order, Metric, and Topology. Number 153 in Encyclopedia of Mathematics and its Applications. Cambridge University Press, 2014. Google Scholar
  19. F.W. Lawvere. Metric spaces, generalized logic, and closed categories. Rend. Sem. Mat. Fis. Milano, 43:135-166, 1973. Google Scholar
  20. John C. Mitchell. Foundations for Programming Languages. MIT Press, 1996. Google Scholar
  21. Sparsh Mittal. A Survey of Techniques for Approximate Computing. ACM Comput. Surv., 48(4), 2016. Google Scholar
  22. J. Morris. Lambda Calculus Models of Programming Languages. PhD thesis, MIT, 1969. Google Scholar
  23. Gordon D. Plotkin. Lambda-Definability and Logical Relations. Memorandum SAI-RM-4, University of Edinburgh, 1973. Google Scholar
  24. J. Reed and B.C. Pierce. Distance makes the types grow stronger: a calculus for differential privacy. In Proc. of ICFP 2010, pages 157-168, 2010. Google Scholar
  25. K.I. Rosenthal. Quantales and their applications. Pitman research notes in mathematics series. Longman Scientific &Technical, 1990. Google Scholar
  26. Dana Scott. Outline of a mathematical theory of computation. Technical Report PRG02, OUCL, November 1970. Google Scholar
  27. Dana Scott and Christopher Strachey. Toward a mathematical semantics for computer languages. Technical Report PRG06, OUCL, August 1971. Google Scholar
  28. F. Van Breugel. An introduction to metric semantics: operational and denotational models for programming and specification languages. Theor. Comput. Sci., 258(1-2):1-98, 2001. Google Scholar
  29. F. Van Breugel and J. Worrell. A behavioural pseudometric for probabilistic transition systems. Theor. Comput. Sci., 331(1):115-142, 2005. Google Scholar
  30. Franck van Breugel and James Worrell. Towards Quantitative Verification of Probabilistic Transition Systems. In Proc. of ICALP 2001, pages 421-432, 2001. Google Scholar
  31. Edwin M. Westbrook and Swarat Chaudhuri. A Semantics for Approximate Program Transformations. CoRR, abs/1304.5531, 2013. URL: http://arxiv.org/abs/1304.5531.
  32. Lili Xu, Konstantinos Chatzikokolakis, and Huimin Lin. Metrics for Differential Privacy in Concurrent Systems. In Proc. of FORTE 2014, pages 199-215, 2014. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact